June 2006 - Projects

XRM 59: Add (buggy) support for PCTL/CSL formulas.
by SIGOURE Benoit 10 Jun '06

10 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> 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 <martin(a)cs.uu.nl> -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 <martin(a)cs.uu.nl> -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", "sigoure.benoit(a)lrde.epita.fr")) Index: src/tools/Makefile.am --- src/tools/Makefile.am (revision 58) +++ src/tools/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## 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 <sigoure.benoit(a)lrde.epita.fr> ## ## 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", "sigoure.benoit(a)lrde.epita.fr")) + , GNU_GPL("2006", "SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr>") + , 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 <sigoure.benoit(a)lrde.epita.fr> +## +## 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 <sigoure.benoit(a)lrde.epita.fr> +## +## 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 <sigoure.benoit(a)lrde.epita.fr> ## ## 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 <sigoure.benoit(a)lrde.epita.fr> +## +## 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 <sigoure.benoit(a)lrde.epita.fr> ## ## 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 <sigoure.benoit(a)lrde.epita.fr> @@ -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 <sigoure.benoit(a)lrde.epita.fr> ## ## 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 <sigoure.benoit(a)lrde.epita.fr> @@ -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 <sigoure.benoit(a)lrde.epita.fr> ## ## 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 ## ## ----- ##

1 0

XRM 58: Add ConstantDef in concrete syntax.
by SIGOURE Benoit 10 Jun '06

10 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Add ConstantDef in concrete syntax. * src/syn/prism/PRISM-ModulesFile.sdf: Remove useless comment. * src/syn/prism/StrategoPRISM.sdf: Add ConstantDef in concrete syntax. PRISM-ModulesFile.sdf | 6 ------ StrategoPRISM.sdf | 1 + 2 files changed, 1 insertion(+), 6 deletions(-) Index: src/syn/prism/PRISM-ModulesFile.sdf --- src/syn/prism/PRISM-ModulesFile.sdf (revision 57) +++ src/syn/prism/PRISM-ModulesFile.sdf (working copy) @@ -37,9 +37,3 @@ SystemComp -> ModulesFileSection RewardStruct -> ModulesFileSection Init -> ModulesFileSection - -%% At this time we don't need to be able to parse property files... - -%% LabelDef* -> PropertiesFile {cons("PropertiesFile")} -%% ConstantDef* -> PropertiesFile {cons("PropertiesFile")} -%% SinglePCTLFormula* -> PropertiesFile {cons("PropertiesFile")} Index: src/syn/prism/StrategoPRISM.sdf --- src/syn/prism/StrategoPRISM.sdf (revision 57) +++ src/syn/prism/StrategoPRISM.sdf (working copy) @@ -15,6 +15,7 @@ "|[" Expression "]|" -> StrategoTerm {prefer,cons("ToTerm")} "|[" Declaration "]|" -> StrategoTerm {prefer,cons("ToTerm")} "|[" Command "]|" -> StrategoTerm {prefer,cons("ToTerm")} + "|[" ConstantDef "]|" -> StrategoTerm {prefer,cons("ToTerm")} context-free syntax

1 0

XRM 57: Fix boxing of meta-if at Expression level.
by SIGOURE Benoit 10 Jun '06

10 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Fix boxing of meta-if at Expression level. The new test fails because of an ambiguity. This ambiguity is a bit tricky and (IMHO) must be resolved at the grammar level. Basically we have: test1 ? test1-true : test2 ? test2-true : test2-false The ambiguity is: (test1 ? test1-true : test2) ? test2-true : test2-false -or- test1 ? test1-true : (test2 ? test2-true : test2-false) The second choice seems more natural and that's how it works in C. Obviously we can't keep this ambiguity in the grammar. * tests/xrm/amb-if-exp.xpm: New. * src/lib/xrm/pp/xrm-meta-if.str: Fix boxing of meta-if. src/lib/xrm/pp/xrm-meta-if.str | 29 +++++++++++++++++++++++++++++ tests/xrm/amb-if-exp.xpm | 14 ++++++++++++++ 2 files changed, 43 insertions(+) Index: tests/xrm/amb-if-exp.xpm --- tests/xrm/amb-if-exp.xpm (revision 0) +++ tests/xrm/amb-if-exp.xpm (revision 0) @@ -0,0 +1,14 @@ +for y from 0 to height - 1 do + module sensor + [] true -> (s'=test1 ? test1-true : test2 ? test2-true : test2-false); + endmodule +end + +// amb + +//bad: +// (test1 ? test1-true : test2) ? test2-true : test2-false + +//good: +// test1 ? test1-true : (test2 ? test2-true : test2-false) +//at least that's how it works in C and it feels more natural. Index: src/lib/xrm/pp/xrm-meta-if.str --- src/lib/xrm/pp/xrm-meta-if.str (revision 56) +++ src/lib/xrm/pp/xrm-meta-if.str (working copy) @@ -2,11 +2,16 @@ rules + /* Boxing for if statements at top level or inside modules. + * Their then-part and else-part are lists. + */ + prism-to-box: MetaIf(condition, then-part) -> V[ V is=2 [ H hs=1 [ KW["if"] ~condition KW["then"] ] ~*then-part ] KW["end"]] + where <is-list> then-part prism-to-box: MetaIf(condition, then-part, else-part) @@ -14,3 +19,27 @@ ~*then-part ] V is=2 [ KW["else"] ~*else-part ] KW["end"]] + where <is-list> then-part + ; <is-list> else-part + + /* Boxing for if statements at the Expression level. + * Their then-part and else-part are not list but instead simple elements. + * This is due to the fact that the language as no way to express + * statements nor expression sequences at Expression level. + */ + + prism-to-box: + MetaIf(condition, then-part) + -> V[ V is=2 [ H hs=1 [ KW["if"] ~condition KW["then"] ] + ~then-part ] + KW["end"]] + where <not(is-list)> then-part + + prism-to-box: + MetaIf(condition, then-part, else-part) + -> V[ V is=2 [ H hs=1 [ KW["if"] ~condition KW["then"] ] + ~then-part ] + V is=2 [ KW["else"] ~else-part ] + KW["end"]] + where <not(is-list)> then-part + ; <not(is-list)> else-part

1 0

XRM 56: Minor cleanups in the grammar.
by SIGOURE Benoit 10 Jun '06

10 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Minor cleanups in the grammar. * src/syn/prism/PRISM-MetaCongruences.sdf: Add ConstantDef in concrete syntax. * src/syn/prism/PRISM-Main.sdf: Remove useless imports. * src/syn/prism/PRISM-StartSymbols.sdf: Remove useless start symbol (Identifier). * src/syn/xrm/XRM-StartSymbols.sdf: Ditto. * src/syn/prism/Makefile.am: Don't generate .pp tables (they're not used anyway). Don't use PRISM-Label (in fact, this is for PCTL). * src/syn/xrm/Makefile.am: Ditto. prism/Makefile.am | 5 +---- prism/PRISM-Main.sdf | 16 ---------------- prism/PRISM-MetaCongruences.sdf | 1 + prism/PRISM-StartSymbols.sdf | 1 - xrm/Makefile.am | 4 +--- xrm/XRM-StartSymbols.sdf | 1 - 6 files changed, 3 insertions(+), 25 deletions(-) Index: src/syn/prism/PRISM-MetaCongruences.sdf --- src/syn/prism/PRISM-MetaCongruences.sdf (revision 55) +++ src/syn/prism/PRISM-MetaCongruences.sdf (working copy) @@ -7,3 +7,4 @@ "|[" Expression "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} "|[" Declaration "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} "|[" Command "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} + "|[" ConstantDef "]|" -> StrategoStrategy {prefer,cons("ToStrategy")} Index: src/syn/prism/PRISM-Main.sdf --- src/syn/prism/PRISM-Main.sdf (revision 55) +++ src/syn/prism/PRISM-Main.sdf (working copy) @@ -1,20 +1,4 @@ module PRISM-Main imports - PRISM-Command - PRISM-Constant - PRISM-Declaration - PRISM-Expression - PRISM-Formula - PRISM-Global - PRISM-Identifier - PRISM-Init - PRISM-Label PRISM-Layout - PRISM-Literals - PRISM-Module PRISM-ModulesFile - PRISM-ModulesFileType - PRISM-Reward - PRISM-SystemComposition - PRISM-Update - Index: src/syn/prism/PRISM-StartSymbols.sdf --- src/syn/prism/PRISM-StartSymbols.sdf (revision 55) +++ src/syn/prism/PRISM-StartSymbols.sdf (working copy) @@ -13,7 +13,6 @@ Command Expression Updates - Identifier SystemComp RewardStruct ModulesFileSection Index: src/syn/prism/Makefile.am --- src/syn/prism/Makefile.am (revision 55) +++ src/syn/prism/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Thu Apr 27 17:40:41 2006 SIGOURE Benoit -## Last update Fri May 26 02:12:29 2006 SIGOURE Benoit +## Last update Sat Jun 10 00:22:28 2006 SIGOURE Benoit ## include $(top_srcdir)/config/Transformers.mk @@ -20,8 +20,6 @@ pkgdata_DATA_built = \ PRISM.def \ PRISM.tbl \ - PRISM.pp \ - PRISM.pp.af \ PRISM.rtg \ PRISM.str \ PRISM-StartSymbols.tbl \ @@ -49,7 +47,6 @@ PRISM-Identifier.sdf \ PRISM-Init.sdf \ PRISM-Keywords.sdf \ - PRISM-Label.sdf \ PRISM-Layout.sdf \ PRISM-Literals.sdf \ PRISM-Main.sdf \ Index: src/syn/xrm/Makefile.am --- src/syn/xrm/Makefile.am (revision 55) +++ src/syn/xrm/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail <sigoure.benoit(a)lrde.epita.fr> ## ## Started on Thu Apr 27 17:40:41 2006 SIGOURE Benoit -## Last update Fri May 26 02:12:42 2006 SIGOURE Benoit +## Last update Sat Jun 10 00:20:27 2006 SIGOURE Benoit ## include $(top_srcdir)/config/Transformers.mk @@ -22,8 +22,6 @@ pkgdata_DATA_built = \ XRM.def \ XRM.tbl \ - XRM.pp \ - XRM.pp.af \ XRM.rtg \ XRM.str \ XRM-StartSymbols.tbl \ Index: src/syn/xrm/XRM-StartSymbols.sdf --- src/syn/xrm/XRM-StartSymbols.sdf (revision 55) +++ src/syn/xrm/XRM-StartSymbols.sdf (working copy) @@ -13,7 +13,6 @@ Command Expression Updates - Identifier SystemComp RewardStruct ModulesFileSection

1 0

Re: test
by Tsuna 08 Jun '06

08 Jun '06

On 2006-06-08, SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> wrote: > test > Pour une raison qui m'échappe, mes commits ne parviennent plus sur lrde.proj (XRM 49 à XRM 54) oO -- SIGOURE Benoit aka Tsuna _____ /EPITA\ Promo 2008.CSI Rock & tRoll

1 0

XRM 55: Add documentation draft for XRM.
by SIGOURE Benoit 08 Jun '06

08 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Add documentation draft for XRM. * src/str/desugar-array-access.str: Add an ICE condition. * tests/xrm/static_rand.xpm: New. * TODO: Bring up to date. * doc: New. * doc/user-guide.txt: New. TODO | 16 - doc/user-guide.txt | 392 +++++++++++++++++++++++++++++++++++++++ src/str/desugar-array-access.str | 7 tests/xrm/static_rand.xpm | 1 4 files changed, 398 insertions(+), 18 deletions(-) Index: src/str/desugar-array-access.str --- src/str/desugar-array-access.str (revision 54) +++ src/str/desugar-array-access.str (working copy) @@ -35,17 +35,12 @@ ** NOTE: we have a 2D list. The first level of lists represents the ** dimension, the second level, the subscripts accessed for that ** dimension. - ** NOTE: If the subscripts contain at least one meta-var, we completely - ** discard this array-access (by failing) and let the eval-meta-code - ** part take care of it. This is a *dirty* hack to allow declarations - ** using meta-vars. This implies that it's impossible to declare - ** something only partially using meta-vars. :| */ desugar-subscripts = collect-all(?ArrayAccess(_, <id>), conc) // collect gives us the list... ; reverse // ... with deepest array accesses first (we want the opposite) ; prism-desugar - ; if has-meta-vars then fail end // see the 2nd NOTE above. + ; if has-meta-vars then ice(|"desugar-subscripts", "shouldn't be here") end ; map( // traverse the list of dimensions map( // traverse the subscripts for a given dimension if ?Int(_) then Index: tests/xrm/static_rand.xpm --- tests/xrm/static_rand.xpm (revision 0) +++ tests/xrm/static_rand.xpm (revision 0) @@ -0,0 +1 @@ +const int N = static_rand(0, 100); Index: TODO --- TODO (revision 54) +++ TODO (working copy) @@ -13,8 +13,6 @@ * Add tests using "system ... endsystem" (it's properly not parsed atm) - * Write some sort of formal descriptions of the extensions offered. - * Add more tests. Add tests which actually do check that the generated code is correct (which is not done ATM). Factorize current tests with shell functions. @@ -63,8 +61,6 @@ x[1..3]?=0 => x_1=0 | x_2=0 | x_3=0 - NOTE: x[5]?=0 should be considered as an error. - * Add non-static array accesses (as suggested by Micha). For instance: module test x[4] : [0..5]; @@ -145,14 +141,7 @@ ## Documentation ## ## ------------- ## - * Document the return values of xrm-front. - - 1: rewriting failed - - 2: error with meta-vars (eg: undefined meta-var, redefined meta-var) - - 3: arithmetic error when evaluating code (eg: division/modulo by 0) - - 4: invalid call to a builtin (eg rand(1,2,3)) - - 5: invalid array access (eg: subscript is not a positive integer) - - 42: internal compiler error - - 51: not yet implemented + see in the doc/ folder. ## ---- ## ## DONE ## @@ -224,3 +213,6 @@ * Add a sanity check before check-meta-vars to collect all statically declared variables (globals, formulas, local declarations etc.) and ensure (in check-meta-vars) that their identifiers are unique. + + * Write some sort of formal descriptions of the extensions offered. + => see under /doc Index: doc/user-guide.txt --- doc/user-guide.txt (revision 0) +++ doc/user-guide.txt (revision 0) @@ -0,0 +1,392 @@ + ooooooo ooooo ooooooooo. ooo ooooo + `8888 d8' `888 `Y88. `88. .888' + Y888..8P 888 .d88' 888b d'888 + `8888' 888ooo88P' 8 Y88. .P 888 + .8PY888. 888`88b. 8 `888' 888 + d8' `888b 888 `88b. 8 Y 888 + o888o o88888o o888o o888o o8o o888o + eXtended Reactive Modules + + ~ Users' Guide ~ + // FIXME: LaTeXise me + + **************** + * Introduction * + **************** + + // FIXME: An introduction about PRISM and what is/isn't XRM is missing + // here. + + **************** + * Installation * + **************** + + - Requirements: + o Stratego/XT 0.17M1 (at least revision 15278 committed Mon, 29 May 2006) + because of libstratego-gpp (added in Stratego/XT 0.17M1 rev 15278). + o Any version of gcc (3.x or 4.x will do). + o Machine with executable stack (Beware of problems with MacIntel). + o ATerm 2.4.2 or newer. + o SDF2-Bundle 2.3.4 or newer. + + - Using Nix: + Nix is a package management system that ensures safe and complete + installation of packages. + You can get Nix from http://www.cs.uu.nl/wiki/Trace/Nix (pick up the + latest unstable release). + Once Nix is installed, use the following commands (you might need to be + root depending on how you installed nix): + $ nix-channel --add http://nix.cs.uu.nl/dist/stratego/channels-v3/strategoxt-unstable + $ nix-env --install aterm sdf2-bundle strategoxt + There you are! + Add the following line to your .bashrc/.zshrc: + [ -r /nix/etc/profile.d/nix.sh ] && source /nix/etc/profile.d/nix.sh + That's it! + + - Without Nix: + Install ATerm, SDF2 Bundle and Stratego/XT from: + http://www.stratego-language.org/Stratego/ContinuousDistribution + Additional install instructions can be found there. + + - Installing XRM: + o Uncompress the tarball: gunzip -c xrm-version.tar.gz | tar -xf - + o Use the following command to setup a build-tree: + $ cd xrm-version && mkdir _build && cd _build + o Invoke configure to generate the Makefiles + If you use Nix, simply use `../configure' + If you don't use Nix, use `PKG_CONFIG_PATH=P ../configure' where + `P' stands for the path(s) to the directory(ies) where the .pc + files of your Stratego/XT installation were installed. eg: + /usr/lib/pkgconfig/aterm.pc + /usr/lib/pkgconfig/sdf2-bundle.pc + /usr/lib/pkgconfig/stratego*.pc + o Then simply type `make all check' then `make install' + + *************************** + * Tools provided with XRM * + *************************** + + - xrm-front: The front-end provided by XRM will take as input an XRM source + code and will transform it into a standard PRISM source code. + - parse-prism: Parse a PRISM source code and yield an AST in ATerms. + - parse-xrm: Ditto with XRM source code. + - pp-prism: Pretty print ("unparse") a PRISM AST as PRISM source code. + - pp-xrm: Ditto but for XRM. + - prism-to-abox: Transform a PRISM AST into a Box AST for pretty printing. + - xrm-to-abox: Ditto but for XRM. + + ******************* + * Using xrm-front * + ******************* + + xrm-front is the main tool of the XRM package. It will transform a source + written in XRM into a standard PRISM source. + + # Common options + -------------- + The options can be reviewed by invoking xrm-front with the --help argument. + Common options include: + -D | --desugar Desugar the generated PRISM code. + --verbose notice Keep you informed about stages of the pipeline. + -A | --pp-aterm Pretty print output with pp-aterm. + + # Return value + ------------ + xrm-front will return 0 if it succeeds and non zero if an error occured. + Possible return values are: + - 1: rewriting failed (eg: it might be a bug in xrm-front) + - 2: error with meta-vars (eg: undefined meta-var, redefined meta-var) + - 3: arithmetic error when evaluating code (eg: division/modulo by 0) + - 4: invalid call to a builtin (eg rand(1,2,3)) + - 5: invalid array access (eg: subscript is not a positive integer) + - 42: internal compiler error (please send a bug report) + - 51: not yet implemented + + ******************** + * The XRM language * + ******************** + + # Introduction + ------------ + + The specification of the base language is documented in PRISM's manual (a + copy is available in the prism/ directory). + + The XRM language is 100% PRISM compliant and only offers extension to the + language. + + Numerous of the constructs in XRM are `meta' because they cannot be + translated in the PRISM language, thus we must evaluate them at + compile-time (this is xrm-front's job) in order to break them down to + simpler PRISM constructs. + + # XRM Modules + ----------- + + Within XRM modules, it is not mandatory to specify declarations before + commands. They can be freely intertwined in any particular order (whereas + in plain PRISM, declarations must come first and then commands will follow). + The following module is valid in XRM: + + module OutOfOrder + [] x=0 -> (x'=1); + x : [0..1] init 0; + endmodule + + The last step of xrm-front's pipeline is to group all declarations together + at the beginning of the module so that the module will be valid standard + PRISM. + + # XRM Expressions + --------------- + + o XRM has arrays (see below). Array accesses are expressions. + o XRM introduces two operators: "<<" and ">>" which have the same semantics + as in C. They are desugared using calls to the builtin pow. + + TODO: "?=" and "?!=" operators for arrays. + + # XRM Arrays + ---------- + + o It is possible to declare an array of variables instead of a several + variables. Everywhere a variable declaration was allowed in PRISM, an + array declaration is allowed in XRM. + o Arrays can be declared like in C, eg: + x[4] : [0..1] init 0; + will declare an array of 4 elements: x[0], x[1], x[2] and x[3]. + So it's all like in C (access from to 0 through N-1) + o It's possible to declare multidimensional arrays, eg: + x[3][4] : [0..1] init 0; + Again this is *almost* like C with the exception for multidimensional + arrays that intermediate dimensions are not accessible (simply because + they don't exist). So the former declaration will declare: + x[0][0], x[0][1], x[0][2], x[0][3], + x[1][0], x[1][1], x[1][2], x[1][3], + x[2][0], x[2][1], x[2][2], x[2][3] + But in this case accessing x[0] for example doesn't make sense. + o It is also possible to specify manually the dimensions of an array using + lists and ranges, eg: + x[2..4][0,3..5] will declare only: x[2][0], x[2][3], x[2][4], x[2][5], + x[3][0], x[3][3], x[3][4], x[3][5], + x[4][0], x[4][3], x[4][4], x[4][5] + So basically, when one of the dimensions of an array declaration is a + simple integer, eg: x[N] it is expansed in x[0..N]. Then the Cartesian + product of all the dimensions of the array is used to compute the set of + accessible variables. + o Dimensions of size zero are not allowed, eg: x[0] : [0..1]; + o Arrays can also be implicitly declared using for loops (see below, the + section about for loops in XRM). + o Array accesses can be found (nearly) everywhere a simple variable + identifier is allowed in PRISM. + o Update of values in arrays is illustrated in the following example: + [] x[N][M]=0 -> (x[N][M]'=1); + Notice that the prime (') comes after the dimensions of the array access. + o All the subscripts in array accesses must be evaluable down to a simple + positive integer at compile time, eg: + const int N = 3; + // ... + i : [0..42] init 0; // declaration of `i'. + [] x[N+3]=0 -> ...; // valid: N+3 can be worked out at compile time. + [] x[i+3]=0 -> ...; // invalid: the value of `i' is dynamic and unknown + // at compile time. + + TODO: Array accesses with dynamic subscripts. + + # XRM Meta-code + ------------- + + XRM introduces meta-for loops and meta-if statements in the language. + These constructs are said to be `meta' because they are evaluated by + xrm-front and lead to code generation. + + o Meta-for loops can be found in only 2 places within a XRM source file: + * Where we could expect a module declaration. + * Where we could expect a declaration or a command, within a module. + This implies that meta-for loops can only be used to generate modules (or + other file sections, such as formulas, globals, etc.) or commands and + declarations within modules. + o There exists 2 flavors of for loops: + * For loops a la Pascal + * For loops a la Shell + Example: + for i from 0 to 3 do ... end // Pascal-like + for i from 0 to 10 step 2 do ... end // Pascal-like + for i in a, 1+2, N do .. end // Shell-like + In each of these 3 cases, the variable `i' will be considered as a + meta-variable, meaning it will only exists at the meta-level and won't + appear in the final source code. + o For Pascal-like for-loops, the fields `from', `to' and `step' must be + evaluable down to simple integers at compile time. The value of the field + `from' must be less than or equal to that of the field `to'. + o For-loops are unrolled by copying the body of the loop and replacing + every match of the identifier of the meta-var by its successive values. + o For-loops are the only way of declaring a meta-var at the moment. + o For-loops can be used to create new modules. Since each module must have + a unique name, it will have to be suffixed by an array access using a + meta-var, eg: + for i from 1 to 3 do + module dummy[i] + x[i] : [0..1] init 0; + endmodule + end + will generate 3 modules: dummy[1], dummy[2] and dummy[3]. + Of course, since each module has its own unique variables too, the + variables declared in that generated module will also have to be suffixed + by an array access with the meta-var. + In this case though, when `i' gets replaced by its successive values, we + have the following modules: + module dummy[1] + x[1] : [0..1] init 0; // not an array declaration + endmodule + module dummy[2] + x[2] : [0..1] init 0; // ditto + endmodule + module dummy[3] + x[3] : [0..1] init 0; // ditto + endmodule + But fortunately, this will not create 3 times an array called `x'. In + this very special case, the numerical values will not be expansed as + x[0..1] for dummy[1], x[0..2] for dummy[2] and x[0..3] for dummy[3] + because the integer in the array subscript comes from the expansion of a + meta-var and won't be further expanded. + Thus in this case you get 3 different modules, each with their own single + unique variable `x'. + If you wish to provide each module with an array of, say 6 elements, then + do the following: + for i from 1 to 3 do + module dummy[i] + x[i][5] : [0..1] init 0; + endmodule + end + In this case the first dimensions (`i') will first be expansed by the + loop unrolling, which will equip each generated module with its own + unique variable `x' and then the second dimension will be expansed to + 0..5 which will create an array of 6 elements for each generated module. + o Meta-for loops can also be used to declare arrays implicitely: + module ImplicitArray + for i from 0 to 3 do + x[i] : [0..i] init i; + end + endmodule + In this case the module ImplicitArray will have a single array named `x' + of 4 elements. This method offers a greater control on how each element + of the array is declared. + + o Meta-if statements can be found in only 3 places within a XRM source file: + * Where we could expect a module declaration. + * Where we could expect a declaration or a command, within a module. + * Where we would expect an expression. + However the latter case has a restriction that the two formers don't have: + the then-part and the else-part of the if statements cannot contain more + than one expression. + o The syntax for meta-if statements is illustrated in the following example: + if true then + module alwaysGenerated + if 0 = 42 - 21 then + neverGenerated : [0..42] init 0; + else + alwaysGeneratedToo : [0..42] init 0; + end + endmodule + end + o The condition of the meta-if statements must be evaluable at compile + time. It must either be evaluable down to true or false, or down to a + simple integer/double. If that integer/double is 0, the condition will be + false, otherwise it will be true (like in C). Comparison on reals are + done with a precision of 10^-7 which means that if the condition is + reduced down to 0.00000001 (for instance) it will be evaluated as being + false. + + # XRM builtins + ------------ + + XRM introduces two new builtins for generating random numbers: rand and + static_rand. + + o Both rand and static_rand take either one or two arguments which must + be evaluable down to simple integers at compile-time. + If rand or static_rand is called with a single argument, a second + argument (an integer equal to zero) is added. If the single argument + is positive, the zero is added before it, otherwise it's added after + it, eg: + rand(3) will be desugared to rand(0, 3) + rand(-3) will be desugared to rand(-3, 0) + o static_rand(low, hi) will be transformed into a random integer ranging + from `low' to `hi' (included). The random number is obtain with rand(3) + which is seeded with the current UNIX time-stamp when xrm-front starts. + o Calls to static_rand will be evaluated after unrolling of meta-for + loops to ensure that each iteration of the loop gets its own random + number. It will be evaluated earlier if it happens to be used where + a statically evaluable value is required more early in the pipeline + (eg: in meta-if statements' condition, in the fields `from', `to' or + `step' of a meta-for loop, etc.) + o Bear in mind that the random numbers generated by static_rand are + constant from one run to another unless you re-generate the PRISM + source (with xrm-front) each time before running. + o rand(low, hi) will be transformed into a new variable (each call to + rand will generate a new unique variable) which will be controlled by + an external module with a single command: + module testRand => module testRand + x : [0..42] init 0; => x : [0..42] init 0; + [] x=0 -> x'=rand(42); => [] x=0 -> x'=__rand_0; + endmodule => endmodule + => module __rand_0 + => __rand_0 : [0..42]; + => [] true -> 1/43:(__rand_0'=0) + => + 1/43:(__rand_0'=1) + => ... + => + 1/43:(__rand_0'=42); + => endmodule + /!\ This is not a reliable random number generator! + + TODO: The current implementation of rand will be renamed (maybe as + bad_rand or old_rand) and a new reliable implementation will be + provided as a replacement. In this implementation, the random variable + won't be hosted in a foreign module anymore, it will be hosted directly + in the module which called rand. The variable will be updated each time + it's accessed to ensure real random numbers. + + ********************* + * Incoming features * + ********************* + + The following features are not yet implemented (or only partially + implemented or broken). They are ordered in term of the estimated time + needed to successfully implement them. For a complete list of things to be + done please review the TODO file. + - More sanity checks for all declarations at different stages of the + pipeline to ensure that everything is well defined. (variables used have + been declared somewhere etc.) + - Possibility to import another module, eg: import common.pm + - Parameterized formulas. (Pretty much like macro-functions in C) + - Scopes for meta variables (allow redefinitions/shadowing). + - Bound/Type checking (ensure that variables are properly used according to + their type/domain definition). + - Conditional tests on arrays. "?=" and "?!=" operators for arrays. eg: + x[1..3]=0 => x_1=0 & x_2=0 & x_3=0 + x[1..3]?=0 => x_1=0 | x_2=0 | x_3=0 + - Dynamic array accesses, eg: x[i] where `i' is not known at compile-time. + - Array initializations a la C: + x[3] : [0..4] init {0, 1, 2}; + const int array[3] = {0, 1, 2}; + - Better error messages (with the location of error). + + ************** + * Known bugs * + ************** + + - The construct "system ... endsystem" (for system compositions) is broken + at the moment (meaning: using it will result in a parse error). It's + probably a simple problem with the base SDF grammar. I've never seen a + PRISM source using this construct so this has been in the TODO list since + the beginning but with a very low priority. + - Unary operators are allowed in the base language whereas they should not + (because they are not allowed in the original PRISM parser). + - There is nearly no warranty that the generated code will work in PRISM. + Generally speaking, if the input XRM source is correct, the output PRISM + source will also be correct. However, at this stage of the development, + the front-end is still pretty fragile and I am sure it's quite easy to + generate invalid PRISM code without having any error reported by + xrm-front (in this case please report the bug). + What we clearly need to thwart this is: + - Type checking. + - Bound checking. + - Probably many other things. (run make check and see the tests that fail).

1 0

XRM 54: Add RIVF's equivalent in XRM meta-code.
by SIGOURE Benoit 08 Jun '06

08 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Add RIVF's equivalent in XRM meta-code. Usage: xrm-front -i rivf.xpm -o rivf.pm -D -D stands for --desugar (it will add an additional pass after the main pipeline to desugar as much as possible everything and perform constant propagation). This is completely optional. One thing has been omitted here: support for battery_mode=0 (which is basically the same thing but without bothering with b[x][y] and without having to check at every update whether or not we should go in the OFF state because we run out of power). I omitted this for the sake of clarity although it's fairly straightforward to add it (since it's only a matter of commenting out some lines). * tests/xrm/rivf.xpm: New. rivf.xpm | 93 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 93 insertions(+) Index: tests/xrm/rivf.xpm --- tests/xrm/rivf.xpm (revision 0) +++ tests/xrm/rivf.xpm (revision 0) @@ -0,0 +1,93 @@ +probabilistic + +const int width = 10; +const int height = 10; + +// coordinates of the sensors where the alert is first seen. +const int event_x = 5; +const int event_y = 5; + +//const int battery_mode = 1; // 0=no-battery, 1=battery +const int power = 15; +const int length = 1200; +const int lossage = 0; +const int loss = 76; + +const int OFF = 0; +const int SLEEP = 1; +const int SENSE = 2; +const int LISTEN = 3; +const int BROADCAST = 4; +const int MAX_STATE = BROADCAST; + +const int COST_SLEEP = 1; +const int COST_SENSE = 1; +const int COST_LISTEN = 3; +const int COST_BROADCAST = 3; + +module timer + t : [0..268435454] init 0; +endmodule + +for x from 0 to width - 1 do + for y from 0 to height - 1 do + module sensor[x][y] + if lossage != 0 & static_rand(0, 100) < lossage then + s[x][y] : [0..MAX_STATE] init OFF; + else + s[x][y] : [0..MAX_STATE] init SENSE; + end + b[x][y] : [0..power] init power; + + if x = event_x & y = event_y then + // this node is the node broadcasting the alert + // rule 1: SENSE -> BROADCAST + [] s[x][y] = SENSE -> 1:(t'=t+1) & + (b[x][y]'=b[x][y] < COST_SENSE ? 0 : b[x][y]-COST_SENSE) & + (s[x][y]'=0 <= b[x][y] ? BROADCAST : OFF); + // rule 2: BROADCAST -> BROADCAST | OFF if no more battery + [] s[x][y] = BROADCAST -> 1:(t'=t+1) & + (b[x][y]'=b[x][y] < COST_BROADCAST ? 0 : b[x][y]-COST_BROADCAST) & + (s[x][y]'=0 <= b[x][y] ? BROADCAST : OFF); + else // !event + + // rule 1: SENSE -> LISTEN + [] s[x][y] = SENSE -> 1:(t'=t+1) & + (b[x][y]'=b[x][y] < COST_SENSE ? 0 : b[x][y]-COST_SENSE) & + (s[x][y]'=0 <= b[x][y] ? LISTEN : OFF); + + // rule 2: LISTEN -> BROADCAST if neighbors broadcasts | SLEEP + [] s[x][y] = LISTEN -> 1:(t'=t+1) & + (b[x][y]'=b[x][y] < COST_LISTEN ? 0 : b[x][y]-COST_LISTEN) & + (s[x][y]'=b[x][y] < COST_BROADCAST ? 0 : + (if x != 0 then + s[x-1][y]=BROADCAST + else false end + | if x != width - 1 then + s[x+1][y]=BROADCAST + else false end + | if y != 0 then + s[x][y-1]=BROADCAST + else false end + | if y != height - 1 then + s[x][y+1]=BROADCAST + else false end + ? BROADCAST : SLEEP)); + + // rule 3: SLEEP -> SENSE | LISTEN + [] s[x][y] = SLEEP -> 0.5:(t'=t+1) & + (b[x][y]'=b[x][y] < COST_SLEEP ? 0 : b[x][y]-COST_SLEEP) & + (s[x][y]'=0 <= b[x][y] ? SENSE : OFF) + + 0.5:(t'=t+1) & + (b[x][y]'=b[x][y] < COST_LISTEN ? 0 : b[x][y]-COST_LISTEN) & + (s[x][y]'=0 <= b[x][y] ? LISTEN : OFF); + + // rule 4: BROADCAST -> BROADCAST + [] s[x][y] = BROADCAST -> 1:(t'=t+1) & + (b[x][y]'=b[x][y] < COST_BROADCAST ? 0 : b[x][y]-COST_BROADCAST) & + (s[x][y]'=0 <= b[x][y] ? BROADCAST : OFF); + end + + endmodule + end +end

1 0

XRM 53: Add meta-if at Expression level.
by SIGOURE Benoit 08 Jun '06

08 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Add meta-if at Expression level. So basically, it is now possible to have a meta-if statement everywhere we can find an Expression. /!\ NOTE: meta-if statements at Expression level are restricted to one single expressions in the then-part and else-part. eg: if some-condition then exp1 exp2 end is *invalid* at Expression level because neither the base language nor the extended language provide real statements/sequences of expressions. Other improvements: PRISM-If statements (cond ? then-part : else-part) are now evaluated by prism-desugar when possible. It is also possible to reduce the condition of a meta-if statement down to a simple Int(_) or Double(_). If that Int(_) or Double(_) is zero, the condition will evaluate as False() otherwise True() [like in C]. NOTE: for Double(_) all tests are performed with a precision of 10^-7 in other words if 0.000000001 then ... else /*executed*/ end will be false. * src/str/prism-desugar.str: Add EvalIf and LitToBool. * src/str/eval-meta-code.str: Allow if statements to evaluate as integer/real. In this case the behavior is the same as in C: 0 means false and all the other values mean true. * src/str/xrm-front.str: Change a debug message to be a notice. * src/syn/xrm/XRM-Arrays.sdf: Use XRMRange for array subscripts. * src/syn/xrm/XRM-MetaIf.sdf: Add meta-if at the Expression level. Correct EBNF grammar. * src/syn/xrm/XRM-MetaFor.sdf: Remove trailing whitespaces. * src/syn/xrm/XRM-Expression.sdf: Add XRMRange. This basically just a simple range but it has a different priority in the grammar than the original Range from the base grammar. It is used for array subscripts. Actually XRMRange might not be a wise name for this sorts. * tests/xrm/desugar-if.xpm: New. * tests/xrm/if-exp.xpm: New. * tests/xrm/cond-array-access.xpm: New. * tests/xrm/priorities-exp-array-subscript.xpm: New. src/str/eval-meta-code.str | 4 +- src/str/prism-desugar.str | 46 +++++++++++++++++++++++++++ src/str/xrm-front.str | 3 - src/syn/xrm/XRM-Arrays.sdf | 16 ++++----- src/syn/xrm/XRM-Expression.sdf | 27 +++++++++++++++ src/syn/xrm/XRM-MetaIf.sdf | 44 ++++++++++++++++++++++--- tests/xrm/cond-array-access.xpm | 4 ++ tests/xrm/desugar-if.xpm | 15 ++++++++ tests/xrm/if-exp.xpm | 7 ++++ tests/xrm/priorities-exp-array-subscript.xpm | 9 +++++ 10 files changed, 158 insertions(+), 17 deletions(-) Index: src/str/prism-desugar.str --- src/str/prism-desugar.str (revision 52) +++ src/str/prism-desugar.str (working copy) @@ -27,6 +27,7 @@ <+ EvalAnd <+ EvalOr <+ EvalMin <+ EvalMax <+ EvalFloor <+ EvalCeil <+ EvalPow <+ EvalMod <+ (EvalStaticRand; IntToDouble) + <+ EvalIf ) ; topdown(try(SimplifyDoubles <+ TruncateDouble)) @@ -305,6 +306,28 @@ /* ** ## ============= ## +** ## If statements ## +** ## ============= ## +*/ + +rules + + EvalIf: + |[ true ? e1 : e2 ]| -> |[ e1 ]| + + EvalIf: + |[ false ? e1 : e2 ]| -> |[ e2 ]| + + EvalIf: + |[ d ? e1 : e2 ]| -> |[ e1 ]| + where <not(compare(real-eq))>(d, 0) + + EvalIf: + |[ d ? e1 : e2 ]| -> |[ e2 ]| + where <compare(real-eq)>(d, 0) + +/* +** ## ============= ## ** ## Eval Builtins ## ** ## ============= ## ** @@ -348,3 +371,26 @@ else <modS> (i, j) => r end + +/* +** ## =========== ## +** ## Misc. stuff ## +** ## =========== ## +*/ + +rules + + LitToBool: + |[ 0 ]| -> |[ false ]| + + LitToBool: + |[ i ]| -> |[ true ]| + where <not(eq)>(i, "0") + + LitToBool: + |[ d ]| -> |[ false ]| + where <compare(real-eq)>(d, 0) + + LitToBool: + |[ d ]| -> |[ true ]| + where <not(compare(real-eq))>(d, 0) Index: src/str/eval-meta-code.str --- src/str/eval-meta-code.str (revision 52) +++ src/str/eval-meta-code.str (working copy) @@ -23,6 +23,7 @@ imports ice signatures + prism-desugar strategies @@ -38,7 +39,8 @@ ?MetaIf(condition, then-part, else-part) ///*DEBUG*/; say(!" @@@ eval-meta-if: starting:") ///*DEBUG*/; printf(|" condition = ", condition) - ; where(<prism-desugar> condition => condition-value) + ; where(<prism-desugar> condition + ; try(LitToBool) => condition-value) ///*DEBUG*/; printf(|" condition-value = ", condition-value) ; if !condition-value => True() then <eval-meta-code> then-part Index: src/str/xrm-front.str --- src/str/xrm-front.str (revision 52) +++ src/str/xrm-front.str (working copy) @@ -42,10 +42,9 @@ notice-msg(|"transformation pipeline starting") ; where(<set-random-seed> (<time>)) ; xrm-to-prism - ; dbg(|"xrm-to-prism finished") ; if must-desugar then prism-desugar - ; dbg(|"prism-desugar finished") + ; notice-msg(|"prism-desugar finished") end /** list of available options for xrm-front */ Index: src/syn/xrm/XRM-Arrays.sdf --- src/syn/xrm/XRM-Arrays.sdf (revision 52) +++ src/syn/xrm/XRM-Arrays.sdf (working copy) @@ -6,21 +6,21 @@ %% EBNF Grammar: Arrays %% ArrayAccess ::= - %% Identifier "[" Range {"," Range} "]" - %% | ArrayAccess "[" Range {"," Range} "]" + %% Identifier "[" XRMRange {"," XRMRange} "]" + %% | ArrayAccess "[" XRMRange {"," XRMRange} "]" %% %% ArrayAccessPrime ::= - %% Identifier "[" Range {"," Range} "]" "'" - %% | ArrayAccess "[" Range {"," Range} "]" "'" + %% Identifier "[" XRMRange {"," XRMRange} "]" "'" + %% | ArrayAccess "[" XRMRange {"," XRMRange} "]" "'" sorts ArrayAccess context-free syntax - Identifier "[" {Range ","}+ "]" -> ArrayAccess {cons("ArrayAccess")} - ArrayAccess "[" {Range ","}+ "]" -> ArrayAccess {cons("ArrayAccess")} + Identifier "[" {XRMRange ","}+ "]" -> ArrayAccess {cons("ArrayAccess")} + ArrayAccess "[" {XRMRange ","}+ "]" -> ArrayAccess {cons("ArrayAccess")} sorts ArrayAccessPrime context-free syntax - ArrayAccess "[" {Range ","}+ "]" "'" + ArrayAccess "[" {XRMRange ","}+ "]" "'" -> ArrayAccessPrime {cons("ArrayAccessPrime")} - Identifier "[" {Range ","}+ "]" "'" + Identifier "[" {XRMRange ","}+ "]" "'" -> ArrayAccessPrime {cons("ArrayAccessPrime")} Index: src/syn/xrm/XRM-MetaIf.sdf --- src/syn/xrm/XRM-MetaIf.sdf (revision 52) +++ src/syn/xrm/XRM-MetaIf.sdf (working copy) @@ -7,23 +7,37 @@ %% EBNF Grammar: Meta if-then-else %% (* if-then-else at top-level *) %% ModulesFileSection ::= - %% "if" Expression "then" ModulesFileSection {ModulesFileSection} "end" + %% "if" Expression "then" {ModulesFileSection} "end" %% | "if" Expression "then" - %% ModulesFileSection {ModulesFileSection} + %% {ModulesFileSection} %% "else" - %% ModulesFileSection {ModulesFileSection} + %% {ModulesFileSection} %% "end" %% %% (* if-then-else inside modules *) %% DeclarationOrCommand ::= - %% "if" Expression "then" DeclarationOrCommand {DeclarationOrCommand} "end" + %% "if" Expression "then" {DeclarationOrCommand} "end" %% | "if" Expression "then" - %% DeclarationOrCommand {DeclarationOrCommand} + %% {DeclarationOrCommand} %% "else" - %% DeclarationOrCommand {DeclarationOrCommand} + %% {DeclarationOrCommand} + %% "end" + %% + %% (* if-then-else inside expressions *) + %% (* NOTE: it's not possible to have more than 1 exp in the then-part + %% * and else-part of the meta-if statements for expression. This is + %% * because the current base and extended language don't have real + %% * statements nor sequences of expressions. *) + %% Expression ::= + %% "if" Expression "then" Expression "end" + %% | "if" Expression "then" + %% Expression + %% "else" + %% Expression %% "end" context-free syntax + %% if-then at top-level "if" Expression "then" ModulesFileSection* "end" -> ModulesFileSection {cons("MetaIf")} @@ -36,6 +50,7 @@ "end" -> ModulesFileSection {cons("MetaIf")} context-free syntax + %% if-then within modules "if" Expression "then" DeclarationOrCommand* "end" -> DeclarationOrCommand {cons("MetaIf")} @@ -46,3 +61,20 @@ "else" DeclarationOrCommand* "end" -> DeclarationOrCommand {cons("MetaIf")} + + %% NOTE: it's not possible to have more than 1 exp in the then-part + %% and else-part of the meta-if statements for expression. This is + %% because the current base and extended language don't have real + %% statements nor sequences of expressions. + context-free syntax + + %% if-then within expressions + "if" Expression "then" Expression "end" + -> Expression {cons("MetaIf")} + + %% if-then-else within expressions + "if" Expression "then" + Expression + "else" + Expression + "end" -> Expression {cons("MetaIf")} Index: src/syn/xrm/XRM-MetaFor.sdf Index: src/syn/xrm/XRM-Expression.sdf --- src/syn/xrm/XRM-Expression.sdf (revision 52) +++ src/syn/xrm/XRM-Expression.sdf (working copy) @@ -18,6 +18,9 @@ %% (* builtin functions calls using the "func" notation *) %% | "func" "(" "rand" "," Expression {"," Expression} ")" %% | "func" "(" "static_rand" "," Expression {"," Expression} ")" + %% + %% (* Ranges in XRM with different priority (for array accesses) *) + %% XRMRange ::= Expression | Expression ".." Expression context-free syntax ArrayAccess -> Expression @@ -39,6 +42,12 @@ "func" "(" "static_rand" "," {Expression ","}+ ")" -> Expression {cons("StaticRand")} + %% Ranges in XRM with different priority (for array accesses) + sorts XRMRange + context-free syntax + Expression -> XRMRange + Expression ".." Expression -> XRMRange {cons("Range")} + %% NOTE: remember: priorities are transitive in SDF. %% The following priorities are marked either with "inherited" or "new". %% The former means that these priorities are inherited from the base @@ -71,3 +80,21 @@ > { %% inherited Expression -> Range } + > { %% inherited + "!" Expression -> Expression + } + > {left: %% inherited + Expression "&" Expression -> Expression + } + > {left: %% inherited + Expression "|" Expression -> Expression + } + > { %% inherited + Expression "?" Expression ":" Expression -> Expression + } + > {non-assoc: %% new + Expression ".." Expression -> XRMRange + } + > { %% new + Expression -> XRMRange + } Index: tests/xrm/desugar-if.xpm --- tests/xrm/desugar-if.xpm (revision 0) +++ tests/xrm/desugar-if.xpm (revision 0) @@ -0,0 +1,15 @@ +if 0=1?0:2 then + const int success1 = 1; + if 0=1?0:2 then + const int success2 = 1; + if false?0:0 then + const int fail1 = 1; + else + const int success3 = 1; + end + else + const int fail2 = 1; + end +else + const int fail3 = 1; +end Index: tests/xrm/if-exp.xpm --- tests/xrm/if-exp.xpm (revision 0) +++ tests/xrm/if-exp.xpm (revision 0) @@ -0,0 +1,7 @@ +const int N = 3; +const int success = 1; + +module test + x : [if true then 0 end..if false then 0 else 42 end]; + [] x=0 -> x'=if 42 then success else -1 end; +endmodule Index: tests/xrm/cond-array-access.xpm --- tests/xrm/cond-array-access.xpm (revision 0) +++ tests/xrm/cond-array-access.xpm (revision 0) @@ -0,0 +1,4 @@ +module test + x[4] : [0..42] init 0; + [] x[-1<0?0:-1]=0 -> true; +endmodule Index: tests/xrm/priorities-exp-array-subscript.xpm --- tests/xrm/priorities-exp-array-subscript.xpm (revision 0) +++ tests/xrm/priorities-exp-array-subscript.xpm (revision 0) @@ -0,0 +1,9 @@ +module test + x[3] : bool init false; + y : bool init true; + x[4] : [0..42] init 0; + + //[] true -> x[1|1]'=true; + [] x[true?2:3]=0 -> true; + [] true -> x[0..1&1]'=true; +endmodule

1 0

XRM 52: Add -a|--allow-amb option for parse-prism/parse-xrm.
by SIGOURE Benoit 08 Jun '06

08 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Add -a|--allow-amb option for parse-prism/parse-xrm. This can be useful for debugging. * src/tools/parse-xrm.str: Add -a|--allow-amb option. * src/tools/parse-prism.str: Ditto. * src/tools/parser-common.str: Ditto. parse-prism.str | 1 + parse-xrm.str | 1 + parser-common.str | 25 ++++++++++++++++++++++--- 3 files changed, 24 insertions(+), 3 deletions(-) Index: src/tools/parse-xrm.str --- src/tools/parse-xrm.str (revision 51) +++ src/tools/parse-xrm.str (working copy) @@ -22,6 +22,7 @@ + preserve-comments-option + preserve-positions-option + pp-aterm-option + + allow-amb-option strategies Index: src/tools/parse-prism.str --- src/tools/parse-prism.str (revision 51) +++ src/tools/parse-prism.str (working copy) @@ -22,6 +22,7 @@ + preserve-comments-option + preserve-positions-option + pp-aterm-option + + allow-amb-option strategies Index: src/tools/parser-common.str --- src/tools/parser-common.str (revision 51) +++ src/tools/parser-common.str (working copy) @@ -8,13 +8,15 @@ ** -fi: heuristic: injection count ** -fe: heuristic: eagerness ** -2: use AsFix2 output format - ** -A: ambiguities are treated as errors ** -p <file>: parse table to use ** -s <symbol>: start symbol to use + ** Additionnaly pass-amb might add this option: + ** -A: ambiguities are treated as errors */ xtc-sglr-no-heuristics(tbl, sort) = - xtc-transform(!"sglr", !["-fi", "-fe", "-2A", "-p", <tbl; xtc-find> (), - "-s", <sort> () | <pass-v-verbose> ()]) + xtc-transform(!"sglr", !["-fi", "-fe", "-2", "-p", <tbl; xtc-find> (), + "-s", <sort>(), <pass-amb>() + | <pass-v-verbose>()]) strategies @@ -48,6 +50,7 @@ <get-config> "preserve-positions" => "yes" strategies + pp-aterm-option = Option("-A" + "--pp-aterm" , <set-pp-aterm> "yes" @@ -60,6 +63,22 @@ must-pp-aterm = <get-config> "pp-aterm" => "yes" +strategies + + allow-amb-option = + Option("-a" + "--allow-amb" + , <set-allow-amb> "yes" + , !HelpString("-a | --allow-amb", "Allow ambiguities") + ) + + set-allow-amb = + <set-config> ("allow-amb", <id>) + + must-allow-amb = + <get-config> "allow-amb" => "yes" + + pass-amb = if must-allow-amb then !"" else !"-A" end + /** * Documentation */

1 0

XRM 51: Add static constant propagations in static definitions.
by SIGOURE Benoit 08 Jun '06

08 Jun '06

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> Add static constant propagations in static definitions. eg: const int N = 3; const int M = N; // propagation of N in the saved definition for M const int X = M; // ditto => const int X = 3; // and not const int X = N; as it used to be. * src/str/collect-static-const-decl.str: Try to propagate static consts/formulas in the definition of static consts/formulas. * tests/prism/desugar-const.pm: New. src/str/collect-static-const-decl.str | 9 ++++++--- tests/prism/desugar-const.pm | 4 ++++ 2 files changed, 10 insertions(+), 3 deletions(-) Index: src/str/collect-static-const-decl.str --- src/str/collect-static-const-decl.str (revision 50) +++ src/str/collect-static-const-decl.str (working copy) @@ -10,35 +10,38 @@ collect-static-const-decl = ?ConstInt(idf, value) - ; where(!value{Type("int")} => v) ; if <ExpandStaticConsts> idf then cannot-redefine-static-const(|idf) end ; if <ExpandFormulas> idf then cannot-redefine-formula(|idf) end + ; where(<innermost(ExpandStaticConsts + ExpandFormulas)> value => v' + ; !v'{Type("int")} => v) ; rules(ExpandStaticConsts: idf -> v) collect-static-const-decl = ?ConstDouble(idf, value) - ; where(!value{Type("double")} => v) ; if <ExpandStaticConsts> idf then cannot-redefine-static-const(|idf) end ; if <ExpandFormulas> idf then cannot-redefine-formula(|idf) end + ; where(<innermost(ExpandStaticConsts + ExpandFormulas)> value => v' + ; !v'{Type("double")} => v) ; rules(ExpandStaticConsts: idf -> v) collect-static-const-decl = ?ConstBool(idf, value) - ; where(!value{Type("bool")} => v) ; if <ExpandStaticConsts> idf then cannot-redefine-static-const(|idf) end ; if <ExpandFormulas> idf then cannot-redefine-formula(|idf) end + ; where(<innermost(ExpandStaticConsts + ExpandFormulas)> value => v' + ; !v'{Type("bool")} => v) ; rules(ExpandStaticConsts: idf -> v) rules Index: tests/prism/desugar-const.pm --- tests/prism/desugar-const.pm (revision 0) +++ tests/prism/desugar-const.pm (revision 0) @@ -0,0 +1,4 @@ +const int N = 3; +const int M = N; + +const int test = M; // this should become a 3 with xrm-front -D

1 0