https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit <sigoure.benoit@lrde.epita.fr> Add XPCTL in XRM. It is now possible to specify properties in property sections directly in XRM (see the update to user-guide.txt). * src/lib/xrm/pp/xrm-properties.meta: New. * src/lib/xrm/pp/pp-xrm-to-box.str: Import xrm-properties. * src/lib/xrm/pp/xrm-properties.str: New. * src/str/xrm-to-prism.str: Handle properties in XRM. * src/str/xrm-front.str: Add the --p-output | -po option. * src/str/properties-in-xrm.str: New. * src/syn/xrm/XRM-Main.sdf: Import XRM-Properties. * src/syn/xrm/XRM-Module.sdf: Make it possible to end the declaration of a module with `end' instead of `endmodule'. * src/syn/xrm/Makefile.am: Bring up to date. * src/syn/xpctl/Makefile.am: Ditto. * src/syn/xrm/XRM-Properties.sdf: New. * tests/xrm/properties-in-xrm.xrm: New. * doc/user-guide.txt: Bring up to date. doc/user-guide.txt | 14 +++++++++ src/lib/xrm/pp/pp-xrm-to-box.str | 1 src/lib/xrm/pp/xrm-properties.meta | 1 src/lib/xrm/pp/xrm-properties.str | 9 +++++ src/str/properties-in-xrm.str | 56 +++++++++++++++++++++++++++++++++++++ src/str/xrm-front.str | 7 ++-- src/str/xrm-to-prism.str | 10 +++++- src/syn/xpctl/Makefile.am | 6 +++ src/syn/xrm/Makefile.am | 7 +++- src/syn/xrm/XRM-Main.sdf | 1 src/syn/xrm/XRM-Module.sdf | 6 +++ src/syn/xrm/XRM-Properties.sdf | 11 +++++++ tests/xrm/properties-in-xrm.xrm | 9 +++++ 13 files changed, 129 insertions(+), 9 deletions(-) Index: src/lib/xrm/pp/xrm-properties.meta --- src/lib/xrm/pp/xrm-properties.meta (revision 0) +++ src/lib/xrm/pp/xrm-properties.meta (revision 0) @@ -0,0 +1 @@ +Meta([Syntax("Stratego-Box")]) Index: src/lib/xrm/pp/pp-xrm-to-box.str --- src/lib/xrm/pp/pp-xrm-to-box.str (revision 73) +++ src/lib/xrm/pp/pp-xrm-to-box.str (working copy) @@ -24,6 +24,7 @@ xrm-meta-if xrm-arrays xrm-formula + xrm-properties strategies Index: src/lib/xrm/pp/xrm-properties.str --- src/lib/xrm/pp/xrm-properties.str (revision 0) +++ src/lib/xrm/pp/xrm-properties.str (revision 0) @@ -0,0 +1,9 @@ +module xrm-properties + +rules + prism-to-box: + Properties(properties-file-section) + -> V [ V is=2 [ KW["properties"] + ~*properties-file-section ] + KW["end"] + ] Index: src/str/xrm-to-prism.str --- src/str/xrm-to-prism.str (revision 73) +++ src/str/xrm-to-prism.str (working copy) @@ -37,6 +37,7 @@ array-decl-desugar builtin-rand log-timed + properties-in-xrm strategies @@ -85,7 +86,7 @@ * This must come AFTER collect-static-const-decl since we might need * to expand an arrays which rely on static const variables. */ - ; log-timed(topdown(try(array-decl-desugar); try(EvalStaticRand)) + ; log-timed(topdown(try(array-decl-desugar + EvalStaticRand)) | "Desugaring array declarations", 2) /* flatten nested lists */ @@ -126,7 +127,12 @@ ; if <is-module-file> start-symbol then /* re-order modules so that all declarations appear before commands */ - log-timed(ModulesFile(id, map(try(reorder-module-contents))) + log-timed-reentrant( + ModulesFile( + id, + map(try(reorder-module-contents + collect-properties)) + ) + ; write-properties | "Reordering module contents", 2) end Index: src/str/xrm-front.str --- src/str/xrm-front.str (revision 73) +++ src/str/xrm-front.str (working copy) @@ -63,6 +63,7 @@ + desugar-option + parse-pctl-option + seed-option + + prop-output-option /** checks the options are consistent */ check-options = @@ -156,9 +157,9 @@ seed-option = ArgOption("-s" + "--seed" , set-seed-option - , !HelpString("-s | --seed", "Set the random seed used for static_rand's - values. Default is the current UNIX - timestamp.") + , !HelpString("-s | --seed i", + "Set the random seed used for static_rand's values. + Default is the current UNIX timestamp.") ) set-seed-option = Index: src/str/properties-in-xrm.str --- src/str/properties-in-xrm.str (revision 0) +++ src/str/properties-in-xrm.str (revision 0) @@ -0,0 +1,56 @@ +/** +** This module is about embedded XPCTL in XRM. +*/ +module properties-in-xrm + +rules + + collect-properties: + Properties(properties-file-section) -> [] + where rules(SavedProperties:+ _ -> properties-file-section) + +strategies + + /** + ** Write properties found to the file specified by the --p-output (or -po) + ** switch. Issue a warning if the switch wasn't passed to xrm-front but we + ** have indeed collected properties (because in this case, they will be + ** discarded). + */ + write-properties = + where( + get-prop-output-option => prop-out-file + ; bagof-SavedProperties + ; reverse + ; if (!prop-out-file => []) then + if ?[_|_] then + warn-msg(|"Properties ignored: you didn't pass --p-output or -po.") + end + else + log-timed( + flatten-list + ; !PropertiesFile(<id>) + ; write-to => FILE(tmp-file) + ; <xtc-command(!"pp-pctl")> [ "-i", tmp-file + , "-o", prop-out-file + | <pass-verbose>() ] + | <concat-strings>["Writing properties to ", prop-out-file], 2) + end + ) // end of where + +strategies + + prop-output-option = + ArgOption("-po" + "--p-output" + , set-prop-output-option + , !HelpString("-po | --p-output f", + "Write properties found to the file f + (default: discard properties)") + ) + + set-prop-output-option = + <set-config> ("prop-output", <id>) + + get-prop-output-option = + <get-config> "prop-output" <+ ![] // empty list = don't output properties + // (discard them) Index: src/syn/xrm/XRM-Main.sdf --- src/syn/xrm/XRM-Main.sdf (revision 73) +++ src/syn/xrm/XRM-Main.sdf (working copy) @@ -12,3 +12,4 @@ XRM-Formula XRM-Constant XRM-Keywords + XRM-Properties Index: src/syn/xrm/XRM-Module.sdf --- src/syn/xrm/XRM-Module.sdf (revision 73) +++ src/syn/xrm/XRM-Module.sdf (working copy) @@ -6,7 +6,9 @@ %% EBNF Grammar: eXtended Modules %% DeclarationOrCommand ::= Declaration | Command - %% Module ::= "module" ArrayAccess Declaration* Command* "endmodule" + %% Module ::= + %% "module" ArrayAccess Declaration* Command* "endmodule" + %% | "module" ArrayAccess Declaration* Command* "end" sorts DeclarationOrCommand context-free syntax @@ -16,3 +18,5 @@ context-free syntax "module" ArrayAccess DeclarationOrCommand* "endmodule" -> Module {cons("Module")} + "module" ArrayAccess DeclarationOrCommand* "end" + -> Module {cons("Module")} Index: src/syn/xrm/Makefile.am --- src/syn/xrm/Makefile.am (revision 73) +++ src/syn/xrm/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail <sigoure.benoit@lrde.epita.fr> ## ## Started on Thu Apr 27 17:40:41 2006 SIGOURE Benoit -## Last update Sun Jun 11 02:39:02 2006 SIGOURE Benoit +## Last update Thu Jun 15 13:26:29 2006 SIGOURE Benoit ## include $(top_srcdir)/config/Transformers.mk @@ -17,7 +17,9 @@ 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/pctl \ + -I $(top_srcdir)/src/syn/xpctl nodist_pkgdata_DATA = \ XRM.def \ @@ -56,6 +58,7 @@ XRM-MetaIfExp.sdf \ XRM-MetaVars.sdf \ XRM-Module.sdf \ + XRM-Properties.sdf \ XRM-StartSymbols.sdf \ XRM-Update.sdf \ XRM.sdf Index: src/syn/xrm/XRM-Properties.sdf --- src/syn/xrm/XRM-Properties.sdf (revision 0) +++ src/syn/xrm/XRM-Properties.sdf (revision 0) @@ -0,0 +1,11 @@ +module XRM-Properties +imports + XPCTL +exports + + %% EBNF Grammar: XPCTL embeddings in XRM + %% ModulesFileSection ::= "properties" PropertiesFileSection* "end" + + context-free syntax + "properties" PropertiesFileSection* "end" + -> ModulesFileSection {cons("Properties")} Index: src/syn/xpctl/Makefile.am --- src/syn/xpctl/Makefile.am (revision 73) +++ src/syn/xpctl/Makefile.am (working copy) @@ -5,7 +5,7 @@ ## Mail <sigoure.benoit@lrde.epita.fr> ## ## Started on Sat Jun 10 00:17:31 2006 SIGOURE Benoit -## Last update Sun Jun 11 02:42:19 2006 SIGOURE Benoit +## Last update Thu Jun 15 13:25:48 2006 SIGOURE Benoit ## include $(top_srcdir)/config/Transformers.mk @@ -42,9 +42,13 @@ XPCTL-Prefixed.def SDFS = \ + StrategoXPCTL.sdf \ XPCTL-Main.sdf \ + XPCTL-MetaCongruences.sdf \ XPCTL-MetaFor.sdf \ XPCTL-MetaIf.sdf \ + XPCTL-MetaVars.sdf \ + XPCTL-PropertiesFile.sdf \ XPCTL-StartSymbols.sdf \ XPCTL.sdf Index: tests/xrm/properties-in-xrm.xrm --- tests/xrm/properties-in-xrm.xrm (revision 0) +++ tests/xrm/properties-in-xrm.xrm (revision 0) @@ -0,0 +1,9 @@ +module sample + x : [0..51] init 0; + [] true -> x'=static_rand(42); + [] true -> x'=rand(42); +endmodule + +properties + Pmin =? [ X x=42 ] +end Index: doc/user-guide.txt --- doc/user-guide.txt (revision 73) +++ doc/user-guide.txt (working copy) @@ -402,6 +402,20 @@ It is also possible to define formulas and parameterized formulas in XPCTL files. + If you wish, it is possible to specify properties directly in XRM files. + You can add property sections to your XRM files. Property sections can be + found everywhere a module declaration can be found. A property section is + specified as: + properties + // XPCTL code here + end + If you use property sections, you will need to pass an additional argument + to xrm-front to specify the PCTL property file where the options must be + saved. The option switch is --p-output f or -po f (where `f' is a path). + However, this option is not mandatory. If you specify property sections but + omit this switch, xrm-front will discard the properties and issue a warning + about that. + ************************ * Forthcoming features * ************************