[Projects] XRM 65: Add XRM-like formulas in eXtended PCTL.

https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit &lt;sigoure.benoit(a)lrde.epita.fr&gt; Add XRM-like formulas in eXtended PCTL. * src/lib/xpctl/pp/pp-xpctl-to-box.str: Import prism-formula. * src/str/xrm-to-prism.str: Add XRM-like formulas in eXtended PCTL. * src/str/collect-static-const-decl.str: Remove XRM-like formula definitions when gathering them. * src/syn/xrm/XRM-Formula.sdf: Hack imports so that this file can be imported from the XPCTL SDFs. * src/syn/xpctl/XPCTL-PropertiesFile.sdf: New. * src/syn/xpctl/XPCTL-Main.sdf: Import XPCTL-PropertiesFile. * doc/user-guide.txt: Add a NOTE about SdfChecker's warnings/errors. doc/user-guide.txt | 3 +++ src/lib/xpctl/pp/pp-xpctl-to-box.str | 1 + src/str/collect-static-const-decl.str | 15 ++++++++++++++- src/str/xrm-to-prism.str | 11 +++++++++-- src/syn/xpctl/XPCTL-Main.sdf | 1 + src/syn/xpctl/XPCTL-PropertiesFile.sdf | 12 ++++++++++++ src/syn/xrm/XRM-Formula.sdf | 8 ++++++-- 7 files changed, 46 insertions(+), 5 deletions(-) Index: src/lib/xpctl/pp/pp-xpctl-to-box.str --- src/lib/xpctl/pp/pp-xpctl-to-box.str (revision 64) +++ src/lib/xpctl/pp/pp-xpctl-to-box.str (working copy) @@ -6,6 +6,7 @@ XRM // signature (required since we use parts of the language) prism-constant prism-expression + prism-formula xpctl-parenthesize pctl-properties-file pctl-label Index: src/str/xrm-to-prism.str --- src/str/xrm-to-prism.str (revision 64) +++ src/str/xrm-to-prism.str (working copy) @@ -54,7 +54,7 @@ ; try(collect-formulas))) else PropertiesFile(map(try(collect-static-const-decl) - ; try(collect-formulas))) + ; try(collect-and-remove-formulas))) end | "Collecting static const and formulas", 2) @@ -104,8 +104,15 @@ /* remove array accesses: x[i] -> x_i */ // FIXME: can we make this more efficient than a complete bottomup? - ; log-timed(bottomup(try(flatten-array-access)) + ; if <is-module-file> start-symbol then + log-timed(bottomup(try(flatten-array-access)) | "Desugaring array accesses", 2) + else + /* NOTE: for XPCTL files we also need to expand use of XRM-Formulas + * because the original definition has been removed. */ + log-timed(innermost(flatten-array-access <+ ExpandFormulas) + | "Desugaring array accesses", 2) + end ; if <is-module-file> start-symbol then /* re-order modules so that all declarations appear before commands */ Index: src/str/collect-static-const-decl.str --- src/str/collect-static-const-decl.str (revision 64) +++ src/str/collect-static-const-decl.str (working copy) @@ -44,7 +44,7 @@ ; !v'{Type("bool")} => v) ; rules(ExpandStaticConsts: idf -> v) -rules +strategies collect-formulas = //?|[ formula x = e; ]| @@ -57,6 +57,19 @@ end ; rules(ExpandFormulas: x -> e) +rules + + collect-and-remove-formulas: + //?|[ formula x = e; ]| + FormulaDef(x, e) -> [] + where if <ExpandStaticConsts> x then + cannot-redefine-static-const(|x) + end + ; if <ExpandFormulas> x then + cannot-redefine-formula(|x) + end + ; rules(ExpandFormulas: x -> e) + strategies cannot-redefine-static-const(|idf) = Index: src/syn/xrm/XRM-Formula.sdf --- src/syn/xrm/XRM-Formula.sdf (revision 64) +++ src/syn/xrm/XRM-Formula.sdf (working copy) @@ -1,6 +1,10 @@ module XRM-Formula -imports PRISM-to-XRM -exports +imports + XRM-Expression + XRM-Arrays +%%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: Extended Formulas %% FormulaDef ::= "formula" ArrayAccess "=" Expression ";" Index: src/syn/xpctl/XPCTL-PropertiesFile.sdf --- src/syn/xpctl/XPCTL-PropertiesFile.sdf (revision 0) +++ src/syn/xpctl/XPCTL-PropertiesFile.sdf (revision 0) @@ -0,0 +1,12 @@ +module XPCTL-PropertiesFile +imports + PRISM-Formula + XRM-Formula +exports + + %% EBNF Grammar: eXtended PCTL top level stuff + %% + %% PropertiesFileSection ::= FormulaDef + + context-free syntax + FormulaDef -> PropertiesFileSection Index: src/syn/xpctl/XPCTL-Main.sdf --- src/syn/xpctl/XPCTL-Main.sdf (revision 64) +++ src/syn/xpctl/XPCTL-Main.sdf (working copy) @@ -1,6 +1,7 @@ module XPCTL-Main imports PCTL-Main + XPCTL-PropertiesFile XPCTL-MetaFor XPCTL-MetaIf XRM-Expression Index: doc/user-guide.txt --- doc/user-guide.txt (revision 64) +++ doc/user-guide.txt (working copy) @@ -61,6 +61,9 @@ /usr/lib/pkgconfig/sdf2-bundle.pc /usr/lib/pkgconfig/stratego*.pc o Then simply type `make all check' then `make install' + o NOTE: If you see many warnings/errors from SdfChecker during + compilation, don't worry, it's normal (unless it actually stops the + build) *************************** * Tools provided with XRM *