https://svn.lrde.epita.fr/svn/xrm/trunk
Index: ChangeLog
from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr>
Fix some mistakes in the doc.
* doc/user-guide.txt: Here.
user-guide.txt | 16 +++++++++++-----
1 file changed, 11 insertions(+), 5 deletions(-)
Index: doc/user-guide.txt
--- doc/user-guide.txt (revision 89)
+++ doc/user-guide.txt (working copy)
@@ -368,6 +368,8 @@
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 NOTE: It is possible to specify a seed with xrm-front's
+ -s | --seed option.
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
@@ -467,7 +469,8 @@
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.
+ done please review the TODO file. You can also review the trac
+ located at http://xrm.lrde.org/
- 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.)
@@ -525,6 +528,9 @@
Pmin=? [ true U<=(k) (1)+1=1 ]
- Probably many other things. (run make check and see the tests that fail).
+ For a complete list of bugs, you should review the trac located at
+ http://xrm.lrde.org/
+
**************************
* Internal Documentation *
**************************
@@ -669,8 +675,8 @@
At this time each random variable is controlled by a separate module
generated by xrm-front. This module is stored in a DR named RandGenModules.
- The second pass collects static const declarations, formula (and
- parameterized) declarations. For property files, the formulas are removed
+ The second pass collects static const declarations, formulas and
+ parameterized formulas. For property files, the formulas are removed
when they are collected (because they are not allowed in standard property
files). Parameterized formulas are always removed once they are collected
because they do not exist in the base languages. These declarations are
@@ -702,7 +708,7 @@
generation). Once again, this pass uses a hand-made traversal and features:
evaluation of static ifs, lazy evaluation of operator `&' and operator `|'
(so that the user can rely on them to prevent invalid code from being
- evaluated, eg: x > 0 && a[x] to prevent an invalid array access). For loops
+ evaluated, eg: x > 0 & a[x] to prevent an invalid array access). For loops
are unrolled. Calls to parameterized are inlined. When a call to a
parameterized formula is inlined, we must re-start the pass on the code
inlined.
@@ -752,7 +758,7 @@
In the end, we can now re-order the content of the modules. Indeed, in XRM
we allow the declarations and commands to be freely intertwined whereas in
PRISM declarations must always come before the commands. This is done
- using a scoped DR. We traverse all the Modules and collect declarations and
+ using a scoped DR. We traverse all the modules and collect declarations and
commands in DRs (respectively CommandList and DeclarationList). Once we
have them all we can easily re-construct the module with the declarations
first, followed by the commands.
https://svn.lrde.epita.fr/svn/xrm/trunk
Index: ChangeLog
from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr>
Add a missing channel in the doc.
* doc/user-guide.txt (install with Nix): Add the nixpkgs channel.
user-guide.txt | 1 +
1 file changed, 1 insertion(+)
Index: doc/user-guide.txt
--- doc/user-guide.txt (revision 88)
+++ doc/user-guide.txt (working copy)
@@ -58,6 +58,7 @@
/!\ Download nix-X.YYpreZZZZ not nixpkgs-X.YYpreZZZZ.
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/nix/channels-v3/nixpkgs-unstable
$ nix-channel --add http://nix.cs.uu.nl/dist/stratego/channels-v3/strategoxt-unstable
$ nix-channel --update
$ nix-env --install aterm sdf2-bundle strategoxt
https://svn.lrde.epita.fr/svn/xrm/trunk
Index: ChangeLog
from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr>
Add an internal documentation.
* src/str/xrm-front.str: Fix comments.
* doc/user-guide.txt: Add an internal documentation.
doc/user-guide.txt | 230 ++++++++++++++++++++++++++++++++++++++++++++++++--
src/str/xrm-front.str | 4
2 files changed, 223 insertions(+), 11 deletions(-)
Index: src/str/xrm-front.str
--- src/str/xrm-front.str (revision 87)
+++ src/str/xrm-front.str (working copy)
@@ -36,13 +36,13 @@
if must-parse-pctl then // output PCTL source
log-timed(xtc-transform(!"pp-pctl", pass-verbose)
| "pretty printed PCTL code", 2)
- else // output PRISM source
+ else // output PRISM source (default)
log-timed(xtc-transform(!"pp-prism", pass-verbose)
| "pretty printed PRISM code", 2)
end
end
end
- /* default: if we don't get inside the previous if, we will output
+ /* if we don't get inside the previous if, we will output
* binary ATerms. */
/** pipeline of transformations performed by xrm-front */
Index: doc/user-guide.txt
--- doc/user-guide.txt (revision 87)
+++ doc/user-guide.txt (working copy)
@@ -27,7 +27,7 @@
The goal of eXtended Reactive Modules is to provide a comprehensive
solution to these problems by adding syntactic extensions to the PRISM
-language. XRM comes with a set of tools with enables the programmer to work
+language. XRM comes with a set of tools which enable the programmer to work
with the extended version of the PRISM language. The main tool, xrm-front,
will compile an XRM source file (written in the extended language) in a PRISM
source file (the base language, as used by the tools PRISM and APMC).
@@ -48,16 +48,18 @@
o OS with executable stack.
o ATerm 2.4.2 or newer.
o SDF2-Bundle 2.3.4 or newer.
+ o GNU make.
- 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).
+ /!\ Download nix-X.YYpreZZZZ not nixpkgs-X.YYpreZZZZ.
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 -u '*'
+ $ nix-channel --update
$ nix-env --install aterm sdf2-bundle strategoxt
There you are!
Add the following line to your .bashrc/.zshrc:
@@ -137,7 +139,7 @@
copy is available in the prism/ directory).
The XRM language is 100% PRISM compliant and only offers extension to the
- language.
+ base language.
Many people used to overcome the limitations of the PRISM language by
generating PRISM code using scripts (Shell scripts, M4 scripts, etc...).
@@ -451,7 +453,7 @@
// 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
+ to xrm-front to specify the PCTL property file where the properties 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
@@ -536,14 +538,224 @@
# General design
--------------
-
- // FIXME
+ This sections explains the general design used when developing XRM.
+ The sources are located under the src/ folder. They are divided in 5
+ sections:
+ * src/lib: Contains strategies/code exported in libraries linked with
+ the tools. In fact (at this time) XRM doesn't use any
+ library but the code under this path should be exported
+ through shared and static libraries.
+ * src/lib/native: Contains C code used by Stratego code (with `prim').
+ Actually this code features several extensions used to
+ manipulate float values in Stratego. This was implemented in
+ C because it wasn't available in stratego-lib and because
+ doing the same work would be a pain in C.
+ This code also provide a random number generator.
+ * src/lib/<lang>/pp: Where <lang> is {pctl,prism,xpctl,xrm}. Contains
+ the pretty-printing strategies used by the pretty printers.
+ These strategies are meant to be available in libraries but
+ at this time they are simply imported by the
+ pretty-printers. Exporting them in libraries would reduce
+ compilation time. They should rather be exported in static
+ libraries (if possible) because dynamic libraries have
+ inconvenient: the .so must be installed and available in
+ the LD_LIBRARY_PATH (or must be installed in standard
+ paths). Installing one dynamic library per pretty-printer
+ does not seem quite attractive.
+ * src/sig: Contains nothing. This is where signatures for the 4
+ languages (pctl, prism, xpctl, xrm) will be generated (under
+ the build dir)
+ * src/str: Contains the Stratego code used by xrm-front.
+ * src/syn/<lang>: Contains the SDF grammar of the language <lang>. Each
+ grammar has Stratego embeddings (for concrete syntax)
+ defined in Stratego<LANG>.sdf and optionally
+ <LANG>-MetaCongruences.sdf and <LANG>-MetaVars.sdf.
+ Renamed version of each grammar are generated during the
+ build so that the grammars can easily be assimilated within
+ other host languages later on.
+ * src/tools: Contains Stratego sources for the pretty-printers and
+ parsers (which are registered as XTC components).
o The build system
- o How the tools (parsers, pretty printers...) are made, XTC
- o FIXME
+ ----------------
+ XRM use the autotools to set up the build system. It also uses the
+ Makefile provided by autoxt and Transformers' Makefile. The configure
+ script tries to guess the correct value for PKG_CONFIG_PATH if it is
+ not provided by looking for common locations where Stratego/XT is
+ installed by Nix. Many GNU make extensions are used by the Makefiles.
+ Parallel builds work and are encouraged.
+
+ o Creating tools with XTC
+ -----------------------
+ XRM uses XTC-registered components. For the documentation of XTC see
+ the chapters 28 and 29 of the Stratego/XT manual
+ (http://nix.cs.uu.nl/dist/stratego/strategoxt-manual-unstable-latest/manual/…,
+ http://nix.cs.uu.nl/dist/stratego/strategoxt-manual-unstable-latest/manual/…).
+ Basically, XTC components are simply applications or files which are
+ registered by a program called `xtc'. This program creates a file where
+ registered components are listed (the repository). When a component is
+ registered in the repository, its name, version and path are saved.
+ This is useful so that you can develop tiny applications and call them
+ one after the other in a pipeline. Calling them from Stratego is made
+ easy because the Stratego programs know where the XTC repository is and
+ it can query that repository to find the auxiliary tools it needs. For
+ instance one could register ls, grep and wc in an XTC repository. Then
+ one could invoke them from a Stratego program one after the other in
+ order to simulate the command `ls -l | grep rwx | wc -l` for instance.
+ Note that XTC repositories are in fact ATerms and you can display them
+ with pp-aterm.
+ For instance this is used by parsers which need to invoke sglr with the
+ correct parse table in argument. The parse table is generated somewhere
+ and is registered in the XTC repository. The parser looks up the
+ location of the parse table through the repository and then invoke sglr
+ with the right path to the parse table.
+ However, this has a disadvantage: Invoking XTC components is quite
+ inefficient. This is because when you do this, the current term is
+ saved in a temporary file under /tmp. When the current term is quite
+ large this can produce files from several hundred mega-bytes up to
+ several giga-bytes. Then the XTC component you invoked is called with
+ that temporary file as input (-i) and another new temporary file as
+ output (-o). Once it has finished, the current processes reloads its
+ current term from the temporary file where the XTC component sent its
+ output. This leads to many i/o operations on disk which tend to be
+ quite slow. That's why XRM tries to avoid to use XTC for external
+ processes as much as possible. But since we still want to be modular,
+ instead of using XTC components, we use external libraries. At this
+ time XRM doesn't use libraries because it was easier to import the
+ libraries required than to export them through libraries which would
+ then be linked with the binary. However this makes the compilation time
+ longer. We should really consider exporting common things in external
+ libraries.
+
+ The --help and --about options are handled using tool-doc
+ (https://svn.cs.uu.nl:12443/repos/StrategoXT/strategoxt/trunk/stratego-regul…).
+ The pretty-printers directly include the strategies they need (the
+ pretty-printing rules are written in Stratego under src/lib/<lang>/pp).
+ This enables them to be stand-alone, they can pretty-print without
+ using intermediate files. They also use libstratego-gpp which is quite
+ recent. This enables them to use abox-to-text without to call an
+ external XTC component and go through intermediate temporary files.
# xrm-front's pipeline
--------------------
- // FIXME
+ In this section we will review the pipeline of xrm-front. We will explain
+ the different passes of the pipeline, how the dynamic rules are used and
+ how the transformations are performed.
+
+ Everything begins in src/str/xrm-front.str. The first thing performed by
+ xrm-front is to check whether the options it was invoked with are
+ consistent. For instance, if the user invokes xrm-front with the flags -b
+ (request output in binary ATerm format) and -P (request output in
+ pretty-printed ATerm format) the switch -P is ignored and a warning is
+ issued. In former version of xrm-front, there were more conflicting options.
+
+ Then xrm-front parses its input files with the correct parser. When the
+ switch -p (or --pctl) is provided, XRM must parse XPCTL source code whereas
+ it parses XRM source code by default. The parsing is performed by an
+ external XTC component. It would be useful to use library-based parser
+ instead to improve performances. Then the strategy xrm-front-pipeline is
+ invoked.
+
+ This where the transformations begin. The real pipeline can be found in
+ src/str/xrm-to-prism.str.
+
+ The first pass removes the XRM sugar. This is a simple innermost traversal
+ where basic transformations rules are applied to remove what is merely
+ simple syntactic sugar. We also use this pass to catch calls to the XRM
+ builtin rand in property files (which is not allowed). In XRM files, these
+ calls are simply replaced by a variable which will be the random variable.
+ At this time each random variable is controlled by a separate module
+ generated by xrm-front. This module is stored in a DR named RandGenModules.
+
+ The second pass collects static const declarations, formula (and
+ parameterized) declarations. For property files, the formulas are removed
+ when they are collected (because they are not allowed in standard property
+ files). Parameterized formulas are always removed once they are collected
+ because they do not exist in the base languages. These declarations are
+ collected in dynamic rules as follows:
+ * ExpandStaticConsts: id -> value
+ * ExpandFormulas: id -> value
+ * ExpandPFormulas: PFormulaCall(name, a*) -> e
+ this DR rewrites a call to the parameterized formula `name' (invoked
+ with the arguments `a*') to `e' which is the inlined version of the
+ formula `name' with its formal parameters replaced by the parameters
+ provided in `a*'.
+
+ The third pass of xrm-front is to check that meta-vars are used correctly.
+ The whole code is traversed using a hand-crafted traversal that collects
+ the declarations of meta-vars (using the appropriate scopes). For instance,
+ when the traversal enters a for loop, it registers the meta-var used to
+ iterate in the loop in a scoped DR. Several things must be evaluable down
+ to simple integers at compile time (such as array subscripts or the
+ `from' or `to' of a for loop for instance. Indeed if you can't evaluate
+ the latter at compile time, how can you unroll the loop if you don't know
+ how many iterations it has to go through?). Once we know what are the
+ meta-vars (as well as static consts, formulas etc.), we can easily check
+ whether an expression is evaluable as a literal value at compile time. If
+ the expression contains only literals and identifiers known to be evaluable
+ at compile time (such as static consts and meta-vars for instance) then the
+ expression itself is evaluable at compile time.
+
+ Then an important pass starts: the meta-code is evaluated (leading to code
+ generation). Once again, this pass uses a hand-made traversal and features:
+ evaluation of static ifs, lazy evaluation of operator `&' and operator `|'
+ (so that the user can rely on them to prevent invalid code from being
+ evaluated, eg: x > 0 && a[x] to prevent an invalid array access). For loops
+ are unrolled. Calls to parameterized are inlined. When a call to a
+ parameterized formula is inlined, we must re-start the pass on the code
+ inlined.
+
+ The fifth pass consists of removal of array declarations, evaluation of
+ calls to the XRM builtin static_rand and collection of non-array local
+ variable declarations. This is 3 different things but they
+ are combined together to reduce the number of traversals. Array
+ declarations are rewritten as declarations of lists of variables. xrm-front
+ ensures that array declarations are not overlapping with each other.
+ Each array declaration is recorded in the DR DeclaredArrays which maps an
+ Identifier(idf) -> aa-list where `aa-list' is the list of array subscript
+ declared for that array. When an array is declared in multiple parts, each
+ part is added in the same entry of DeclaredArrays (we first fetch the parts
+ previously declared, check that they don't overlap with the parts being
+ declared, and if they don't, we concatenate them and save them back in the
+ DR). This part of the code might be a bit hard to read because an abstract
+ factory is used to build declaration lists resulting of array declarations
+ and this is a bit hard to follow. Hopefully the numerous comments in the
+ file will help the reader to understand how the rewriting is performed.
+ Non-array declarations are also collected in a DR named DeclaredIdentifers
+ which maps an identifier to some information about it (such as its type,
+ its definition range, its initial value). These information are gathered
+ for the type-checking pass. Note that type information of variables
+ declared in arrays are not yet gathered.
+
+ So now, array declarations have been rewritten as declaration lists. This
+ introduces several unwanted nested lists in the AST which are then removed
+ using `flatten-list'.
+
+ Then comes the type-checking pass. At this time, this pass is quite basic
+ and only checks that array subscripts do not lead to out of bound array
+ accesses. We can easily do this thanks to the DR DeclaredArrays which maps
+ an identifier to the dimensions declared for that array. The pass also
+ ensures that all array accesses are made on declared arrays.
+
+ Then, we paste the module generated by the calls to the rand builtin
+ (which were saved in the DR RandGenModules) at the end of the file.
+
+ Now we can remove all array accesses. This is done by flattening them, eg
+ x[1][2][3] is rewritten as x_1_2_3. For property files, we also use this
+ pass to expand all non-parameterized formulas since their expansions wasn't
+ forced by any previous pass. We must force the expansion of
+ non-parameterized formulas in property files because they are not allowed
+ in the base language.
+
+ In the end, we can now re-order the content of the modules. Indeed, in XRM
+ we allow the declarations and commands to be freely intertwined whereas in
+ PRISM declarations must always come before the commands. This is done
+ using a scoped DR. We traverse all the Modules and collect declarations and
+ commands in DRs (respectively CommandList and DeclarationList). Once we
+ have them all we can easily re-construct the module with the declarations
+ first, followed by the commands.
+
+ The resulting AST is further desugared if the -D | --desugar switch was
+ provided, then it is pretty-printed in the format required by the command
+ line (default: PRISM code).
https://svn.lrde.epita.fr/svn/xrm/trunk
Index: ChangeLog
from SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr>
Update documentation.
* doc/user-guide.txt: Update.
user-guide.txt | 132 +++++++++++++++++++++++++++++++++++++++++++++------------
1 file changed, 106 insertions(+), 26 deletions(-)
Index: doc/user-guide.txt
--- doc/user-guide.txt (revision 86)
+++ doc/user-guide.txt (working copy)
@@ -14,8 +14,28 @@
* Introduction *
****************
- // FIXME: An introduction about PRISM and what is/isn't XRM is missing
- // here.
+ Reactive Modules is a formal model used to represent synchronous and
+asynchronous components of a system. It has never really been used as a
+practical computer language but it is a formalism used to _describe_ systems.
+ PRISM is a tool widely used in probabilistic model checking. It features
+the PRISM language which is highly based on the Reactive Modules formalism.
+This language has been found to have several limitations when it comes to
+large systems containing tens or hundreds of modules. It does not enable to
+easily parameterize the model so that it can be checked with different
+parameters. This comes from the fact that this language was simply designed
+to _describe_ systems, not to actually program them.
+
+ The goal of eXtended Reactive Modules is to provide a comprehensive
+solution to these problems by adding syntactic extensions to the PRISM
+language. XRM comes with a set of tools with enables the programmer to work
+with the extended version of the PRISM language. The main tool, xrm-front,
+will compile an XRM source file (written in the extended language) in a PRISM
+source file (the base language, as used by the tools PRISM and APMC).
+
+ In this document, we will describe how to use the XRM package, and what are
+the syntactic extensions featured. We assume that the reader is comfortable
+with model checking, with the Reactive Modules formalism and especially with
+the PRISM language. If not, please read [AH99] or PRISM's Manual.
****************
* Installation *
@@ -25,7 +45,7 @@
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 OS with executable stack.
o ATerm 2.4.2 or newer.
o SDF2-Bundle 2.3.4 or newer.
@@ -33,7 +53,7 @@
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).
+ 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
@@ -72,9 +92,9 @@
- 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-prism: Parses a PRISM source code and yield an AST in ATerms.
- parse-xrm, parse-pctl, parse-xpctl: Ditto with XRM/PCTL/XPCTL source code.
- - pp-prism: Pretty print ("unparse") a PRISM AST as PRISM source code.
+ - pp-prism: Pretty prints ("unparses") a PRISM AST as PRISM source code.
- pp-xrm, pp-pctl, pp-xpctl: Ditto with XRM/PCTL/XPCTL source code.
*******************
@@ -110,8 +130,8 @@
* The XRM language *
********************
- # Introduction
- ------------
+ # Foreword
+ --------
The specification of the base language is documented in PRISM's manual (a
copy is available in the prism/ directory).
@@ -119,10 +139,35 @@
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.
+ Many people used to overcome the limitations of the PRISM language by
+ generating PRISM code using scripts (Shell scripts, M4 scripts, etc...).
+ They came to this kind of solution because they needed to generate large
+ systems which is almost impossible to do by hand. Indeed, most of the time,
+ a system is made of several identical modules which are interacting with
+ each other. Traditionally, this is done using module renaming.
+ Nevertheless, it is still impossible to easily parameterize the number of
+ modules in the system. Moreover when a module is slightly different than
+ the others, it is impossible to use module renaming. Thus, PRISM files are
+ usually highly redundant and hard to write by hand. That's why it is so
+ common to generate PRISM code using scripts.
+
+ However, scripts are generally not aware of the PRISM code they are
+ generating. It is easy to generate invalid code. In this case, one has to
+ find where is the error in the script and fix it. The advantage of using a
+ compiler such as xrm-front becomes clear: a compiler doesn't carry around
+ strings, it works with an AST (Abstract Syntax Tree) generated by a parser
+ itself guided by a grammar. Most error will be detected and reported at
+ parse time or compile time, making the developing process more reliable.
+
+ Since the main concern is about code generation, XRM enables a form of
+ meta-programming. For instance, the number of modules in a system could be
+ stored in a variable and a for loop could be used to generate them. For
+ loops don't exist in PRISM. In order to transform an XRM for loop in a
+ standard PRISM code, we have to unroll the loop, which leads to code
+ generation (meta-programming).
+
+ We will now see what are the syntactic extensions featured by XRM and how
+ to use them.
# XRM Modules
-----------
@@ -133,8 +178,8 @@
The following module is valid in XRM:
module OutOfOrder
- [] x=0 -> (x'=1);
- x : [0..1] init 0;
+ [] x=0 -> (x'=1); // command
+ x : [0..1] init 0; // declaration
endmodule
The last step of xrm-front's pipeline is to group all declarations together
@@ -144,7 +189,8 @@
# XRM Expressions
---------------
- o XRM has arrays (see below). Array accesses are expressions.
+ o XRM has arrays (see below). Array accesses (or subscripted arrays, eg:
+ x[3]) 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.
o It is possible to disambiguate a double value from an integer by
@@ -159,26 +205,34 @@
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:
+ o Arrays are declared with ranges, eg:
x[0..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[0..3][0..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:
+ For multidimensional arrays 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:
+ But in this case accessing x[0] for example doesn't make sense. If you
+ want to access x[0] you have to declare it using a 1-dimension array.
+ This array can coexist with x[][].
+ o It is possible to use any kind of range to declare an array, 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]
The Cartesian product of all the dimensions of the array is used to
compute the set of accessible variables.
+ o Arrays can be declared in different parts, eg:
+ x[0..3] : bool init true;
+ x[4..7] : [1..5] init 2;
+ In this case, x[0] through x[3] contains a boolean value whereas x[4]
+ through x[7] contains an integer value between 1 and 5 included.
+ Note that in this case, multiple declaration must not overlap, eg:
+ x[0..4] : bool init true;
+ x[4..7] : [1..5] init 2; // x[4] overlaps with the previous declaration!
+ This is will be caught as an error by xrm-front.
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
@@ -200,8 +254,8 @@
was automatically desugared to:
const int array[0..N-1];
This is no longer true since XRM 1.1, one must now explicitly write
- const int array[0..N-1] and const int array[N] leads to the declaration
- of a single variable, that is, the Nth variable of the array.
+ const int array[0..N-1]. Since then, const int array[N] leads to the
+ declaration of a single variable, that is, the Nth variable of the array.
+ TODO: Array accesses with dynamic subscripts.
# XRM Meta-code
@@ -290,7 +344,7 @@
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.
+ false because this value is 0 when used with a precision of 10^-7.
# XRM builtins
------------
@@ -467,3 +521,29 @@
In this case, add a couple of parenthesizes to remove the ambiguity:
Pmin=? [ true U<=(k) (1)+1=1 ]
- Probably many other things. (run make check and see the tests that fail).
+
+ **************************
+ * Internal Documentation *
+ **************************
+
+ # Introduction
+ ------------
+
+ This part of the documentation aims at explaining the internals of XRM, how
+ it has been developed and how it works. This is only useful if you intend
+ to further develop XRM or to understand the underlying code. This could
+ also be useful if you're learning Stratego.
+
+ # General design
+ --------------
+
+ // FIXME
+
+ o The build system
+ o How the tools (parsers, pretty printers...) are made, XTC
+ o FIXME
+
+ # xrm-front's pipeline
+ --------------------
+
+ // FIXME
"Nicolas Pouillard" <nicolas.pouillard(a)gmail.com> writes:
> Nan mais je connais le pb c'est assez complexe, c'est peut etre pas grand
> chose par example il cherche Datas et il est dans le contexte
> Commands::Runners::Runner
> et il s'arrete sur Commands::Runners::Runner::Datas ce qui est faut,
> il doit continuer et
> tester Commands::Runners::Datas puis Commands::Datas qui est correcte.
> Mais la j'ai mon rapport sur le feu et je n'ai pas le temps de voir.
Reminder. ;)
On 2006-06-21, SIGOURE Benoit <sigoure.benoit(a)lrde.epita.fr> wrote:
> * tests/xrm/rivf.xrm: Fix.
>
> tests/xrm/rivf.xrm | 2 +-
>
> Index: tests/xrm/rivf.xrm
> --- tests/xrm/rivf.xrm (revision 82)
> +++ tests/xrm/rivf.xrm (working copy)
> @@ -100,6 +100,6 @@
> properties
> for T from 0 to 1200 step 100 do
> // Alarmed triggered before instant T?
> - P =? [ true U (t <= 0 & true) ]
> + P =? [ true U (t <= T & boundary_broadcasts) ]
> end
> end
>
Bon je sais vraiment pas ce qui se passe mais ça marche pas. J'ai essaye avec
une grille 2x2 et xrm-front ne termine pas même après avoir attendu plus de
45min. Y'a forcement quelque chose qui fait que ça termine pas.
Donc j'ai fait en sorte d'afficher un message a chaque fois qu'un appel a une
formule paramétrée était inliné et au bout de quelques seconde je vois plus
de messages... ce qui veut donc bien dire que la récursion s'arrête. Mais
alors pourquoi ça continue de tourner pendant aussi longtemps? La je
comprends pas... mais va falloir fixer ça rapidement.
:(
--
SIGOURE Benoit aka Tsuna
_____
/EPITA\ Promo 2008.CSI Rock & tRoll
