https://svn.lrde.epita.fr/svn/xrm/trunk Index: ChangeLog from SIGOURE Benoit &lt;sigoure.benoit(a)lrde.epita.fr&gt; 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