https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit &lt;sigoure.benoit(a)lrde.epita.fr&gt; Add the base for eXtended PCTL. * src/tools/Makefile.am: Add parse-xpctl and pp-xpctl. * src/tools/parse-xpctl.str: New. * src/tools/pp-xpctl.str: New. * src/sig/Makefile.am: Add signature for XPCTL. * src/lib/xrm/pp/Makefile.am: Fix dependencies. * src/lib/Makefile.am (SUBDIRS): Add xpctl. * src/syn/Makefile.am: Ditto. * src/lib/prism/pp/Makefile.am: Fix a comment. * src/lib/xpctl: New. * src/lib/xpctl/pp: New. * src/lib/xpctl/pp/pp-xpctl-to-box.str: New. * src/lib/xpctl/pp/xpctl-to-abox.str: New. * src/lib/xpctl/pp/Makefile.am: New. * src/lib/xpctl/Makefile.am: New. * src/str/xrm-to-prism.str: Make the pipe-line aware of PropertiesFile. * src/str/builtin-rand.str: Add catch-rand. * src/str/xrm-front.str: Add the -p|--pctl option for using PCTL files in xrm-front. Adapt the main-wrapped strategy. * src/syn/pctl/PCTL-Formula.sdf: Remove old comment. * src/syn/xrm/XRM-MetaIf.sdf: Move meta-if statements at the Expression level... * src/syn/xrm/XRM-MetaIfExp.sdf: ... here. * src/syn/xrm/StrategoXRM.sdf: Use StrategoPRISM. * src/syn/xrm/Makefile.am: Add XRM-MetaIfExp.sdf. * src/syn/xpctl: New. * src/syn/xpctl/XPCTL-MetaFor.sdf: New. * src/syn/xpctl/XPCTL.sdf: New. * src/syn/xpctl/XPCTL-MetaVars.sdf: New. * src/syn/xpctl/XPCTL-MetaCongruences.sdf: New. * src/syn/xpctl/XPCTL-Main.sdf: New. * src/syn/xpctl/XPCTL-MetaIf.sdf: New. * src/syn/xpctl/Makefile.am: New. * src/syn/xpctl/XPCTL-StartSymbols.sdf: New. * src/syn/xpctl/StrategoXPCTL.sdf: New. * tests/test-pp-xpctl.sh.in: New. * tests/Makefile.am: Add new tests for parse-xpctl and pp-xpctl. * tests/test-parse-xpctl.sh.in: New. * configure.ac: Add new Makefiles and test scripts. * TODO: New thing to do. TODO | 3 + configure.ac | 13 ++++- src/lib/Makefile.am | 4 - src/lib/prism/pp/Makefile.am | 4 - src/lib/xpctl/Makefile.am | 6 +- src/lib/xpctl/pp/Makefile.am | 34 ++++++++------ src/lib/xpctl/pp/pp-xpctl-to-box.str | 43 +++++++----------- src/lib/xpctl/pp/xpctl-to-abox.str | 22 ++++----- src/lib/xrm/pp/Makefile.am | 10 ++-- src/sig/Makefile.am | 15 ++++-- src/str/builtin-rand.str | 8 ++- src/str/xrm-front.str | 40 +++++++++++++---- src/str/xrm-to-prism.str | 56 ++++++++++++++++++----- src/syn/Makefile.am | 4 - src/syn/pctl/PCTL-Formula.sdf | 2 src/syn/xpctl/Makefile.am | 61 ++++++++++++-------------- src/syn/xpctl/StrategoXPCTL.sdf | 12 +++++ src/syn/xpctl/XPCTL-Main.sdf | 7 +- src/syn/xpctl/XPCTL-MetaCongruences.sdf | 1 src/syn/xpctl/XPCTL-MetaFor.sdf | 33 +++----------- src/syn/xpctl/XPCTL-MetaIf.sdf | 75 +++++--------------------------- src/syn/xpctl/XPCTL-MetaVars.sdf | 1 src/syn/xpctl/XPCTL-StartSymbols.sdf | 4 - src/syn/xpctl/XPCTL.sdf | 4 - src/syn/xrm/Makefile.am | 3 - src/syn/xrm/StrategoXRM.sdf | 20 -------- src/syn/xrm/XRM-MetaIf.sdf | 31 ------------- src/syn/xrm/XRM-MetaIfExp.sdf | 36 +++++++++++++++ src/tools/Makefile.am | 12 ++++- src/tools/parse-xpctl.str | 38 ++++++++-------- src/tools/pp-xpctl.str | 24 +++++----- tests/Makefile.am | 6 ++ tests/test-parse-xpctl.sh.in | 6 +- tests/test-pp-xpctl.sh.in | 28 +++++------ 34 files changed, 345 insertions(+), 321 deletions(-) Index: src/tools/Makefile.am --- src/tools/Makefile.am (revision 61) +++ src/tools/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; ## ## Started on Mon May 8 21:16:56 2006 SIGOURE Benoit -## Last update Sat Jun 10 04:48:43 2006 SIGOURE Benoit +## Last update Sun Jun 11 03:30:17 2006 SIGOURE Benoit ## include $(top_srcdir)/config/Transformers.mk @@ -15,9 +15,11 @@ parse-prism \ parse-pctl \ parse-xrm \ + parse-xpctl \ pp-prism \ pp-pctl \ - pp-xrm + pp-xrm \ + pp-xpctl EXTRA_DIST = $(wildcard *.str) $(wildcard *.meta) CLEANFILES = $(wildcard *.c) $(wildcard *.dep) @@ -29,9 +31,11 @@ -I $(top_srcdir)/src/lib/prism/pp \ -I $(top_srcdir)/src/lib/pctl/pp \ -I $(top_srcdir)/src/lib/xrm/pp \ + -I $(top_srcdir)/src/lib/xpctl/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/lib/xpctl/pp \ -I $(top_builddir)/src/sig LDADD += $(SSL_LIBS) @@ -46,3 +50,7 @@ parse_xrm_SOURCES = parse-xrm.c pp_xrm_SOURCES = pp-xrm.c pp_xrm_LDADD = $(STRATEGO_GPP_LIBS) + +parse_xpctl_SOURCES = parse-xpctl.c +pp_xpctl_SOURCES = pp-xpctl.c +pp_xpctl_LDADD = $(STRATEGO_GPP_LIBS) Index: src/tools/parse-xpctl.str --- src/tools/parse-xpctl.str (revision 61) +++ src/tools/parse-xpctl.str (working copy) @@ -1,23 +1,23 @@ // Code mostly from parse-java by Martin Bravenboer &lt;martin(a)cs.uu.nl&gt; -module parse-xrm +module parse-xpctl imports libxtclib // FIXME: import libstratego-xtc for strc 0.17 tool-doc parser-common strategies - main-parse-xrm = + main-parse-xpctl = // xtc-io-wrap(extra-opts, usage, about, deps, s) xtc-io-wrap( - parse-xrm-options - , parse-xrm-usage + parse-xpctl-options + , parse-xpctl-usage , parser-about - , !["sglr", "implode-asfix", "XRM.tbl", "pp-aterm"] - , parse-xrm + , !["sglr", "implode-asfix", "XPCTL.tbl", "pp-aterm"] + , parse-xpctl ) - parse-xrm-options = + parse-xpctl-options = symbol-option + preserve-comments-option + preserve-positions-option @@ -26,7 +26,7 @@ strategies - parse-xrm = + parse-xpctl = 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 (XRM.tbl) has a - ** single start symbol (ModulesFile) and the other (XRM-StartSymbols) has + ** We use two parse tables for performances. One of them (XPCTL.tbl) has a + ** single start symbol (ModulesFile) and the other (XPCTL-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(?"XRM.tbl") - <+ if get-start-symbol => "ModulesFile" then - !"XRM.tbl" + <get-config> "parsetable"; not(?"XPCTL.tbl") + <+ if get-start-symbol => "PropertiesFile" then + !"XPCTL.tbl" else - !"XRM-StartSymbols.tbl" + !"XPCTL-StartSymbols.tbl" end /** @@ -77,11 +77,11 @@ */ strategies - parse-xrm-usage = + parse-xpctl-usage = <tool-doc> - [ Usage("parse-xrm [OPTIONS]") + [ Usage("parse-xpctl [OPTIONS]") , Summary( - "Parses an eXtended Reactive Module source file to an abstract syntax + "Parses an eXtended Properties source file to an abstract syntax tree in the ATerm format.") , OptionUsage() , AutoReportBugs() Index: src/tools/pp-xpctl.str --- src/tools/pp-xpctl.str (revision 61) +++ src/tools/pp-xpctl.str (working copy) @@ -1,26 +1,26 @@ // Code mostly from pp-java by Martin Bravenboer &lt;martin(a)cs.uu.nl&gt; -module pp-xrm +module pp-xpctl imports libstratego-lib tool-doc libstratego-gpp - pp-xrm-to-box + pp-xpctl-to-box strategies - main-pp-xrm = + main-pp-xpctl = // io-stream-wrap(extra-opts, usage, about, s) io-stream-wrap( fail - , pp-xrm-usage - , pp-xrm-about - , pp-xrm + , pp-xpctl-usage + , pp-xpctl-about + , pp-xpctl ) - pp-xrm = + pp-xpctl = ?(<read-from-stream>, out-file) - ; pp-xrm-to-abox + ; pp-xpctl-to-abox ; box2text-stream(|80, out-file) ; <fputs> ("\n", out-file) @@ -29,17 +29,17 @@ */ strategies - pp-xrm-usage = + pp-xpctl-usage = <tool-doc> - [ Usage("pp-xrm [OPTIONS]") - , Summary("Pretty-prints an eXtended Reactive Module abstract syntax + [ Usage("pp-xpctl [OPTIONS]") + , Summary("Pretty-prints an eXtended Properties abstract syntax tree in ATerm format to an eXtended Reactive Module source file.") , OptionUsage() , AutoReportBugs() ] - pp-xrm-about = + pp-xpctl-about = <tool-doc> [ AutoProgram() , Author(Person("SIGOURE Benoit", &quot;sigoure.benoit(a)lrde.epita.fr&quot;)) Index: src/sig/Makefile.am --- src/sig/Makefile.am (revision 61) +++ src/sig/Makefile.am (working copy) @@ -5,28 +5,33 @@ ## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; ## ## Started on Mon May 8 18:38:32 2006 SIGOURE Benoit -## Last update Sat Jun 10 04:43:36 2006 SIGOURE Benoit +## Last update Sun Jun 11 02:54:51 2006 SIGOURE Benoit ## include $(top_srcdir)/config/Transformers.mk pkgdata_DATA = PRISM.rtg PRISM.str \ PCTL.rtg PCTL.str \ + XPCTL.rtg XPCTL.str \ XRM.rtg XRM.str EXTRA_DIST = $(pkgdata_DATA) -CLEANFILES = $(pkgdata_DATA) PRISM.def PCTL.def XRM.def +CLEANFILES = $(pkgdata_DATA) PRISM.def PCTL.def XPCTL.def XRM.def SDF2RTG_FLAGS = --main $* PRISM.def: $(top_builddir)/src/syn/prism/PRISM.def rm -f $@ - $(LN_S) $(top_builddir)/src/syn/prism/$@ $@ + $(LN_S) $^ $@ PCTL.def: $(top_builddir)/src/syn/pctl/PCTL.def rm -f $@ - $(LN_S) $(top_builddir)/src/syn/pctl/$@ $@ + $(LN_S) $^ $@ + +XPCTL.def: $(top_builddir)/src/syn/xpctl/XPCTL.def + rm -f $@ + $(LN_S) $^ $@ XRM.def: $(top_builddir)/src/syn/xrm/XRM.def rm -f $@ - $(LN_S) $(top_builddir)/src/syn/xrm/$@ $@ + $(LN_S) $^ $@ Index: src/lib/xrm/pp/Makefile.am --- src/lib/xrm/pp/Makefile.am (revision 61) +++ src/lib/xrm/pp/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; ## ## Started on Wed May 10 19:27:12 2006 SIGOURE Benoit -## Last update Thu May 25 17:27:04 2006 SIGOURE Benoit +## Last update Sun Jun 11 03:26:50 2006 SIGOURE Benoit ## include $(top_srcdir)/config/toplevel.mk @@ -23,13 +23,17 @@ SCFLAGS = --main main-$* LDADD += $(SSL_LIBS) -# We put it in BUILT_SOURCES so that it's symlinked before we compile +# We put it in BUILT_SOURCES so that it's built before we compile # xrm-to-abox BUILT_SOURCES = xrm-parenthesize.str EXTRA_DIST = $(wildcard *.str) $(wildcard *.meta) -xrm-parenthesize.str: $(top_builddir)/src/syn/xrm/XRM.def +SDEFS = \ + $(top_builddir)/src/syn/prism/PRISM.def \ + $(top_builddir)/src/syn/xrm/XRM.def + +xrm-parenthesize.str: $(SDEFS) $(SDF_TOOLS)/bin/sdf2parenthesize -i $< -o $@ \ -m XRM \ --omod xrm-parenthesize \ Index: src/lib/Makefile.am --- src/lib/Makefile.am (revision 61) +++ src/lib/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; ## ## Started on Wed May 10 19:27:12 2006 SIGOURE Benoit -## Last update Sat Jun 10 03:57:26 2006 SIGOURE Benoit +## Last update Sun Jun 11 02:56:24 2006 SIGOURE Benoit ## -SUBDIRS = prism pctl xrm native +SUBDIRS = prism pctl xrm xpctl native Index: src/lib/prism/pp/Makefile.am --- src/lib/prism/pp/Makefile.am (revision 61) +++ src/lib/prism/pp/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; ## ## Started on Wed May 10 19:27:12 2006 SIGOURE Benoit -## Last update Thu May 25 17:26:51 2006 SIGOURE Benoit +## Last update Sun Jun 11 02:59:46 2006 SIGOURE Benoit ## include $(top_srcdir)/config/toplevel.mk @@ -22,7 +22,7 @@ SCFLAGS = --main main-$* LDADD += $(SSL_LIBS) -# We put it in BUILT_SOURCES so that it's symlinked before we compile +# We put it in BUILT_SOURCES so that it's built before we compile # prism-to-abox BUILT_SOURCES = prism-parenthesize.str Index: src/lib/xpctl/pp/pp-xpctl-to-box.str --- src/lib/xpctl/pp/pp-xpctl-to-box.str (revision 0) +++ src/lib/xpctl/pp/pp-xpctl-to-box.str (working copy) @@ -1,37 +1,30 @@ -module pp-xrm-to-box +module pp-xpctl-to-box imports Box - XRM // signature - PRISM // signature of the base language (see README) - prism-command + XPCTL // signature + PCTL // signature of the base language prism-constant - prism-declaration prism-expression - prism-formula - prism-global - prism-init - prism-module - prism-modulesfile - prism-modulesfiletype - prism-reward - prism-systemcomposition - prism-update - xrm-parenthesize - xrm-expression - xrm-module - xrm-meta-for - xrm-meta-if - xrm-arrays + xpctl-parenthesize + pctl-properties-file + pctl-label + pctl-formula + pctl-property + pctl-path + pctl-reward + pctl-filter + xrm-meta-for // Hack: Meta-For loops are identical in XPCTL and XRM. :) + xrm-meta-if // Ditto. strategies - pp-xrm-to-abox = - pp-xrm-to-abox(prism-to-box) // we keep prism-to-box as rule name + pp-xpctl-to-abox = + pp-xpctl-to-abox(prism-to-box) // we keep prism-to-box as rule name // because we simply extend it - pp-xrm-to-abox(pprules) = - // strategy from xrm-parenthesize.str generated by sdf2parenthesize - parenthesize-XRM + pp-xpctl-to-abox(pprules) = + // strategy from xpctl-parenthesize.str generated by sdf2parenthesize + parenthesize-XPCTL ; topdown(try(very-special-conflict) ; repeat(pprules)) Index: src/lib/xpctl/pp/xpctl-to-abox.str --- src/lib/xpctl/pp/xpctl-to-abox.str (revision 0) +++ src/lib/xpctl/pp/xpctl-to-abox.str (working copy) @@ -1,26 +1,26 @@ -module xrm-to-abox +module xpctl-to-abox imports libxtclib // FIXME: import libstratego-xtc for strc 0.17 tool-doc - pp-xrm-to-box + pp-xpctl-to-box strategies - main-xrm-to-abox = + main-xpctl-to-abox = // xtc-io-wrap(extra-opts, usage, about, deps, s) xtc-io-wrap( fail - , xrm-to-abox-usage - , xrm-to-abox-about + , xpctl-to-abox-usage + , xpctl-to-abox-about , ![] , main-wrapped ) - // main wrapped in main-xrm-to-abox + // main wrapped in main-xpctl-to-abox main-wrapped = // read data from input read-from - ; pp-xrm-to-abox + ; pp-xpctl-to-abox ; if <get-config> "-b" then write-to // write binary output else @@ -32,16 +32,16 @@ */ strategies - xrm-to-abox-usage = + xpctl-to-abox-usage = <tool-doc> - [ Usage("xrm-to-abox [OPTIONS]") - , Summary("Transforms an XRM abstract syntax tree in ATerm format + [ Usage("xpctl-to-abox [OPTIONS]") + , Summary("Transforms an XPCTL abstract syntax tree in ATerm format to a box representation of the AST for pretty-printing") , OptionUsage() , AutoReportBugs() ] - xrm-to-abox-about = + xpctl-to-abox-about = <tool-doc> [ AutoProgram() , Author(Person("SIGOURE Benoit", &quot;sigoure.benoit(a)lrde.epita.fr&quot;)) Index: src/lib/xpctl/pp/Makefile.am --- src/lib/xpctl/pp/Makefile.am (revision 0) +++ src/lib/xpctl/pp/Makefile.am (working copy) @@ -1,38 +1,44 @@ ## -## Makefile.am for xrm in /home/tsuna/work/xrm/trunk/src/lib/pctl/pp +## Makefile.am for xrm in /home/tsuna/work/xrm/trunk/src/lib/xpctl/pp ## ## Made by SIGOURE Benoit ## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; ## ## Started on Sat Jun 10 03:59:11 2006 SIGOURE Benoit -## Last update Sat Jun 10 04:00:21 2006 SIGOURE Benoit +## Last update Sun Jun 11 03:26:36 2006 SIGOURE Benoit ## include $(top_srcdir)/config/toplevel.mk -include $(wildcard *.dep) -pkgdata_DATA = pctl-parenthesize.str -libexec_PROGRAMS = pctl-to-abox +pkgdata_DATA = xpctl-parenthesize.str +libexec_PROGRAMS = xpctl-to-abox -pctl_to_abox_SOURCES = pctl-to-abox.c +xpctl_to_abox_SOURCES = xpctl-to-abox.c STRINCLUDES = -I $(GPP)/share/sdf/gpp -I $(GPP)/share/gpp \ -I $(top_srcdir)/src/lib/prism/pp \ + -I $(top_srcdir)/src/lib/pctl/pp \ -I $(top_builddir)/src/lib/pctl/pp -I $(srcdir) \ + -I $(top_srcdir)/src/lib/xrm/pp \ + -I $(top_builddir)/src/lib/xrm/pp -I $(srcdir) \ + -I $(top_builddir)/src/lib/xpctl/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 +BUILT_SOURCES = xpctl-parenthesize.str EXTRA_DIST = $(wildcard *.str) $(wildcard *.meta) -pctl-parenthesize.str: $(top_builddir)/src/syn/pctl/PCTL.def +SDEFS = \ + $(top_builddir)/src/syn/pctl/PCTL.def \ + $(top_builddir)/src/syn/xpctl/XPCTL.def + +xpctl-parenthesize.str: $(SDEFS) $(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 + -m XPCTL \ + --omod xpctl-parenthesize \ + --sig-module $(top_builddir)/src/sig/XPCTL \ + --main-strategy io-xpctl-parenthesize \ + --lang XPCTL Index: src/lib/xpctl/Makefile.am --- src/lib/xpctl/Makefile.am (revision 0) +++ src/lib/xpctl/Makefile.am (working copy) @@ -1,11 +1,11 @@ ## -## Makefile.am for xrm in /home/tsuna/work/xrm/trunk/src/lib/pctl +## Makefile.am for xrm in /home/tsuna/work/xrm/trunk/src/lib/xpctl ## ## Made by SIGOURE Benoit ## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; ## -## Started on Sat Jun 10 03:57:49 2006 SIGOURE Benoit -## Last update Sat Jun 10 03:58:01 2006 SIGOURE Benoit +## Started on Sun Jun 11 02:56:41 2006 SIGOURE Benoit +## Last update Sun Jun 11 02:56:52 2006 SIGOURE Benoit ## SUBDIRS = pp Index: src/str/xrm-to-prism.str --- src/str/xrm-to-prism.str (revision 61) +++ src/str/xrm-to-prism.str (working copy) @@ -27,7 +27,8 @@ */ module xrm-to-prism imports - XRM + XRM // signature + PCTL // signature collect-static-const-decl prism-desugar flatten-array-access @@ -39,20 +40,30 @@ strategies xrm-to-prism = + /* bind the start-symbol (ModulesFile or PropertiesFile) */ + ?start-symbol#(_) + ; if <is-module-file> start-symbol then /* remove XRM sugar, normalize some nodes */ - innermost( - DesugarRightShift <+ DesugarLeftShift - <+ DesugarImplicitForStep <+ DesugarImplicitElse - <+ DesugarRand <+ EvalRand - /*FIXME: to be implemented. - <+ DesugarArrayEq <+ DesugarArrayNotEq - <+ DesugarArrayExistsEq <+ DesugarArrayExistsNotEq*/ - ) + innermost(xrm-generic-desugar <+ DesugarRand <+ EvalRand) + else + if <is-properties-file> start-symbol then + /* rand isn't allowed in PropertiesFile hence the catch-rand */ + innermost(xrm-generic-desugar <+ catch-rand) + else + ice(|"xrm-to-prism", "Unexpected start-symbol", start-symbol) + end + end ; notice-msg(|"xrm-to-prism: XRM sugar removed") /* Collect static const variables * Two goals: expand them if needed, look for variable name conflicts. */ - ; ModulesFile(id, map(try(collect-static-const-decl); try(collect-formulas))) + ; if <is-module-file> start-symbol then + ModulesFile(id, map(try(collect-static-const-decl) + ; try(collect-formulas))) + else + PropertiesFile(map(try(collect-static-const-decl) + ; try(collect-formulas))) + end ; notice-msg(|"xrm-to-prism: static const and formulas collected") /* Check that meta vars are always defined in the current scope when used @@ -82,7 +93,8 @@ ; notice-msg(|"xrm-to-prism: array declarations desugared") /* flatten nested lists */ - ; ModulesFile(id, flatten-list) + ; if <is-module-file> start-symbol then + ModulesFile(id, flatten-list) ; ModulesFile(id, map(try(Module(id, flatten-list)))) ; notice-msg(|"xrm-to-prism: flatten-list done") @@ -92,15 +104,35 @@ /* paste them at the end of the file */ ; ModulesFile(id, <conc>(<id>, rand-gen-modules)) ; notice-msg(|"xrm-to-prism: added modules for random numbers") + end /* remove array accesses: x[i] -> x_i */ // FIXME: can we make this more efficient than a complete bottomup? ; bottomup(try(flatten-array-access)) ; notice-msg(|"xrm-to-prism: flatten-array-access done") + ; if <is-module-file> start-symbol then /* re-order modules so that all declarations appear before commands */ - ; ModulesFile(id, map(try(reorder-module-contents))) + ModulesFile(id, map(try(reorder-module-contents))) ; notice-msg(|"xrm-to-prism: reorder-module-contents done") + end + + is-module-file = ?"ModulesFile" + is-properties-file = ?"PropertiesFile" + +strategies + + /** + ** Perform generic transformations which can apply to either a ModulesFile + ** or a PropertiesFile. + */ + xrm-generic-desugar = + DesugarRightShift <+ DesugarLeftShift + <+ DesugarImplicitForStep <+ DesugarImplicitElse + /*FIXME: to be implemented. + <+ DesugarArrayEq <+ DesugarArrayNotEq + <+ DesugarArrayExistsEq <+ DesugarArrayExistsNotEq + */ rules Index: src/str/builtin-rand.str --- src/str/builtin-rand.str (revision 61) +++ src/str/builtin-rand.str (working copy) @@ -114,10 +114,16 @@ invalid-call-to-rand-non-int = err-msg(|<concat-strings>["invalid call to XRM builtin: rand's", - " arguments must be statically evaluable"]) + " arguments must be statically evaluable."]) ; debug ; <xtc-exit> 4 + /** Issue an error if rand is called in a property file */ + catch-rand = + ?Rand(_) + ; err-msg(|"you cannot use the XRM builtin rand in a property file.") + ; <xtc-exit> 4 + strategies /** Index: src/str/xrm-front.str --- src/str/xrm-front.str (revision 61) +++ src/str/xrm-front.str (working copy) @@ -20,22 +20,29 @@ main-wrapped = check-options - ; xtc-transform(!"parse-xrm", // parse input (returns a FILE) + ; xtc-transform(get-parser, // parse input (returns a FILE) <concat>[ ["-b"], <pass-verbose>(), <pass-add-pos>() ]) ; read-from // read parsed input ; xrm-front-pipeline // transformations ; if not(must-keep-attributes) then strip-annos end - ; if <get-config> "-b" then - write-to // output binary ATerms - else + /* save the current term in a /tmp file with binary ATerms */ + ; write-to + ; if not(<get-config> "-b") then if must-pp-aterm then // output pp-ATerms notice-msg(|"pretty printing ATerms") - ; write-to; xtc-transform(!"pp-aterm", pass-verbose) + ; xtc-transform(!"pp-aterm", pass-verbose) + else + if must-parse-pctl then // output PCTL source + notice-msg(|"pretty printing PCTL code") + ; xtc-transform(!"pp-pctl", pass-verbose) else // output PRISM source notice-msg(|"pretty printing PRISM code") - ; write-to; xtc-transform(!"pp-prism", pass-verbose) + ; xtc-transform(!"pp-prism", pass-verbose) + end end end + /* default: if we don't get inside the previous if, we will output + * binary ATerms. */ /** pipeline of transformations performed by xrm-front */ xrm-front-pipeline = @@ -53,6 +60,7 @@ + add-pos-option + keep-attributes-option + desugar-option + + parse-pctl-option /** checks the options are consistent */ check-options = @@ -125,6 +133,22 @@ pass-add-pos = must-add-pos < !["--preserve-positions"] + ![] +strategies + + parse-pctl-option = + Option("-p" + "--pctl" + , <set-parse-pctl> "yes" + , !HelpString("-p | --pctl", "The input file is an eXtended PCTL file") + ) + + set-parse-pctl = + <set-config> ("parse-pctl", <id>) + + must-parse-pctl = + <get-config> "parse-pctl" => "yes" + + get-parser = must-parse-pctl < !"parse-pctl" + !"parse-xrm" + /** * Documentation */ @@ -133,8 +157,8 @@ xrm-front-usage = <tool-doc> [ Usage("xrm-front [OPTIONS]") - , Summary("Transforms an eXtended Reactive Module source file in a - PRISM-equivalent source code (default) or abstract syntax + , Summary("Transforms an eXtended Reactive Module or Property source file + in a PRISM-equivalent source code (default) or abstract syntax tree. (see option -A)") , OptionUsage() , AutoReportBugs() Index: src/syn/pctl/PCTL-Formula.sdf --- src/syn/pctl/PCTL-Formula.sdf (revision 61) +++ src/syn/pctl/PCTL-Formula.sdf (working copy) @@ -15,8 +15,6 @@ %% %% PCTLFormula ::= PCTLImplies %% - %% PCTLImplies ::= PCTLOr ["=>" PCTLOr] - %% sorts Formula context-free syntax Index: src/syn/xrm/XRM-MetaIf.sdf --- src/syn/xrm/XRM-MetaIf.sdf (revision 61) +++ src/syn/xrm/XRM-MetaIf.sdf (working copy) @@ -2,6 +2,7 @@ imports PRISM-to-XRM XRM-Module + XRM-MetaIfExp exports %% EBNF Grammar: Meta if-then-else @@ -22,19 +23,6 @@ %% "else" %% {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 @@ -61,20 +49,3 @@ "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/StrategoXRM.sdf --- src/syn/xrm/StrategoXRM.sdf (revision 61) +++ src/syn/xrm/StrategoXRM.sdf (working copy) @@ -1,32 +1,14 @@ module StrategoXRM imports - StrategoRenamed + StrategoPRISM XRM PRISM-MetaVars PRISM-MetaCongruences XRM-MetaVars XRM-MetaCongruences - XRM-MetaFor - XRM-MetaIf exports - context-free start-symbols StrategoModule context-free syntax - - "|[" Module "]|" -> StrategoTerm {prefer,cons("ToTerm")} - "|[" RenamedModule "]|" -> StrategoTerm {prefer,cons("ToTerm")} - "|[" Expression "]|" -> StrategoTerm {prefer,cons("ToTerm")} - "|[" Declaration "]|" -> StrategoTerm {prefer,cons("ToTerm")} - "|[" Command "]|" -> StrategoTerm {prefer,cons("ToTerm")} "|[" MetaFor "]|" -> StrategoTerm {prefer,cons("ToTerm")} "|[" MetaIf "]|" -> StrategoTerm {prefer,cons("ToTerm")} - - context-free syntax - - "~" StrategoTerm -> Expression {prefer,cons("FromTerm")} - "~id:" StrategoTerm -> ID {prefer,cons("FromTerm")} - %% FIXME: the following rule is b0rken - "~id':" StrategoTerm -> IdentifierPrime {prefer,cons("FromTerm")} - "~int:" StrategoTerm -> LInt {prefer,cons("FromTerm")} - "~double:" StrategoTerm -> LDouble {prefer,cons("FromTerm")} Index: src/syn/xrm/XRM-MetaIfExp.sdf --- src/syn/xrm/XRM-MetaIfExp.sdf (revision 0) +++ src/syn/xrm/XRM-MetaIfExp.sdf (revision 0) @@ -0,0 +1,36 @@ +module XRM-MetaIfExp +%%imports %% import commented out so that we can import +%% PRISM-to-XRM %% XRM-MetaIfExp from XPCTL without importing +exports %% the whole PRISM stuff.. dirty hack inside! + + %% EBNF Grammar: Meta if-then-else + %% + %% (* 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" + + %% 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/Makefile.am --- src/syn/xrm/Makefile.am (revision 61) +++ src/syn/xrm/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; ## ## Started on Thu Apr 27 17:40:41 2006 SIGOURE Benoit -## Last update Sat Jun 10 00:20:27 2006 SIGOURE Benoit +## Last update Sun Jun 11 02:39:02 2006 SIGOURE Benoit ## include $(top_srcdir)/config/Transformers.mk @@ -53,6 +53,7 @@ XRM-MetaCongruences.sdf \ XRM-MetaFor.sdf \ XRM-MetaIf.sdf \ + XRM-MetaIfExp.sdf \ XRM-MetaVars.sdf \ XRM-Module.sdf \ XRM-StartSymbols.sdf \ Index: src/syn/Makefile.am --- src/syn/Makefile.am (revision 61) +++ src/syn/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; ## ## Started on Thu Apr 27 17:40:41 2006 SIGOURE Benoit -## Last update Fri Jun 9 19:16:48 2006 SIGOURE Benoit +## Last update Sun Jun 11 02:30:13 2006 SIGOURE Benoit ## -SUBDIRS = prism pctl xrm +SUBDIRS = prism pctl xrm xpctl Index: src/syn/xpctl/XPCTL-MetaFor.sdf --- src/syn/xpctl/XPCTL-MetaFor.sdf (revision 0) +++ src/syn/xpctl/XPCTL-MetaFor.sdf (working copy) @@ -1,41 +1,24 @@ -module XRM-MetaFor +module XPCTL-MetaFor imports - PRISM-to-XRM - XRM-Module + PCTL-PropertiesFile exports %% EBNF Grammar: Meta For Loops %% (* Meta For loops at the top level *) - %% ModulesFileSection ::= + %% PropertiesFileSection ::= %% "for" Identifier "from" Expression "to" Expression %% ["step" Expression] "do" - %% {ModulesFileSection} "end" + %% {PropertiesFileSection} "end" %% - %% (* Meta For loops inside modules *) - %% DeclarationOrCommand ::= - %% "for" Identifier "from" Expression "to" Expression - %% ["step" Expression] "do" - %% {DeclarationOrCommand} "end" context-free syntax %% This MetaFor can be found only at top-level - %% So we can see it as a ModulesFileSection - "for" Identifier "from" Expression "to" Expression "do" - ModulesFileSection* "end" -> ModulesFileSection {cons("MetaFor")} - - "for" Identifier "from" Expression "to" Expression "step" Expression "do" - ModulesFileSection* "end" -> ModulesFileSection {cons("MetaFor")} - - "for" Identifier "in" {Expression ","}+ "do" - ModulesFileSection* "end" -> ModulesFileSection {cons("MetaForIn")} - - %% This MetaFor can be found only inside Modules - %% So we can see it as a DeclarationOrCommand + %% So we can see it as a PropertiesFileSection "for" Identifier "from" Expression "to" Expression "do" - DeclarationOrCommand* "end" -> DeclarationOrCommand {cons("MetaFor")} + PropertiesFileSection* "end" -> PropertiesFileSection {cons("MetaFor")} "for" Identifier "from" Expression "to" Expression "step" Expression "do" - DeclarationOrCommand* "end" -> DeclarationOrCommand {cons("MetaFor")} + PropertiesFileSection* "end" -> PropertiesFileSection {cons("MetaFor")} "for" Identifier "in" {Expression ","}+ "do" - ModulesFileSection* "end" -> DeclarationOrCommand {cons("MetaForIn")} + PropertiesFileSection* "end" -> PropertiesFileSection {cons("MetaForIn")} Index: src/syn/xpctl/XPCTL.sdf --- src/syn/xpctl/XPCTL.sdf (revision 0) +++ src/syn/xpctl/XPCTL.sdf (working copy) @@ -2,9 +2,9 @@ %% 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 +module XPCTL imports - PCTL-Main + XPCTL-Main exports context-free start-symbols Index: src/syn/xpctl/XPCTL-MetaVars.sdf --- src/syn/xpctl/XPCTL-MetaVars.sdf (revision 0) +++ src/syn/xpctl/XPCTL-MetaVars.sdf (revision 0) @@ -0,0 +1 @@ +module XPCTL-MetaVars Index: src/syn/xpctl/XPCTL-MetaCongruences.sdf --- src/syn/xpctl/XPCTL-MetaCongruences.sdf (revision 0) +++ src/syn/xpctl/XPCTL-MetaCongruences.sdf (revision 0) @@ -0,0 +1 @@ +module XPCTL-MetaCongruences Index: src/syn/xpctl/XPCTL-Main.sdf --- src/syn/xpctl/XPCTL-Main.sdf (revision 0) +++ src/syn/xpctl/XPCTL-Main.sdf (working copy) @@ -1,4 +1,5 @@ -module PCTL-Main +module XPCTL-Main imports - PRISM-Layout - PCTL-PropertiesFile + PCTL-Main + XPCTL-MetaFor + XPCTL-MetaIf Index: src/syn/xpctl/XPCTL-MetaIf.sdf --- src/syn/xpctl/XPCTL-MetaIf.sdf (revision 0) +++ src/syn/xpctl/XPCTL-MetaIf.sdf (working copy) @@ -1,80 +1,29 @@ -module XRM-MetaIf +module XPCTL-MetaIf imports - PRISM-to-XRM - XRM-Module + PCTL-PropertiesFile + XRM-MetaIfExp exports %% EBNF Grammar: Meta if-then-else %% (* if-then-else at top-level *) - %% ModulesFileSection ::= - %% "if" Expression "then" {ModulesFileSection} "end" + %% PropertiesFile ::= + %% "if" Expression "then" {PropertiesFile} "end" %% | "if" Expression "then" - %% {ModulesFileSection} + %% {PropertiesFile} %% "else" - %% {ModulesFileSection} + %% {PropertiesFile} %% "end" %% - %% (* if-then-else inside modules *) - %% DeclarationOrCommand ::= - %% "if" Expression "then" {DeclarationOrCommand} "end" - %% | "if" Expression "then" - %% {DeclarationOrCommand} - %% "else" - %% {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")} + "if" Expression "then" PropertiesFile* "end" + -> PropertiesFile {cons("MetaIf")} %% if-then-else at top-level "if" Expression "then" - ModulesFileSection* - "else" - ModulesFileSection* - "end" -> ModulesFileSection {cons("MetaIf")} - - context-free syntax - - %% if-then within modules - "if" Expression "then" DeclarationOrCommand* "end" - -> DeclarationOrCommand {cons("MetaIf")} - - %% if-then-else within modules - "if" Expression "then" - DeclarationOrCommand* - "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 + PropertiesFile* "else" - Expression - "end" -> Expression {cons("MetaIf")} + PropertiesFile* + "end" -> PropertiesFile {cons("MetaIf")} Index: src/syn/xpctl/Makefile.am --- src/syn/xpctl/Makefile.am (revision 0) +++ src/syn/xpctl/Makefile.am (working copy) @@ -1,11 +1,11 @@ ## -## Makefile.am for xrm in /home/tsuna/work/xrm/trunk/src/syn/pctl +## Makefile.am for xrm in /home/tsuna/work/xrm/trunk/src/syn/xpctl ## ## Made by SIGOURE Benoit ## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; ## ## Started on Sat Jun 10 00:17:31 2006 SIGOURE Benoit -## Last update Sat Jun 10 00:36:56 2006 SIGOURE Benoit +## Last update Sun Jun 11 02:42:19 2006 SIGOURE Benoit ## include $(top_srcdir)/config/Transformers.mk @@ -17,49 +17,46 @@ STRINCLUDES = -I $(srcdir) SDFINCLUDES = -I $(srcdir) \ -I $(STRATEGO_FRONT)/share/sdf/stratego-front \ - -I $(top_srcdir)/src/syn/prism + -I $(top_srcdir)/src/syn/prism \ + -I $(top_srcdir)/src/syn/xrm \ + -I $(top_srcdir)/src/syn/pctl pkgdata_DATA_built = \ - PCTL.def \ - PCTL.tbl \ - PCTL.rtg \ - PCTL.str \ - PCTL-StartSymbols.tbl \ - PCTL-Prefixed.def \ - StrategoPCTL.def \ - StrategoPCTL.tbl + XPCTL.def \ + XPCTL.tbl \ + XPCTL.rtg \ + XPCTL.str \ + XPCTL-StartSymbols.tbl \ + XPCTL-Prefixed.def \ + StrategoXPCTL.def \ + StrategoXPCTL.tbl pkgdata_DATA = $(pkgdata_DATA_built) sdfdata_DATA = $(pkgdata_DATA_built) -nobase_sdfdata_DATA = PCTL-Prefixed.sdf $(SDFS) +nobase_sdfdata_DATA = XPCTL-Prefixed.sdf $(SDFS) CLEANFILES = $(pkgdata_DATA_built) \ $(wildcard *.dep) \ - PCTL.{c,str,c.dep} \ - PCTL-StartSymbols.def \ - PCTL-Prefixed.def + XPCTL.{c,str,c.dep} \ + XPCTL-StartSymbols.def \ + XPCTL-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 + XPCTL-Main.sdf \ + XPCTL-MetaFor.sdf \ + XPCTL-MetaIf.sdf \ + XPCTL-StartSymbols.sdf \ + XPCTL.sdf EXTRA_DIST = $(SDFS) -PCTL.def: $(SDFS) -PCTL-StartSymbols.def: $(SDFS) +XPCTL.def: $(SDFS) +XPCTL-StartSymbols.def: $(SDFS) -StrategoPCTL.def: StrategoPCTL.sdf \ - PCTL-MetaVars.sdf \ - PCTL-MetaCongruences.sdf +StrategoXPCTL.def: StrategoXPCTL.sdf \ + XPCTL-MetaVars.sdf \ + XPCTL-MetaCongruences.sdf -PCTL-Prefixed.sdf: PCTL.def +XPCTL-Prefixed.sdf: XPCTL.def $(SDF_TOOLS)/bin/gen-renamed-sdf-module -i $< -o $@ \ - --main PCTL --name PCTL-Prefixed --prefix PCTL + --main XPCTL --name XPCTL-Prefixed --prefix XPCTL Index: src/syn/xpctl/XPCTL-StartSymbols.sdf --- src/syn/xpctl/XPCTL-StartSymbols.sdf (revision 0) +++ src/syn/xpctl/XPCTL-StartSymbols.sdf (working copy) @@ -2,9 +2,9 @@ %% 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 +module XPCTL-StartSymbols imports - PCTL-Main + XPCTL-Main exports context-free start-symbols Index: src/syn/xpctl/StrategoXPCTL.sdf --- src/syn/xpctl/StrategoXPCTL.sdf (revision 0) +++ src/syn/xpctl/StrategoXPCTL.sdf (revision 0) @@ -0,0 +1,12 @@ +module StrategoXPCTL +imports + StrategoPCTL + XPCTL + XPCTL-MetaVars + XPCTL-MetaCongruences + +exports + + context-free syntax + "|[" MetaFor "]|" -> StrategoTerm {prefer,cons("ToTerm")} + "|[" MetaIf "]|" -> StrategoTerm {prefer,cons("ToTerm")} Index: tests/test-pp-xpctl.sh.in --- tests/test-pp-xpctl.sh.in (revision 61) +++ tests/test-pp-xpctl.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-xpctl.sh for xrm in /home/tsuna/work/xrm/trunk/tests ## ## Made by SIGOURE Benoit ## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; @@ -11,7 +11,7 @@ test_cnt=0 test_pass=0 -target_dir='output-pp-xrm' +target_dir='output-pp-xpctl' rm -f failed_tests.$$ test ! -d $target_dir && { mkdir $target_dir \ @@ -21,15 +21,15 @@ 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$//'`" + bfile="`echo \"$basefile\" | sed 's/\.x\?pctl$//;s/\.x\?csl//'`" echo ">>> Starting the test for $basefile" 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-xpctl" -i "$file" -o "$outdir/$bfile.aterm" if [ $? -ne 0 ]; then echo 'FAILED, continuing with the next test...' echo " * $file: parsing FAILED" >> failed_tests.$$ @@ -38,8 +38,8 @@ echo 'OK, no ambiguities found' echo @ECHO_N@ " Pretty printing $basefile ... " - "@top_builddir@/src/tools/pp-xrm" \ - -i "$outdir/$bfile.aterm" -o "$outdir/$bfile.pp.xpm" + "@top_builddir@/src/tools/pp-xpctl" \ + -i "$outdir/$bfile.aterm" -o "$outdir/$bfile.pp.xpctl" if [ $? -ne 0 ]; then echo 'FAILED, continuing with the next test...' echo " * $file: pretty printing FAILED" >> failed_tests.$$ @@ -48,12 +48,12 @@ echo 'OK' echo @ECHO_N@ " Re-Parsing pretty printed file $basefile ... " - "@top_builddir@/src/tools/parse-xrm" \ - -i "$outdir/$bfile.pp.xpm" -o "$outdir/$bfile.pp2aterm" + "@top_builddir@/src/tools/parse-xpctl" \ + -i "$outdir/$bfile.pp.xpctl" -o "$outdir/$bfile.pp2aterm" if [ $? -ne 0 ]; then echo 'FAILED, here is the content of the file:' echo '>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>' - cat -n "$outdir/$bfile.pp.xpm" + cat -n "$outdir/$bfile.pp.xpctl" echo '<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<' echo 'Now continuing with the next test...' echo " * $file: re-parsing FAILED" >> failed_tests.$$ @@ -62,8 +62,8 @@ echo 'OK, no ambiguities found' echo @ECHO_N@ " Re-Pretty printing the re-parsed file $basefile ... " - "@top_builddir@/src/tools/pp-xrm" \ - -i "$outdir/$bfile.pp2aterm" -o "$outdir/$bfile.pp2.xpm" + "@top_builddir@/src/tools/pp-xpctl" \ + -i "$outdir/$bfile.pp2aterm" -o "$outdir/$bfile.pp2.xpctl" if [ $? -ne 0 ]; then echo 'FAILED, continuing with the next test...' echo " * $file: re-pretty printing FAILED" >> failed_tests.$$ @@ -73,7 +73,7 @@ err='' diff -q "$outdir/$bfile.aterm" "$outdir/$bfile.pp2aterm" || err='aterm' - diff -q "$outdir/$bfile.pp.xpm" "$outdir/$bfile.pp2.xpm" || err="$err+pp" + diff -q "$outdir/$bfile.pp.xpctl" "$outdir/$bfile.pp2.xpctl" || err="$err+pp" case $err in *aterm*) @@ -88,7 +88,7 @@ ;; *pp*) echo 'FAILED: the two pretty printing did NOT produce the same source:' - diff -u "$outdir/$bfile.pp.xpm" "$outdir/$bfile.pp2.xpm" + diff -u "$outdir/$bfile.pp.xpctl" "$outdir/$bfile.pp2.xpctl" echo " * $file: both pretty pretty did NIT produce the same source" >> failed_tests.$$ continue ;; Index: tests/Makefile.am --- tests/Makefile.am (revision 61) +++ tests/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; ## ## Started on Thu Apr 27 16:56:50 2006 SIGOURE Benoit -## Last update Sat Jun 10 05:24:43 2006 SIGOURE Benoit +## Last update Sun Jun 11 03:40:50 2006 SIGOURE Benoit ## #include $(top_srcdir)/config/toplevel.mk @@ -14,9 +14,11 @@ test-parse-prism.sh \ test-parse-pctl.sh \ test-parse-xrm.sh \ + test-parse-xpctl.sh \ test-pp-prism.sh \ test-pp-pctl.sh \ test-pp-xrm.sh \ + test-pp-xpctl.sh \ test-xrm-front.sh # Set the XTC_REPOSITORY environment variable so that we override the XTC @@ -29,9 +31,11 @@ TESTS = test-parse-prism.sh \ test-parse-pctl.sh \ test-parse-xrm.sh \ + test-parse-xpctl.sh \ test-pp-prism.sh \ test-pp-pctl.sh \ test-pp-xrm.sh \ + test-pp-xpctl.sh \ test-xrm-front.sh \ test-summary.sh Index: tests/test-parse-xpctl.sh.in --- tests/test-parse-xpctl.sh.in (revision 61) +++ tests/test-parse-xpctl.sh.in (working copy) @@ -1,6 +1,6 @@ #!/bin/sh ## -## test-parse-xrm.sh for xrm in /home/tsuna/work/xrm/trunk/tests +## test-parse-xpctl.sh for xrm in /home/tsuna/work/xrm/trunk/tests ## ## Made by SIGOURE Benoit ## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; @@ -13,9 +13,9 @@ test_pass=0 rm -f failed_tests.$$ -for file in `find "@srcdir@" -name '*.pm' -o -name '*.nm' -o -name '*.sm' -o -name '*.xpm' | sort`; do +for file in `find "@srcdir@" -name '*.pctl' -o -name '*.csl' -o -name '*.xpctl' -o -name '*.xcsl' | sort`; do echo @ECHO_N@ " Parsing `basename $file` ... " - "@top_builddir@/src/tools/parse-xrm" -i "$file" -o /dev/null + "@top_builddir@/src/tools/parse-xpctl" -i "$file" -o /dev/null rv=$? test_cnt=$((test_cnt + 1)) if [ $? -eq 0 ]; then Index: configure.ac --- configure.ac (revision 61) +++ configure.ac (working copy) @@ -5,7 +5,7 @@ ## Mail &lt;sigoure.benoit(a)lrde.epita.fr&gt; ## ## Started on Thu Apr 27 15:55:56 2006 SIGOURE Benoit -## Last update Sat Jun 10 05:25:09 2006 SIGOURE Benoit +## Last update Sun Jun 11 03:38:49 2006 SIGOURE Benoit ## ## --------------- ## @@ -75,6 +75,7 @@ src/syn/prism/Makefile src/syn/pctl/Makefile src/syn/xrm/Makefile + src/syn/xpctl/Makefile src/sig/Makefile src/str/Makefile src/lib/Makefile @@ -84,6 +85,8 @@ src/lib/pctl/pp/Makefile src/lib/xrm/Makefile src/lib/xrm/pp/Makefile + src/lib/xpctl/Makefile + src/lib/xpctl/pp/Makefile src/lib/native/Makefile src/tools/Makefile tests/Makefile @@ -91,10 +94,12 @@ AC_CONFIG_FILES([tests/test-parse-prism.sh], [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-parse-xrm.sh], + [chmod a=rx tests/test-parse-xrm.sh]) +AC_CONFIG_FILES([tests/test-parse-xpctl.sh], + [chmod a=rx tests/test-parse-xpctl.sh]) AC_CONFIG_FILES([tests/test-pp-prism.sh], [chmod a=rx tests/test-pp-prism.sh]) @@ -102,6 +107,8 @@ [chmod a=rx tests/test-pp-pctl.sh]) AC_CONFIG_FILES([tests/test-pp-xrm.sh], [chmod a=rx tests/test-pp-xrm.sh]) +AC_CONFIG_FILES([tests/test-pp-xpctl.sh], + [chmod a=rx tests/test-pp-xpctl.sh]) AC_CONFIG_FILES([tests/test-xrm-front.sh], [chmod a=rx tests/test-xrm-front.sh]) Index: TODO --- TODO (revision 61) +++ TODO (working copy) @@ -13,6 +13,9 @@ * Add tests using "system ... endsystem" (it's properly not parsed atm) + * Fix the PCTL grammar (see tests/pctl/longuest-exp-match.pctl for a simple + test case) + * 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.