[Projects] XRM 59: Add (buggy) support for PCTL/CSL formulas.

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit &lt;sigoure.benoit(a)lrde.epita.fr&gt; Add (buggy) support for PCTL/CSL formulas. This commit provides a parser and a pretty printer for PCTL/CSL formulas as used in PRISM. The parser is buggy (several ambiguities to be fixed etc.). The pretty-printer also seems buggy although it seems to be boxing properly the AST, it's (sometimes) rejected by libstratego-gpp for some reason... To be fixed... * src/tools/parse-pctl.str: New. * src/tools/pp-pctl.str: New. * src/tools/Makefile.am: Add parse-pctl and pp-pctl. * src/sig/Makefile.am: Generate signatures for PCTL. * src/lib/pctl: New. * src/lib/pctl/pp: New. * src/lib/pctl/pp/pctl-properties-file.str: New. * src/lib/pctl/pp/pctl-to-abox.str: New. * src/lib/pctl/pp/pctl-path.meta: New. * src/lib/pctl/pp/pctl-label.str: New. * src/lib/pctl/pp/pctl-formula.meta: New. * src/lib/pctl/pp/pctl-property.str: New. * src/lib/pctl/pp/pctl-reward.str: New. * src/lib/pctl/pp/pctl-filter.str: New. * src/lib/pctl/pp/pp-pctl-to-box.str: New. * src/lib/pctl/pp/pctl-properties-file.meta: New. * src/lib/pctl/pp/pctl-path.str: New. * src/lib/pctl/pp/pctl-label.meta: New. * src/lib/pctl/pp/pctl-reward.meta: New. * src/lib/pctl/pp/Makefile.am: New. * src/lib/pctl/pp/pctl-property.meta: New. * src/lib/pctl/pp/pctl-filter.meta: New. * src/lib/pctl/pp/pctl-formula.str: New. * src/lib/pctl/Makefile.am: New. * src/lib/xrm/pp/xrm-to-abox.str: Correct the usage summary. * src/lib/Makefile.am (SUBDIRS): Add pctl. * src/syn/pctl: New. * src/syn/pctl/PCTL-Main.sdf: New. * src/syn/pctl/PCTL-Property.sdf: New. * src/syn/pctl/PCTL-Reward.sdf: New. * src/syn/pctl/PCTL-Filter.sdf: New. * src/syn/pctl/PCTL-Formula.sdf: New. * src/syn/pctl/PCTL-StartSymbols.sdf: New. * src/syn/pctl/StrategoPCTL.sdf: New. * src/syn/pctl/PCTL-Path.sdf: New. * src/syn/pctl/PCTL-PropertiesFile.sdf: New. * src/syn/pctl/Makefile.am: New. * src/syn/pctl/PCTL-Label.sdf: New. * src/syn/pctl/PCTL-MetaCongruences.sdf: New. * src/syn/pctl/PCTL-MetaVars.sdf: New. * src/syn/pctl/PCTL.sdf: New. * src/syn/Makefile.am (SUBDIRS): Add pctl. * src/syn/prism/PRISM-Label.sdf: Remove. * tests/pctl: New. * tests/pctl/man_examples.pctl: New. * tests/test-parse-pctl.sh.in: New. * tests/test-pp-pctl.sh.in: New. * tests/Makefile.am: Add test-parse-pctl and test-pp-pctl. * configure.ac: Ditto. * TODO: New idea (-O option for xrm-front to produce optimized PRISM code). TODO | 49 +++++++ configure.ac | 9 + src/lib/Makefile.am | 4 src/lib/pctl/Makefile.am | 11 + src/lib/pctl/pp/Makefile.am | 38 +++++ src/lib/pctl/pp/pctl-filter.meta | 1 src/lib/pctl/pp/pctl-filter.str | 13 + src/lib/pctl/pp/pctl-formula.meta | 1 src/lib/pctl/pp/pctl-formula.str | 6 src/lib/pctl/pp/pctl-label.meta | 1 src/lib/pctl/pp/pctl-label.str | 7 + src/lib/pctl/pp/pctl-path.meta | 1 src/lib/pctl/pp/pctl-path.str | 22 +++ src/lib/pctl/pp/pctl-properties-file.meta | 1 src/lib/pctl/pp/pctl-properties-file.str | 7 + src/lib/pctl/pp/pctl-property.meta | 1 src/lib/pctl/pp/pctl-property.str | 184 +++++++++++++++++++++++++++ src/lib/pctl/pp/pctl-reward.meta | 1 src/lib/pctl/pp/pctl-reward.str | 15 ++ src/lib/pctl/pp/pctl-to-abox.str | 53 +++++++ src/lib/pctl/pp/pp-pctl-to-box.str | 35 +++++ src/lib/xrm/pp/xrm-to-abox.str | 2 src/sig/Makefile.am | 9 + src/syn/Makefile.am | 4 src/syn/pctl/Makefile.am | 65 +++++++++ src/syn/pctl/PCTL-Filter.sdf | 17 ++ src/syn/pctl/PCTL-Formula.sdf | 24 +++ src/syn/pctl/PCTL-Label.sdf | 5 src/syn/pctl/PCTL-Main.sdf | 4 src/syn/pctl/PCTL-MetaCongruences.sdf | 12 + src/syn/pctl/PCTL-MetaVars.sdf | 11 + src/syn/pctl/PCTL-Path.sdf | 23 +++ src/syn/pctl/PCTL-PropertiesFile.sdf | 22 +++ src/syn/pctl/PCTL-Property.sdf | 203 ++++++++++++++++++++++++++++++ src/syn/pctl/PCTL-Reward.sdf | 19 ++ src/syn/pctl/PCTL-StartSymbols.sdf | 17 ++ src/syn/pctl/PCTL.sdf | 11 + src/syn/pctl/StrategoPCTL.sdf | 26 +++ src/tools/Makefile.am | 10 + src/tools/parse-pctl.str | 38 ++--- src/tools/pp-pctl.str | 27 +-- tests/Makefile.am | 6 tests/pctl/man_examples.pctl | 96 ++++++++++++++ tests/test-parse-pctl.sh.in | 6 tests/test-pp-pctl.sh.in | 14 +- 45 files changed, 1074 insertions(+), 57 deletions(-) Index: src/tools/parse-pctl.str --- src/tools/parse-pctl.str (revision 58) +++ src/tools/parse-pctl.str (working copy) @@ -1,23 +1,23 @@ // Code mostly from parse-java by Martin Bravenboer &lt;martin(a)cs.uu.nl&gt; -module parse-prism +module parse-pctl imports libxtclib // FIXME: import libstratego-xtc for strc 0.17 tool-doc parser-common strategies - main-parse-prism = + main-parse-pctl = // xtc-io-wrap(extra-opts, usage, about, deps, s) xtc-io-wrap( - parse-prism-options - , parse-prism-usage + parse-pctl-options + , parse-pctl-usage , parser-about - , !["sglr", "implode-asfix", "PRISM.tbl", "pp-aterm"] - , parse-prism + , !["sglr", "implode-asfix", "PCTL.tbl", "pp-aterm"] + , parse-pctl ) - parse-prism-options = + parse-pctl-options = symbol-option + preserve-comments-option + preserve-positions-option @@ -26,7 +26,7 @@ strategies - parse-prism = + parse-pctl = where(?FILE(input-file-name) + !"stdin" => input-file-name) ; xtc-sglr-no-heuristics(get-parse-table, get-start-symbol) ; if must-preserve-comments then @@ -47,29 +47,29 @@ ArgOption("-s" + "--start-symbol" , set-start-symbol , !HelpString("-s | --start-symbol s", - "Start parsing with symbol s [ModulesFile]") + "Start parsing with symbol s [PropertiesFile]") ) set-start-symbol = <set-config> ("start-symbol", <id>) get-start-symbol = - <get-config> "start-symbol" <+ !"ModulesFile" + <get-config> "start-symbol" <+ !"PropertiesFile" strategies /* - ** We use two parse tables for performances. One of them (PRISM.tbl) has a - ** single start symbol (ModulesFile) and the other (PRISM-StartSymbols) has + ** We use two parse tables for performances. One of them (PCTL.tbl) has a + ** single start symbol (ModulesFile) and the other (PCTL-StartSymbols) has ** several other start symbols. We're doing this because start symbol ** selection happens *after* parsing in sglr. So first all the alternatives ** are parsed, and then the selected start symbol is chosen. */ get-parse-table = - <get-config> "parsetable"; not(?"PRISM.tbl") - <+ if get-start-symbol => "ModulesFile" then - !"PRISM.tbl" + <get-config> "parsetable"; not(?"PCTL.tbl") + <+ if get-start-symbol => "PropertiesFile" then + !"PCTL.tbl" else - !"PRISM-StartSymbols.tbl" + !"PCTL-StartSymbols.tbl" end /** @@ -77,11 +77,11 @@ */ strategies - parse-prism-usage = + parse-pctl-usage = <tool-doc> - [ Usage("parse-prism [OPTIONS]") + [ Usage("parse-pctl [OPTIONS]") , Summary( - "Parses a PRISM source file to an abstract syntax + "Parses a PCTL source file to an abstract syntax tree in the ATerm format.") , OptionUsage() , AutoReportBugs() Index: src/tools/pp-pctl.str --- src/tools/pp-pctl.str (revision 58) +++ src/tools/pp-pctl.str (working copy) @@ -1,26 +1,26 @@ // Code mostly from pp-java by Martin Bravenboer &lt;martin(a)cs.uu.nl&gt; -module pp-xrm +module pp-pctl imports libstratego-lib tool-doc libstratego-gpp - pp-xrm-to-box + pp-pctl-to-box strategies - main-pp-xrm = + main-pp-pctl = // io-stream-wrap(extra-opts, usage, about, s) io-stream-wrap( fail - , pp-xrm-usage - , pp-xrm-about - , pp-xrm + , pp-pctl-usage + , pp-pctl-about + , pp-pctl ) - pp-xrm = + pp-pctl = ?(<read-from-stream>, out-file) - ; pp-xrm-to-abox + ; pp-pctl-to-abox ; box2text-stream(|80, out-file) ; <fputs> ("\n", out-file) @@ -29,17 +29,16 @@ */ strategies - pp-xrm-usage = + pp-pctl-usage = <tool-doc> - [ Usage("pp-xrm [OPTIONS]") - , Summary("Pretty-prints an eXtended Reactive Module abstract syntax - tree in ATerm format to an eXtended Reactive Module source - file.") + [ Usage("pp-pctl [OPTIONS]") + , Summary("Pretty-prints a PCTL abstract syntax tree in ATerm format + to an eXtended Reactive Module source file.") , OptionUsage() , AutoReportBugs() ] - pp-xrm-about = + pp-pctl-about = <tool-doc> [ AutoProgram() , Author(Person("SIGOURE Benoit", &quot;sigoure.benoit(a)lrde.epita.fr&quot;)) Index: src/tools/Makefile.am --- src/tools/Makefile.am (revision 58) +++ src/tools/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; ## ## Started on Mon May 8 21:16:56 2006 SIGOURE Benoit -## Last update Fri Jun 2 17:57:09 2006 SIGOURE Benoit +## Last update Sat Jun 10 04:48:43 2006 SIGOURE Benoit ## include $(top_srcdir)/config/Transformers.mk @@ -13,8 +13,10 @@ bin_PROGRAMS = \ parse-prism \ + parse-pctl \ parse-xrm \ pp-prism \ + pp-pctl \ pp-xrm EXTRA_DIST = $(wildcard *.str) $(wildcard *.meta) @@ -25,8 +27,10 @@ -I $(GPP)/share/sdf/gpp \ $(STRATEGO_GPP_STRCFLAGS) \ -I $(top_srcdir)/src/lib/prism/pp \ + -I $(top_srcdir)/src/lib/pctl/pp \ -I $(top_srcdir)/src/lib/xrm/pp \ -I $(top_builddir)/src/lib/prism/pp \ + -I $(top_builddir)/src/lib/pctl/pp \ -I $(top_builddir)/src/lib/xrm/pp \ -I $(top_builddir)/src/sig LDADD += $(SSL_LIBS) @@ -35,6 +39,10 @@ pp_prism_SOURCES = pp-prism.c pp_prism_LDADD = $(STRATEGO_GPP_LIBS) +parse_pctl_SOURCES = parse-pctl.c +pp_pctl_SOURCES = pp-pctl.c +pp_pctl_LDADD = $(STRATEGO_GPP_LIBS) + parse_xrm_SOURCES = parse-xrm.c pp_xrm_SOURCES = pp-xrm.c pp_xrm_LDADD = $(STRATEGO_GPP_LIBS) Index: src/sig/Makefile.am --- src/sig/Makefile.am (revision 58) +++ src/sig/Makefile.am (working copy) @@ -5,16 +5,17 @@ ## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; ## ## Started on Mon May 8 18:38:32 2006 SIGOURE Benoit -## Last update Thu May 25 23:41:55 2006 SIGOURE Benoit +## Last update Sat Jun 10 04:43:36 2006 SIGOURE Benoit ## include $(top_srcdir)/config/Transformers.mk pkgdata_DATA = PRISM.rtg PRISM.str \ + PCTL.rtg PCTL.str \ XRM.rtg XRM.str EXTRA_DIST = $(pkgdata_DATA) -CLEANFILES = $(pkgdata_DATA) PRISM.def XRM.def +CLEANFILES = $(pkgdata_DATA) PRISM.def PCTL.def XRM.def SDF2RTG_FLAGS = --main $* @@ -22,6 +23,10 @@ rm -f $@ $(LN_S) $(top_builddir)/src/syn/prism/$@ $@ +PCTL.def: $(top_builddir)/src/syn/pctl/PCTL.def + rm -f $@ + $(LN_S) $(top_builddir)/src/syn/pctl/$@ $@ + XRM.def: $(top_builddir)/src/syn/xrm/XRM.def rm -f $@ $(LN_S) $(top_builddir)/src/syn/xrm/$@ $@ Index: src/lib/pctl/pp/pctl-properties-file.str --- src/lib/pctl/pp/pctl-properties-file.str (revision 0) +++ src/lib/pctl/pp/pctl-properties-file.str (revision 0) @@ -0,0 +1,7 @@ +module pctl-properties-file + +rules + // PropertiesFileSection* -> PropertiesFile + prism-to-box: + PropertiesFile(properties-file-sections) + -> box |[ V vs=1 [ ~*properties-file-sections ] ]| Index: src/lib/pctl/pp/pctl-to-abox.str --- src/lib/pctl/pp/pctl-to-abox.str (revision 0) +++ src/lib/pctl/pp/pctl-to-abox.str (revision 0) @@ -0,0 +1,53 @@ +module pctl-to-abox +imports + libxtclib // FIXME: import libstratego-xtc for strc 0.17 + tool-doc + pp-pctl-to-box + +strategies + + main-pctl-to-abox = + // xtc-io-wrap(extra-opts, usage, about, deps, s) + xtc-io-wrap( + fail + , pctl-to-abox-usage + , pctl-to-abox-about + , ![] + , main-wrapped + ) + + // main wrapped in main-pctl-to-abox + main-wrapped = + // read data from input + read-from + ; pp-pctl-to-abox + ; if <get-config> "-b" then + write-to // write binary output + else + write-to-text // write text output + end + +/** + * Documentation + */ +strategies + + pctl-to-abox-usage = + <tool-doc> + [ Usage("pctl-to-abox [OPTIONS]") + , Summary("Transforms a PCTL abstract syntax tree in ATerm format + to a box representation of the AST for pretty-printing") + , OptionUsage() + , AutoReportBugs() + ] + + pctl-to-abox-about = + <tool-doc> + [ AutoProgram() + , Author(Person("SIGOURE Benoit", &quot;sigoure.benoit(a)lrde.epita.fr&quot;)) + , GNU_GPL("2006", "SIGOURE Benoit &lt;sigoure.benoit(a)lrde.epita.fr&gt;&quot;) + , Config([ + DefaultXTCRepository() + , CurrentXTCRepository() + ]) + ] Index: src/lib/pctl/pp/pctl-path.meta --- src/lib/pctl/pp/pctl-path.meta (revision 0) +++ src/lib/pctl/pp/pctl-path.meta (revision 0) @@ -0,0 +1 @@ +Meta([Syntax("Stratego-Box")]) Index: src/lib/pctl/pp/pctl-label.str --- src/lib/pctl/pp/pctl-label.str (revision 0) +++ src/lib/pctl/pp/pctl-label.str (revision 0) @@ -0,0 +1,7 @@ +module pctl-label + +rules + // "label" "\"" Identifier "\"" "=" Expression ";" -> LabelDef + prism-to-box: + LabelDef(idf, exp) + -> H hs=1 [ KW["label"] "\"" ~idf "\"" "=" H hs=0 [~exp ";"] ] Index: src/lib/pctl/pp/pctl-formula.meta --- src/lib/pctl/pp/pctl-formula.meta (revision 0) +++ src/lib/pctl/pp/pctl-formula.meta (revision 0) @@ -0,0 +1 @@ +Meta([Syntax("Stratego-Box")]) Index: src/lib/pctl/pp/pctl-property.str --- src/lib/pctl/pp/pctl-property.str (revision 0) +++ src/lib/pctl/pp/pctl-property.str (revision 0) @@ -0,0 +1,184 @@ +module pctl-property + +rules + + prism-to-box: + Implies(lhs, rhs) -> H hs=1 [~lhs MATH["=>"] ~rhs] + + // already imported from PRISM's boxer + //prism-to-box: + // Or(lhs, rhs) -> H hs=1 [~lhs MATH["|"] ~rhs] + + // already imported from PRISM's boxer + //prism-to-box: + // And(lhs, rhs) -> H hs=1 [~lhs MATH["|"] ~rhs] + + // already imported from PRISM's boxer + //prism-to-box: + // Not(exp) -> H hs=0 [ MATH["!"] ~exp ] + + /* P Operator */ + + prism-to-box: + ProbLt(exp, path, None()) + -> H hs=1 [ H hs=0[ KW["P"] MATH["<"] ~exp ] "[" ~path "]" ] + + prism-to-box: + ProbLt(exp, path, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["P"] MATH["<"] ~exp ] "[" ~path ~filter_ "]" ] + + prism-to-box: + ProbLtEq(exp, path, None()) + -> H hs=1 [ H hs=0[ KW["P"] MATH["<="] ~exp ] "[" ~path "]" ] + + prism-to-box: + ProbLtEq(exp, path, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["P"] MATH["<="] ~exp ] "[" ~path ~filter_ "]" ] + + prism-to-box: + ProbGt(exp, path, None()) + -> H hs=1 [ H hs=0[ KW["P"] MATH[">"] ~exp ] "[" ~path "]" ] + + prism-to-box: + ProbGt(exp, path, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["P"] MATH[">"] ~exp ] "[" ~path ~filter_ "]" ] + + prism-to-box: + ProbGtEq(exp, path, None()) + -> H hs=1 [ H hs=0[ KW["P"] MATH[">="] ~exp ] "[" ~path "]" ] + + prism-to-box: + ProbGtEq(exp, path, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["P"] MATH[">="] ~exp ] "[" ~path ~filter_ "]" ] + + prism-to-box: + ProbEq(path, None()) + -> H hs=1 [ H hs=0[ KW["P"] MATH["=?"] ] "[" ~path "]" ] + + prism-to-box: + ProbEq(path, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["P"] MATH["=?"] ] "[" ~path ~filter_ "]" ] + + prism-to-box: + ProbAtLeast(path, None()) + -> H hs=1 [ KW["Pmin"] MATH["=?"] "[" ~path "]" ] + + prism-to-box: + ProbAtLeast(path, Some(filter_)) + -> H hs=1 [ KW["Pmin"] MATH["=?"] "[" ~path ~filter_ "]" ] + + prism-to-box: + ProbAtMost(path, None()) + -> H hs=1 [ KW["Pmax"] MATH["=?"] "[" ~path "]" ] + + prism-to-box: + ProbAtMost(path, Some(filter_)) + -> H hs=1 [ KW["Pmax"] MATH["=?"] "[" ~path ~filter_ "]" ] + + /* S Operator */ + + prism-to-box: + SteadyLt(exp, formula, None()) + -> H hs=1 [ H hs=0[ KW["S"] MATH["<"] ~exp ] "[" ~formula "]" ] + + prism-to-box: + SteadyLt(exp, formula, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["S"] MATH["<"] ~exp ] "[" ~formula "{" ~filter_ "}" "]" ] + + prism-to-box: + SteadyLtEq(exp, formula, None()) + -> H hs=1 [ H hs=0[ KW["S"] MATH["<="] ~exp ] "[" ~formula "]" ] + + prism-to-box: + SteadyLtEq(exp, formula, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["S"] MATH["<="] ~exp ] "[" ~formula "{" ~filter_ "}" "]" ] + + prism-to-box: + SteadyGt(exp, formula, None()) + -> H hs=1 [ H hs=0[ KW["S"] MATH[">"] ~exp ] "[" ~formula "]" ] + + prism-to-box: + SteadyGt(exp, formula, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["S"] MATH[">"] ~exp ] "[" ~formula ~filter_ "]" ] + + prism-to-box: + SteadyGtEq(exp, formula, None()) + -> H hs=1 [ H hs=0[ KW["S"] MATH[">="] ~exp ] "[" ~formula "]" ] + + prism-to-box: + SteadyGtEq(exp, formula, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["S"] MATH[">="] ~exp ] "[" ~formula "{" ~filter_ "}" "]" ] + + prism-to-box: + SteadyEq(formula, None()) + -> H hs=1 [ H hs=0[ KW["S"] MATH["=?"] ] "[" ~formula "]" ] + + prism-to-box: + SteadyEq(formula, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["S"] MATH["=?"] ] "[" ~formula "{" ~filter_ "}" "]" ] + + /* Reward stuff */ + + prism-to-box: + RewardLt(exp, reward, None()) + -> H hs=1 [ H hs=0[ KW["R"] MATH["<"] ~exp ] "[" ~reward "]" ] + + prism-to-box: + RewardLt(exp, reward, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["R"] MATH["<"] ~exp ] "[" ~reward ~filter_ "]" ] + + prism-to-box: + RewardLtEq(exp, reward, None()) + -> H hs=1 [ H hs=0[ KW["R"] MATH["<="] ~exp ] "[" ~reward "]" ] + + prism-to-box: + RewardLtEq(exp, reward, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["R"] MATH["<="] ~exp ] "[" ~reward ~filter_ "]" ] + + prism-to-box: + RewardGt(exp, reward, None()) + -> H hs=1 [ H hs=0[ KW["R"] MATH[">"] ~exp ] "[" ~reward "]" ] + + prism-to-box: + RewardGt(exp, reward, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["R"] MATH[">"] ~exp ] "[" ~reward ~filter_ "]" ] + + prism-to-box: + RewardGtEq(exp, reward, None()) + -> H hs=1 [ H hs=0[ KW["R"] MATH[">="] ~exp ] "[" ~reward "]" ] + + prism-to-box: + RewardGtEq(exp, reward, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["R"] MATH[">="] ~exp ] "[" ~reward ~filter_ "]" ] + + prism-to-box: + RewardEq(reward, None()) + -> H hs=1 [ H hs=0[ KW["R"] MATH["=?"] ] "[" ~reward "]" ] + + prism-to-box: + RewardEq(reward, Some(filter_)) + -> H hs=1 [ H hs=0[ KW["R"] MATH["=?"] ] "[" ~reward ~filter_ "]" ] + + prism-to-box: + RewardAtLeast(reward, None()) + -> H hs=1 [ KW["Rmin"] MATH["=?"] "[" ~reward "]" ] + + prism-to-box: + RewardAtLeast(reward, Some(filter_)) + -> H hs=1 [ KW["Rmin"] MATH["=?"] "[" ~reward ~filter_ "]" ] + + prism-to-box: + RewardAtMost(reward, None()) + -> H hs=1 [ KW["Rmax"] MATH["=?"] "[" ~reward "]" ] + + prism-to-box: + RewardAtMost(reward, Some(filter_)) + -> H hs=1 [ KW["Rmax"] MATH["=?"] "[" ~reward ~filter_ "]" ] + + /* Misc. stuff */ + + prism-to-box: + Init() -> H hs=0 ["\"" KW["init"] "\""] + + prism-to-box: + Label(s) -> H hs=0 ["\"" s "\""] Index: src/lib/pctl/pp/pctl-reward.str --- src/lib/pctl/pp/pctl-reward.str (revision 0) +++ src/lib/pctl/pp/pctl-reward.str (revision 0) @@ -0,0 +1,15 @@ +module pctl-reward + +rules + + prism-to-box: + Cumul(exp) -> H hs=0 [ KW["C"] MATH["<="] ~exp ] + + prism-to-box: + Inst(exp) -> H hs=0 [ KW["I"] MATH["="] ~exp ] + + prism-to-box: + Reach(formula) -> H hs=1 [ KW["F"] ~formula ] + + prism-to-box: + Steady() -> box |[ KW["S"] ]| Index: src/lib/pctl/pp/pctl-filter.str --- src/lib/pctl/pp/pctl-filter.str (revision 0) +++ src/lib/pctl/pp/pctl-filter.str (revision 0) @@ -0,0 +1,13 @@ +module pctl-filter + +rules + + prism-to-box: + Filter(formula, min-max-list) + -> H hs=0 [ "{" ~formula "}" ~*min-max-list ] + + prism-to-box: + ComputeMin() -> H hs=0 [ "{" KW["min"] "}" ] + + prism-to-box: + ComputeMax() -> H hs=0 [ "{" KW["max"] "}" ] Index: src/lib/pctl/pp/pp-pctl-to-box.str --- src/lib/pctl/pp/pp-pctl-to-box.str (revision 0) +++ src/lib/pctl/pp/pp-pctl-to-box.str (revision 0) @@ -0,0 +1,35 @@ +module pp-pctl-to-box +imports + Box + PCTL // signature + PRISM // needed because we use PRISM's Expression etc... + prism-constant + prism-expression + pctl-parenthesize + pctl-properties-file + pctl-label + pctl-formula + pctl-property + pctl-path + pctl-reward + pctl-filter + +strategies + + pp-pctl-to-abox = + pp-pctl-to-abox(prism-to-box) // we keep prism-to-box as rule name + // because we simply extend it + + pp-pctl-to-abox(pprules) = + // strategy from pctl-parenthesize.str generated by sdf2parenthesize + parenthesize-PCTL + ; topdown(try(very-special-conflict) + ; repeat(pprules)) + +rules + + very-special-conflict: + Minus(Minus(e)) -> Minus(Parenthetical(Minus(e))) + + very-special-conflict: + Plus(Plus(e)) -> Plus(Parenthetical(Plus(e))) Index: src/lib/pctl/pp/pctl-properties-file.meta --- src/lib/pctl/pp/pctl-properties-file.meta (revision 0) +++ src/lib/pctl/pp/pctl-properties-file.meta (revision 0) @@ -0,0 +1 @@ +Meta([Syntax("Stratego-Box")]) Index: src/lib/pctl/pp/pctl-path.str --- src/lib/pctl/pp/pctl-path.str (revision 0) +++ src/lib/pctl/pp/pctl-path.str (revision 0) @@ -0,0 +1,22 @@ +module pctl-path + +rules + + prism-to-box: + Next(formula) -> H hs=1 [ KW["X"] ~formula ] + + prism-to-box: + BoundedUntilLtEq(f1, exp, f2) + -> H hs=1 [ ~f1 H hs=0 [KW["U"] MATH["<="] ~exp] ~f2 ] + + prism-to-box: + BoundedUntilGtEq(f1, exp, f2) + -> H hs=1 [ ~f1 H hs=0 [KW["U"] MATH[">="] ~exp] ~f2 ] + + prism-to-box: + BoundedUntilRange(f1, range-start, range-end, f2) + -> H hs=1 [ ~f1 H hs=0 [KW["U"] "[" ~range-start "," ~range-end "]"] ~f2 ] + + prism-to-box: + Until(f1, f2) + -> H hs=1 [ ~f1 KW["U"] ~f2 ] Index: src/lib/pctl/pp/pctl-label.meta --- src/lib/pctl/pp/pctl-label.meta (revision 0) +++ src/lib/pctl/pp/pctl-label.meta (revision 0) @@ -0,0 +1 @@ +Meta([Syntax("Stratego-Box")]) Index: src/lib/pctl/pp/pctl-reward.meta --- src/lib/pctl/pp/pctl-reward.meta (revision 0) +++ src/lib/pctl/pp/pctl-reward.meta (revision 0) @@ -0,0 +1 @@ +Meta([Syntax("Stratego-Box")]) Index: src/lib/pctl/pp/Makefile.am --- src/lib/pctl/pp/Makefile.am (revision 0) +++ src/lib/pctl/pp/Makefile.am (revision 0) @@ -0,0 +1,38 @@ +## +## Makefile.am for xrm in /home/tsuna/work/xrm/trunk/src/lib/pctl/pp +## +## Made by SIGOURE Benoit +## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; +## +## Started on Sat Jun 10 03:59:11 2006 SIGOURE Benoit +## Last update Sat Jun 10 04:00:21 2006 SIGOURE Benoit +## + +include $(top_srcdir)/config/toplevel.mk +-include $(wildcard *.dep) + +pkgdata_DATA = pctl-parenthesize.str +libexec_PROGRAMS = pctl-to-abox + +pctl_to_abox_SOURCES = pctl-to-abox.c + +STRINCLUDES = -I $(GPP)/share/sdf/gpp -I $(GPP)/share/gpp \ + -I $(top_srcdir)/src/lib/prism/pp \ + -I $(top_builddir)/src/lib/pctl/pp -I $(srcdir) \ + -I $(top_builddir)/src/sig +SCFLAGS = --main main-$* +LDADD += $(SSL_LIBS) + +# We put it in BUILT_SOURCES so that it's symlinked before we compile +# pctl-to-abox +BUILT_SOURCES = pctl-parenthesize.str + +EXTRA_DIST = $(wildcard *.str) $(wildcard *.meta) + +pctl-parenthesize.str: $(top_builddir)/src/syn/pctl/PCTL.def + $(SDF_TOOLS)/bin/sdf2parenthesize -i $< -o $@ \ + -m PCTL \ + --omod pctl-parenthesize \ + --sig-module $(top_builddir)/src/sig/PCTL \ + --main-strategy io-pctl-parenthesize \ + --lang PCTL Index: src/lib/pctl/pp/pctl-property.meta --- src/lib/pctl/pp/pctl-property.meta (revision 0) +++ src/lib/pctl/pp/pctl-property.meta (revision 0) @@ -0,0 +1 @@ +Meta([Syntax("Stratego-Box")]) Index: src/lib/pctl/pp/pctl-filter.meta --- src/lib/pctl/pp/pctl-filter.meta (revision 0) +++ src/lib/pctl/pp/pctl-filter.meta (revision 0) @@ -0,0 +1 @@ +Meta([Syntax("Stratego-Box")]) Index: src/lib/pctl/pp/pctl-formula.str --- src/lib/pctl/pp/pctl-formula.str (revision 0) +++ src/lib/pctl/pp/pctl-formula.str (revision 0) @@ -0,0 +1,6 @@ +module pctl-formula + +rules + // Property -> Formula + prism-to-box: + Formula(prop) -> prop Index: src/lib/pctl/Makefile.am --- src/lib/pctl/Makefile.am (revision 0) +++ src/lib/pctl/Makefile.am (revision 0) @@ -0,0 +1,11 @@ +## +## Makefile.am for xrm in /home/tsuna/work/xrm/trunk/src/lib/pctl +## +## Made by SIGOURE Benoit +## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; +## +## Started on Sat Jun 10 03:57:49 2006 SIGOURE Benoit +## Last update Sat Jun 10 03:58:01 2006 SIGOURE Benoit +## + +SUBDIRS = pp Index: src/lib/xrm/pp/xrm-to-abox.str --- src/lib/xrm/pp/xrm-to-abox.str (revision 58) +++ src/lib/xrm/pp/xrm-to-abox.str (working copy) @@ -35,7 +35,7 @@ xrm-to-abox-usage = <tool-doc> [ Usage("xrm-to-abox [OPTIONS]") - , Summary("Transforms a PRISM abstract syntax tree in ATerm format + , Summary("Transforms an XRM abstract syntax tree in ATerm format to a box representation of the AST for pretty-printing") , OptionUsage() , AutoReportBugs() Index: src/lib/Makefile.am --- src/lib/Makefile.am (revision 58) +++ src/lib/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; ## ## Started on Wed May 10 19:27:12 2006 SIGOURE Benoit -## Last update Thu May 25 18:55:45 2006 SIGOURE Benoit +## Last update Sat Jun 10 03:57:26 2006 SIGOURE Benoit ## -SUBDIRS = prism xrm native +SUBDIRS = prism pctl xrm native Index: src/syn/pctl/PCTL-Main.sdf --- src/syn/pctl/PCTL-Main.sdf (revision 0) +++ src/syn/pctl/PCTL-Main.sdf (revision 0) @@ -0,0 +1,4 @@ +module PCTL-Main +imports + PRISM-Layout + PCTL-PropertiesFile Index: src/syn/pctl/PCTL-Property.sdf --- src/syn/pctl/PCTL-Property.sdf (revision 0) +++ src/syn/pctl/PCTL-Property.sdf (revision 0) @@ -0,0 +1,203 @@ +module PCTL-Property +imports + PRISM-Expression + PRISM-Identifier + PCTL-Formula + PCTL-Path + PCTL-Reward + PCTL-Filter +exports + + %% EBNF Grammar: PCTL Properties + %% + %% Property ::= + %% "true" + %% | "false" + %% | Property "=>" Property + %% | Property "|" Property + %% | Property "&" Property + %% | "!" Property + %% | "P" "<" Expression "[" Path [Filter] "]" + %% | "P" "<=" Expression "[" Path [Filter] "]" + %% | "P" ">" Expression "[" Path [Filter] "]" + %% | "P" ">=" Expression "[" Path [Filter] "]" + %% | "P" "=?" "[" Path [Filter] "]" + %% | Pmin "=?" "[" Path [Filter] "]" + %% | Pmax "=?" "[" Path [Filter] "]" + %% + %% | "S" "<" Expression "[" Formula ["{" Formula "}"] "]" + %% | "S" "<=" Expression "[" Formula ["{" Formula "}"] "]" + %% | "S" ">" Expression "[" Formula ["{" Formula "}"] "]" + %% | "S" ">=" Expression "[" Formula ["{" Formula "}"] "]" + %% | "S" "=?" "[" Formula ("{" Formula "}")? "]" + %% + %% | "R" "<" Expression "[" Reward [Filter] "]" + %% | "R" "<=" Expression "[" Reward [Filter] "]" + %% | "R" ">" Expression "[" Reward [Filter] "]" + %% | "R" ">=" Expression "[" Reward [Filter] "]" + %% | "R" "=?" "[" Reward [Filter] "]" + %% | Rmin "=?" "[" Reward [Filter] "]" + %% | Rmax "=?" "[" Reward [Filter] "]" + %% + %% | "\"init\"" + %% | "\"" + %% | Expression + %% + %% Rmin ::= "R" "min" | "Rmin" + %% Rmax ::= "R" "max" | "Rmax" + + %% EBNF Grammar: PCTL Properties as in PRISM's parser + %% + %% PCTLOr ::= PCTLAnd ["|" PCTLAnd] + %% + %% PCTLAnd ::= PCTLNot ["&" PCTLNot] + %% + %% PCTLNot ::= ["!"] PCTLProb + %% + %% PCTLProb ::= + %% { + %% "P" LtGt Expression + %% | "P" "=" "?" + %% | "P" "min" "=" "?" + %% | "P" "max" "=" "?" + %% | "Pmin" "=" "?" + %% | "Pmax" "=" "?" + %% } "[" + %% { PCTLProbNext | PCTLProbBoundedUntil | PCTLProbUntil } + %% ["{" PCTLFormula "}" { "{" "min" "}" | ( "{" "max" "}" }] + %% "]" + %% | PCTLSS + %% + %% PCTLProbNext ::= "X" PCTLFormula + %% + %% PCTLProbBoundedUntil ::= + %% PCTLFormula "U" "<=" Expression PCTLFormula + %% | PCTLFormula "U" ">=" Expression PCTLFormula + %% | PCTLFormula "U" "[" Expression, Expression "]" PCTLFormula + %% + %% PCTLProbUntil ::= PCTLFormula "U" PCTLFormula + %% + %% PCTLSS ::= + %% { + %% "S" LtGt Expression + %% | "S" "=" "?" + %% } "[" + %% PCTLFormula ["{" PCTLFormula "}"] + %% "]" + %% | PCTLReward + %% + %% PCTLReward ::= + %% { + %% "R" LtGt Expression + %% | "R" "=" "?" + %% | "R" "min" "=" "?" + %% | "R" "max" "=" "?" + %% | "Rmin" "=" "?" + %% | "Rmax" "=" "?" + %% } "[" + %% {PCTLRewardCumul | PCTLRewardInst | PCTLRewardReach | PCTLRewardSS} + %% ["{" PCTLFormula "}" { "{" "min" "}" | "{" "max" "}" }] + %% "]" + %% | PCTLInit + %% + %% PCTLRewardCumul ::= "C" "<=" Expression + %% + %% PCTLRewardInst ::= "I" "=" Expression + %% + %% PCTLRewardReach ::= "F" PCTLFormula + %% + %% PCTLRewardSS ::= "S" + %% + %% PCTLInit ::= + %% "\"" "init" "\"" + %% | PCTLLabel + %% + %% PCTLLabel ::= + %% "\"" Identifier "\"" + %% | PCTLBrackets + %% + %% PCTLBrackets ::= + %% "(" PCTLFormula ")" + %% | PCTLExpression + %% + %% (* Comment from PRISM's parser: + %% * Note that we jump into the middle of the Expression hierarchy. + %% * In practice, this means that Boolean conjunctives in expressions + %% * must be below at least one level of parentheses. Otherwise, the + %% * fact that both PCTLFormulas and Expressions can contain such + %% * operators leads to an ambiguous grammar and a whole world of + %% * associated problems. Chances are the or/and/not will just be + %% * happily parsed as a PCTL operator anyway. Note that this is + %% * not true for the if-then-else operator which is not present in + %% * PCTL but has lower precedence than or/and/not. Oh well. + %% *) + %% PCTLExpression ::= + %% ExpressionRelOpRange + + sorts Property + context-free syntax + %% The two following are inherited by Expression -> Property (see below) + %%"true" -> Property {cons("True")} + %%"false" -> Property {cons("False")} + Property "=>" Property -> Property {cons("Implies")} + Property "|" Property -> Property {cons("Or")} + Property "&" Property -> Property {cons("And")} + "!" Property -> Property {cons("Not")} + + "P" "<" Expression "[" Path Filter? "]" -> Property {cons("ProbLt")} + "P" "<=" Expression "[" Path Filter? "]" -> Property {cons("ProbLtEq")} + "P" ">" Expression "[" Path Filter? "]" -> Property {cons("ProbGt")} + "P" ">=" Expression "[" Path Filter? "]" -> Property {cons("ProbGtEq")} + "P" "=?" "[" Path Filter? "]" -> Property {cons("ProbEq")} + "P" "min" "=?" "[" Path Filter? "]" -> Property {cons("ProbAtLeast")} + "Pmin" "=?" "[" Path Filter? "]" -> Property {cons("ProbAtLeast")} + "P" "max" "=?" "[" Path Filter? "]" -> Property {cons("ProbAtMost")} + "Pmax" "=?" "[" Path Filter? "]" -> Property {cons("ProbAtMost")} + + "S" "<" Expression "[" Formula ("{" Formula "}")? "]" -> Property {cons("SteadyLt")} + "S" "<=" Expression "[" Formula ("{" Formula "}")? "]" -> Property {cons("SteadyLtEq")} + "S" ">" Expression "[" Formula ("{" Formula "}")? "]" -> Property {cons("SteadyGt")} + "S" ">=" Expression "[" Formula ("{" Formula "}")? "]" -> Property {cons("SteadyGtEq")} + "S" "=?" "[" Formula ("{" Formula "}")? "]" -> Property {cons("SteadyEq")} + + "R" "<" Expression "[" Reward Filter? "]" -> Property {cons("RewardLt")} + "R" "<=" Expression "[" Reward Filter? "]" -> Property {cons("RewardLtEq")} + "R" ">" Expression "[" Reward Filter? "]" -> Property {cons("RewardGt")} + "R" ">=" Expression "[" Reward Filter? "]" -> Property {cons("RewardGtEq")} + "R" "=?" "[" Reward Filter? "]" -> Property {cons("RewardEq")} + "R" "min" "=?" "[" Reward Filter? "]" -> Property {cons("RewardAtLeast")} + "Rmin" "=?" "[" Reward Filter? "]" -> Property {cons("RewardAtLeast")} + "R" "max" "=?" "[" Reward Filter? "]" -> Property {cons("RewardAtMost")} + "Rmax" "=?" "[" Reward Filter? "]" -> Property {cons("RewardAtMost")} + + "\"init\"" -> Property {cons("Init")} + "\"" Identifier "\"" -> Property {cons("Label")} + Expression -> Property + "(" Property ")" -> Property {bracket} + + %% FIXME: Some priorities are probably missing here + context-free priorities + { + Property "=>" Property -> Property + } + > { + Property "|" Property -> Property + } + > { + Property "&" Property -> Property + } + > { + "!" Property -> Property + } + > { + Expression -> Property + } + + %% FIXME: This looks a bit weird... + context-free priorities + { + "(" Formula ")" -> Formula + } + > { + "(" Property ")" -> Property + } Index: src/syn/pctl/PCTL-Reward.sdf --- src/syn/pctl/PCTL-Reward.sdf (revision 0) +++ src/syn/pctl/PCTL-Reward.sdf (revision 0) @@ -0,0 +1,19 @@ +module PCTL-Reward +imports + PRISM-Expression +exports + + %% EBNF Grammar: Rewards in PCTL + %% + %% Reward ::= + %% "C" "<=" Expression + %% | "I" "=" Expression + %% | "F" Formula + %% | "S" + + sorts Reward + context-free syntax + "C" "<=" Expression -> Reward {cons("Cumul")} + "I" "=" Expression -> Reward {cons("Inst")} + "F" Formula -> Reward {cons("Reach")} + "S" -> Reward {cons("Steady")} Index: src/syn/pctl/PCTL-Filter.sdf --- src/syn/pctl/PCTL-Filter.sdf (revision 0) +++ src/syn/pctl/PCTL-Filter.sdf (revision 0) @@ -0,0 +1,17 @@ +module PCTL-Filter +imports + PCTL-Formula +exports + + %% EBNF Grammar: PCTL Filters + %% + %% Filter ::= + %% "{" Formula "}" {FilterMinMax} + %% | "{" "min" "}" + %% | "{" "max" "}" + + sorts Filter FilterMinMax + context-free syntax + "{" Formula "}" FilterMinMax* -> Filter {cons("Filter")} + "{" "min" "}" -> FilterMinMax {bracket,cons("ComputeMin")} + "{" "max" "}" -> FilterMinMax {bracket,cons("ComputeMax")} Index: src/syn/pctl/PCTL-Formula.sdf --- src/syn/pctl/PCTL-Formula.sdf (revision 0) +++ src/syn/pctl/PCTL-Formula.sdf (revision 0) @@ -0,0 +1,24 @@ +module PCTL-Formula +imports + PCTL-Property +exports + + %% EBNF Grammar: PCTL Formulas in our parser + %% + %% Formula ::= + %% Property + %% | "(" Formula ")" + + %% EBNF Grammar: PCTL Formulas as in PRISM's parser + %% + %% SinglePCTLFormula ::= PCTLFormula + %% + %% PCTLFormula ::= PCTLImplies + %% + %% PCTLImplies ::= PCTLOr ["=>" PCTLOr] + %% + + sorts Formula + context-free syntax + Property -> Formula {cons("Formula")} + "(" Formula ")" -> Formula {bracket} Index: src/syn/pctl/PCTL-StartSymbols.sdf --- src/syn/pctl/PCTL-StartSymbols.sdf (revision 0) +++ src/syn/pctl/PCTL-StartSymbols.sdf (revision 0) @@ -0,0 +1,17 @@ +%% Multiple start symbols for convenience +%% This is because, unfortunately, start symbol selection happens *after* +%% parsing in sglr. So first all the alternatives are parsed, and then +%% the selected start symbol is chosen. +module PCTL-StartSymbols +imports + PCTL-Main + +exports + context-free start-symbols + PropertiesFile + Expression + LabelDef + ConstantDef + Formula + Property + Path Index: src/syn/pctl/StrategoPCTL.sdf --- src/syn/pctl/StrategoPCTL.sdf (revision 0) +++ src/syn/pctl/StrategoPCTL.sdf (revision 0) @@ -0,0 +1,26 @@ +module StrategoPCTL +imports + StrategoRenamed + PCTL + PCTL-MetaVars + PCTL-MetaCongruences + +exports + context-free start-symbols StrategoModule + + context-free syntax + + "|[" LabelDef "]|" -> StrategoTerm {prefer,cons("ToTerm")} + "|[" ConstantDef "]|" -> StrategoTerm {prefer,cons("ToTerm")} + "|[" Formula "]|" -> StrategoTerm {prefer,cons("ToTerm")} + "|[" Property "]|" -> StrategoTerm {prefer,cons("ToTerm")} + "|[" Label "]|" -> StrategoTerm {prefer,cons("ToTerm")} + "|[" Path "]|" -> StrategoTerm {prefer,cons("ToTerm")} + "|[" Reward "]|" -> StrategoTerm {prefer,cons("ToTerm")} + "|[" Filter "]|" -> StrategoTerm {prefer,cons("ToTerm")} + + context-free syntax + + "~" StrategoTerm -> Expression {prefer,cons("FromTerm")} + "~id:" StrategoTerm -> ID {prefer,cons("FromTerm")} + "~label:" StrategoTerm -> Label {prefer,cons("FromTerm")} Index: src/syn/pctl/PCTL-Path.sdf --- src/syn/pctl/PCTL-Path.sdf (revision 0) +++ src/syn/pctl/PCTL-Path.sdf (revision 0) @@ -0,0 +1,23 @@ +module PCTL-Path +imports + PRISM-Expression + PCTL-Formula +exports + + %% EBNF Grammar: PCTL Paths + %% + %% Path ::= + %% "X" Formula + %% | Formula "U" "<=" Expression Formula + %% | Formula "U" ">=" Expression Formula + %% | Formula "U" "[" Expression "," Expression "]" Formula + %% | Formula "U" Formula + + sorts Path + context-free syntax + "X" Formula -> Path {cons("Next")} + Formula "U" "<=" Expression Formula -> Path {cons("BoundedUntilLtEq")} + Formula "U" ">=" Expression Formula -> Path {cons("BoundedUntilGtEq")} + Formula "U" "[" Expression "," Expression "]" Formula + -> Path {cons("BoundedUntilRange")} + Formula "U" Formula -> Path {cons("Until")} Index: src/syn/pctl/PCTL-PropertiesFile.sdf --- src/syn/pctl/PCTL-PropertiesFile.sdf (revision 0) +++ src/syn/pctl/PCTL-PropertiesFile.sdf (revision 0) @@ -0,0 +1,22 @@ +module PCTL-PropertiesFile +imports + PCTL-Label + PRISM-Constant + PCTL-Formula + +exports + + %% EBNF Grammar: PCTL top level stuff + %% + %% PropertiesFile ::= + %% {LabelDef} + %% | {ConstantDef} + %% | {SinglePCTLFormula} + + sorts PropertiesFile PropertiesFileSection + context-free syntax + PropertiesFileSection* -> PropertiesFile {cons("PropertiesFile")} + + LabelDef -> PropertiesFileSection + ConstantDef -> PropertiesFileSection + Formula -> PropertiesFileSection Index: src/syn/pctl/Makefile.am --- src/syn/pctl/Makefile.am (revision 0) +++ src/syn/pctl/Makefile.am (revision 0) @@ -0,0 +1,65 @@ +## +## Makefile.am for xrm in /home/tsuna/work/xrm/trunk/src/syn/pctl +## +## Made by SIGOURE Benoit +## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; +## +## Started on Sat Jun 10 00:17:31 2006 SIGOURE Benoit +## Last update Sat Jun 10 00:36:56 2006 SIGOURE Benoit +## + +include $(top_srcdir)/config/Transformers.mk +-include $(wildcard *.dep) + +PGEN_FLAGS = -m $* +SDF2RTG_FLAGS = -m $* +SCFLAGS = -O 2 +STRINCLUDES = -I $(srcdir) +SDFINCLUDES = -I $(srcdir) \ + -I $(STRATEGO_FRONT)/share/sdf/stratego-front \ + -I $(top_srcdir)/src/syn/prism + +pkgdata_DATA_built = \ + PCTL.def \ + PCTL.tbl \ + PCTL.rtg \ + PCTL.str \ + PCTL-StartSymbols.tbl \ + PCTL-Prefixed.def \ + StrategoPCTL.def \ + StrategoPCTL.tbl + +pkgdata_DATA = $(pkgdata_DATA_built) +sdfdata_DATA = $(pkgdata_DATA_built) +nobase_sdfdata_DATA = PCTL-Prefixed.sdf $(SDFS) + +CLEANFILES = $(pkgdata_DATA_built) \ + $(wildcard *.dep) \ + PCTL.{c,str,c.dep} \ + PCTL-StartSymbols.def \ + PCTL-Prefixed.def + +SDFS = \ + PCTL-Filter.sdf \ + PCTL-Formula.sdf \ + PCTL-Label.sdf \ + PCTL-Main.sdf \ + PCTL-Path.sdf \ + PCTL-PropertiesFile.sdf \ + PCTL-Property.sdf \ + PCTL-Reward.sdf \ + PCTL-StartSymbols.sdf \ + PCTL.sdf + +EXTRA_DIST = $(SDFS) + +PCTL.def: $(SDFS) +PCTL-StartSymbols.def: $(SDFS) + +StrategoPCTL.def: StrategoPCTL.sdf \ + PCTL-MetaVars.sdf \ + PCTL-MetaCongruences.sdf + +PCTL-Prefixed.sdf: PCTL.def + $(SDF_TOOLS)/bin/gen-renamed-sdf-module -i $< -o $@ \ + --main PCTL --name PCTL-Prefixed --prefix PCTL Index: src/syn/pctl/PCTL-Label.sdf --- src/syn/pctl/PCTL-Label.sdf (revision 0) +++ src/syn/pctl/PCTL-Label.sdf (working copy) @@ -1,13 +1,10 @@ -module PRISM-Label +module PCTL-Label imports PRISM-Expression PRISM-Identifier exports - %% NOTE: Labels are used in properties files which we don't need to support - %% at this time. - %% EBNF Grammar: Labels %% LabelDef ::= "label" "\"" Identifier "\"" "=" Expression ";" Index: src/syn/pctl/PCTL-MetaCongruences.sdf --- src/syn/pctl/PCTL-MetaCongruences.sdf (revision 0) +++ src/syn/pctl/PCTL-MetaCongruences.sdf (revision 0) @@ -0,0 +1,12 @@ +module PCTL-MetaCongruences +exports + + context-free syntax + "|[" LabelDef "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} + "|[" ConstantDef "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} + "|[" Formula "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} + "|[" Property "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} + "|[" Label "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} + "|[" Path "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} + "|[" Reward "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} + "|[" Filter "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} Index: src/syn/pctl/PCTL-MetaVars.sdf --- src/syn/pctl/PCTL-MetaVars.sdf (revision 0) +++ src/syn/pctl/PCTL-MetaVars.sdf (revision 0) @@ -0,0 +1,11 @@ +module PCTL-MetaVars +exports + variables + [ijkln][0-9]* -> LInt {prefer} + [dr][0-9]* -> LDouble {prefer} + [xyzfgh][0-9]* -> ID {prefer} + [e][0-9]* -> Expression {prefer} + [F][0-9]* -> Formula {prefer} + [p][0-9]* -> Path {prefer} + [t][0-9]* -> Filter {prefer} + [R][0-9]* -> Reward {prefer} Index: src/syn/pctl/PCTL.sdf --- src/syn/pctl/PCTL.sdf (revision 0) +++ src/syn/pctl/PCTL.sdf (revision 0) @@ -0,0 +1,11 @@ +%% Single start symbol for faster parsing +%% This is because, unfortunately, start symbol selection happens *after* +%% parsing in sglr. So first all the alternatives are parsed, and then +%% the selected start symbol is chosen. +module PCTL +imports + PCTL-Main + +exports + context-free start-symbols + PropertiesFile Index: src/syn/Makefile.am --- src/syn/Makefile.am (revision 58) +++ src/syn/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; ## ## Started on Thu Apr 27 17:40:41 2006 SIGOURE Benoit -## Last update Thu May 25 18:44:17 2006 SIGOURE Benoit +## Last update Fri Jun 9 19:16:48 2006 SIGOURE Benoit ## -SUBDIRS = prism xrm +SUBDIRS = prism pctl xrm Index: tests/pctl/man_examples.pctl --- tests/pctl/man_examples.pctl (revision 0) +++ tests/pctl/man_examples.pctl (revision 0) @@ -0,0 +1,96 @@ +P>=1 [ true U terminate ] +// the algorithm eventually terminates successfully with probability 1 + +"init" => P<0.1 [ true U<=100 num_errors > 5 ] +// from an initial state, the probability that more than 5 errors occur within +// the first 100 me units is less than 0.1 + +"down" => P>0.75 [ !"fail" U[1,2] "up" ] +// when a shutdown occurs, the probability of system recovery being completed +// in between and 2 hours without further failures occurring is greater than +// 0.75 + +S<0.01 [ num_sensors < min_sensors ] +// in the long-run, the probability that an inadequate number of sensors are +// operational is less than 0.01 + +P=? [ !proc2_terminate U proc1_terminate ] +// the probability that process 1 terminates before process 2 does + +Pmax=? [ true U<=T messages_lost > 10 ] +// the maximum probability that more than 10 messages have been lost by time T + +S=? [ queue_size / max_size > 0.75 ] +// the long-run probability that the queue is more than 75% full + +P<0.01 [ X y=1 ] +// the probability of the expression y=1 being true in the next state is less +// than 0.01. + +P>0.5 [ true U z=2 ] +// the probability that z is eventually equal to 2 is greater than 0.5 + +P>=0.98 [ true U<=7 y=4 ] +// the probability of y being equal to 4 within 7 time steps is greater than +// or equal to 0.98 + +P>=0.25 [ y<=1 U<=6.5 y>1 ] +P<0.4 [ y<=1 U>=5.5 y>1 ] + +P>0 [ y<=1 U[5.5,6.5] y>1 ] +// the probability that y first exceeds 1 the time interval [5.5, 6.5] is +// greater than zero + +S<0.05 [ queue_size / max_size > 0.75 ] +// the long-run probability of the queue being more than 75% full is less +// than 0.05. + +"init" => P>=1 [ true U leader_elected=true ] + +P=? [ true U x=5&y=5 ] +// returns the probability of, from the initial state, reaching a state +// satisfying x=5&y=5 + +P=? [ true U x=5&y=5 {x=1&y=2} ] +// returns the probability of, from the state (1,2) (i.e. x=1 and y=2), +// reaching a state satisfying x=5&y=5 + +P=? [ true U x=5&y=5 {y=2}{min} ] +P=? [ true U x=5&y=5 {y=2}{max} ] +// return the minimum and maximum probability, respectively, of reaching a +// state satisfying x=5&y=5 from all the states satisfying y=2. In addition, +// PRISM will report the states of the model in which the minimum or maximum +// probability is attained. + +P=? [ true U x=5&y=5 {y=2}{min}{max} ] +// both the minimum and maximum value are computed simultaneously + +P>0.5 [ true U x=5&y=5 {y=2} ] +// will return a Boolean value, depending whether the property is true in all +// states of the model or not, but the probability of path property true U +// x=5&y=5 being satisfied will be displayed for all states where y=2. + +const int k = 7; +const double T = 9.5; +const double p = 0.01; +P<p [ true U<=T x=k ] + +label "safe" = temp<=100 | alarm=true; +label "fail" = temp>100 & alarm=false; +P>=0.99 [ "safe" U "fail" ] + +"init" => P>=0.99 [ "safe" U "fail" ] + +R<=9.5 [ F z=2 ] +// the expected time taken to reach, from s, a state where z equals 2 is less +// than or equal to 9.5 + +R=? [ C<=15.5 ] +// the expected number of lost requests within 15.5 time units of operation. + +R<4.4 [ I=100 ] +// starting from s, the expected queue size exactly 100 time units later is +// less than 4.4 + +R<=0.7 [ S ] +// starting from s, the long-run average power consumption is less than 0.7 Index: tests/test-parse-pctl.sh.in --- tests/test-parse-pctl.sh.in (revision 58) +++ tests/test-parse-pctl.sh.in (working copy) @@ -1,6 +1,6 @@ #!/bin/sh ## -## test-parse-prism.sh for xrm in /home/tsuna/work/xrm/trunk/tests +## test-parse-pctl.sh for xrm in /home/tsuna/work/xrm/trunk/tests ## ## Made by SIGOURE Benoit ## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; @@ -13,9 +13,9 @@ test_pass=0 rm -f failed_tests.$$ -for file in `find "@srcdir@" -name '*.pm' -o -name '*.nm' -o -name '*.sm' | sort`; do +for file in `find "@srcdir@" -name '*.pctl' -o -name '*.csl' | sort`; do echo @ECHO_N@ " Parsing `basename $file` ... " - "@top_builddir@/src/tools/parse-prism" -i "$file" -o /dev/null + "@top_builddir@/src/tools/parse-pctl" -i "$file" -o /dev/null rv=$? test_cnt=$((test_cnt + 1)) if [ $rv -eq 0 ]; then Index: tests/Makefile.am --- tests/Makefile.am (revision 58) +++ tests/Makefile.am (working copy) @@ -5,15 +5,17 @@ ## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; ## ## Started on Thu Apr 27 16:56:50 2006 SIGOURE Benoit -## Last update Thu May 25 17:29:32 2006 SIGOURE Benoit +## Last update Sat Jun 10 05:24:43 2006 SIGOURE Benoit ## #include $(top_srcdir)/config/toplevel.mk dist_check_SCRIPTS = \ test-parse-prism.sh \ + test-parse-pctl.sh \ test-parse-xrm.sh \ test-pp-prism.sh \ + test-pp-pctl.sh \ test-pp-xrm.sh \ test-xrm-front.sh @@ -25,8 +27,10 @@ TESTS_ENVIRONMENT = XTC_REPOSITORY="$(BUILD_REPOSITORY)" TESTS = test-parse-prism.sh \ + test-parse-pctl.sh \ test-parse-xrm.sh \ test-pp-prism.sh \ + test-pp-pctl.sh \ test-pp-xrm.sh \ test-xrm-front.sh \ test-summary.sh Index: tests/test-pp-pctl.sh.in --- tests/test-pp-pctl.sh.in (revision 58) +++ tests/test-pp-pctl.sh.in (working copy) @@ -1,6 +1,6 @@ #!/bin/sh ## -## test-pp-xrm.sh for xrm in /home/tsuna/work/xrm/trunk/tests +## test-pp-pctl.sh for xrm in /home/tsuna/work/xrm/trunk/tests ## ## Made by SIGOURE Benoit ## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; @@ -11,7 +11,7 @@ test_cnt=0 test_pass=0 -target_dir='output-pp-xrm' +target_dir='output-pp-pctl' rm -f failed_tests.$$ test ! -d $target_dir && { mkdir $target_dir \ @@ -21,7 +21,7 @@ outdir="`pwd`" cd .. -for file in `find "@srcdir@" -name '*.pm' -o -name '*.nm' -o -name '*.sm' -o -name '*.xpm' | sort`; do +for file in `find "@srcdir@" -name '*.pctl' -o -name '*.csl' -o -name '*.xpctl' -o -name '*.xcsl' | sort`; do basefile="`basename $file`" bfile="`echo \"$basefile\" | sed 's/\.x\?pm$//'`" @@ -29,7 +29,7 @@ test_cnt=$((test_cnt + 1)) echo @ECHO_N@ " Parsing $basefile ... " - "@top_builddir@/src/tools/parse-xrm" -i "$file" -o "$outdir/$bfile.aterm" + "@top_builddir@/src/tools/parse-pctl" -i "$file" -o "$outdir/$bfile.aterm" if [ $? -ne 0 ]; then echo 'FAILED, continuing with the next test...' echo " * $file: parsing FAILED" >> failed_tests.$$ @@ -38,7 +38,7 @@ echo 'OK, no ambiguities found' echo @ECHO_N@ " Pretty printing $basefile ... " - "@top_builddir@/src/tools/pp-xrm" \ + "@top_builddir@/src/tools/pp-pctl" \ -i "$outdir/$bfile.aterm" -o "$outdir/$bfile.pp.xpm" if [ $? -ne 0 ]; then echo 'FAILED, continuing with the next test...' @@ -48,7 +48,7 @@ echo 'OK' echo @ECHO_N@ " Re-Parsing pretty printed file $basefile ... " - "@top_builddir@/src/tools/parse-xrm" \ + "@top_builddir@/src/tools/parse-pctl" \ -i "$outdir/$bfile.pp.xpm" -o "$outdir/$bfile.pp2aterm" if [ $? -ne 0 ]; then echo 'FAILED, here is the content of the file:' @@ -62,7 +62,7 @@ echo 'OK, no ambiguities found' echo @ECHO_N@ " Re-Pretty printing the re-parsed file $basefile ... " - "@top_builddir@/src/tools/pp-xrm" \ + "@top_builddir@/src/tools/pp-pctl" \ -i "$outdir/$bfile.pp2aterm" -o "$outdir/$bfile.pp2.xpm" if [ $? -ne 0 ]; then echo 'FAILED, continuing with the next test...' Index: configure.ac --- configure.ac (revision 58) +++ configure.ac (working copy) @@ -5,7 +5,7 @@ ## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; ## ## Started on Thu Apr 27 15:55:56 2006 SIGOURE Benoit -## Last update Fri Jun 2 17:52:40 2006 SIGOURE Benoit +## Last update Sat Jun 10 05:25:09 2006 SIGOURE Benoit ## ## --------------- ## @@ -73,12 +73,15 @@ src/Makefile src/syn/Makefile src/syn/prism/Makefile + src/syn/pctl/Makefile src/syn/xrm/Makefile src/sig/Makefile src/str/Makefile src/lib/Makefile src/lib/prism/Makefile src/lib/prism/pp/Makefile + src/lib/pctl/Makefile + src/lib/pctl/pp/Makefile src/lib/xrm/Makefile src/lib/xrm/pp/Makefile src/lib/native/Makefile @@ -90,9 +93,13 @@ [chmod a=rx tests/test-parse-prism.sh]) AC_CONFIG_FILES([tests/test-parse-xrm.sh], [chmod a=rx tests/test-parse-xrm.sh]) +AC_CONFIG_FILES([tests/test-parse-pctl.sh], + [chmod a=rx tests/test-parse-pctl.sh]) AC_CONFIG_FILES([tests/test-pp-prism.sh], [chmod a=rx tests/test-pp-prism.sh]) +AC_CONFIG_FILES([tests/test-pp-pctl.sh], + [chmod a=rx tests/test-pp-pctl.sh]) AC_CONFIG_FILES([tests/test-pp-xrm.sh], [chmod a=rx tests/test-pp-xrm.sh]) Index: TODO --- TODO (revision 58) +++ TODO (working copy) @@ -124,6 +124,55 @@ [] x=3 -> ... // x=3 is impossible [] x=0 -> (x'=3) // x=3 is not in the definition range of x + ## ------------- ## + ## Optimizations ## + ## ------------- ## + + * If there are some optimization(s) available in xrm-front add a -O option + to enable them (and thus, leave them off by default). If there is more + than one level of optimization, try to add different optimization levels + (pretty much like in GCC): + -O 0 = no optimizations + -O 1 = little optimizations -or- safe optimizations + -O 2 = many optimizations -or- include rarely unsafe optimizations + -O 3 = all optimizations -or- include unsafe optimizations + + * Group variable declarations (Idea from Micha). Goal: reduce the size of the + output file by grouping declarations. When several modules declare the same + variable (such as var[i]) the same way, declarations could be grouped + together and then multiplied using variable renaming. This also seems to + produce more optimized C source (to be confirmed). + for i from 0 to 2 do => module test_0 + module test[i] => // code using a_0, b_0 + a[i]: [0..1] init 0; => endmodule + b[i]: [0..1] init 0; => module test_1 + if i = 2 then => // code using a_1. b_1 + d[i]: [0..1] init 0; => endmodule + end => module test_2 + // code => d_2: [0..1] init 0; + endmodule => // code using a_2, b_2, d_2 + end => endmodule + => module __vars_0 + => a_0: [0..1] init 0; + => b_0: [0..1] init 0; + => endmodule + => module __vars_1 + => = __vars_0 [a_0=a_1, b_0=b_1] + => endmodule + => module __vars_2 + => = __vars_0 [a_0=a_2, b_0=b_2] + => endmodule + With many definitions this can save quite a lot of space because variable + renaming is shorter than copying definitions over and over. + How to do this? Do we do this (partially?) before loops are unrolled? Or + do we do it at the very end of the pipeline (which implies that we have to + collect declarations, see which declarations could go together etc... + seems to be quite a mess since doing this sounds like recovering + information lost when unrolling loops). + Should we try to spot potential redundant declarations when unrolling + loops and then later try to group them? Would there be cases where + grouping gets tricky? What about d_2 above? + ## ----- ## ## Notes ## ## ----- ##