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