- 17 Mar, 2010 25 commits
-
-
Erwan Jahier authored
Parent-Version: 0.89 Version-Log: source/parse_env.ml: Allow arbitrary expression in the lhs of boolean compararison operators (<,>,=,>=,<=). Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.87 Version-Log: Turn around the bug in sim2chro where it can not read floats such like 4. (pb cause there is not digits...). Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.83 Version-Log: empty Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.79 Version-Log: source/control.ml: source/parse_env.ml: Add a new ctrl expr (set_between) to let one set the value of a CE var in such a way that it is backtracable within an interval. One rational is that it let ones code infinite loops that can be exited when the formula is false. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.77 Version-Log: source/parse_env.ml: Fix a bug where empty ctrl expr labels were causing a parse error. source/control.ml,mli: Add those files to the project as should have been done for a while... Do not handle infinite values for ctrl expr counters anymore as it is useless (and not so easy to be handled properly). Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.68 Version-Log: wtree.ml,mli: (deleted) automa.ml,mli: (new files) control.ml,mli: (new files) Replace the [wtree] module by an [automata] module, that basically does the same job, but in a different way. Namely, it no more uses the [wtree] DS to use [graph]s instead. Indeed, the product of wtrees introduces some problems, in particular to ensure its correctness wrt to the automata run concurrently. Now, everything a dead-simple wrt product: we simply perform a quasi-classical automata product (well, at least, much closer from a classical product, cf paper). The way loop counters are handled has also changed. Now, counters are handled via expressions of a simple arithmetic language that basically lets one initialise a variable to an exact or a random value (uniform or normal draw) and decrement it. Arcs are now labelled by a formula plus 2 expressions of that mini-language (no more weigth nor cpt_init stuff). The 1st expression is evaluated during the draw, basically performs any operations on counters, and returns a positive int that is used as the formula weigth. The second expression (a kind of post-condition) is evaluated if its arc is the one that has been elected to perform the step. At several locations long lines (< 80) are reindented. parse_env.ml: In the ima format, IfThenElseExpr becomes IfThenElseNum. Also, parse list more cleanly. graph.ml,mli: Add a function that test whether a transition is in the graph. Do not sort list of transitions anymore (what was the point?). Also do not sort nodes in any way. show_env_env.ml,mli: Abstract away nodes and arcs data types (so that I can display Automata graphs). rename generate_env_graph into ima_to_dot. lurette.ml: ima_exe.ml: Fix a bug where bbd table were filled by asserted non regression expr. lurette.ml: Fix a bug where incorrect data was sent to sim2chro (ie, the output of the previous step instead of the ones of the current step. env_state.ml: solver.ml: gne.ml: Fix a performance bug where I was storing formula indexes even if they were depending on inputs or pre, which is stupid as they generally won't be used again. In order to fix that, I introduced new atomic_formula <-> indexes table to stote the ones that do not depend on inputs apart. It was also necassery to propogate the <<depend on pre>> flag inside Gne.gn_expr (which i renamed Gne.t BTW). Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.63 Version-Log: Add support for loop Gauss. Fix a bug in the handling of loops where lurette (and ima_exe) was stopping whenever the body of a loop contains no satisfiable formula whereas the endLoop branch should be taken in that case. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.60 Version-Log: Add support for handling loops. This is based on the use of dynamic weigths. The idea is to compute the dynamic weigths before the trees are constructed. Add a --show-aut option for ima_exe. Also, Add the command lise args hashed to the end of the name of the dot file that is used to visualize the ima file. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.59 Version-Log: Add an make release rule to package a lurette.tgz ready to distribute. Create a bin dir where all the biniries (except lurette) will live. Create a show_ima executable that lets one (Yvan actually) display .env (or .ima) files off-line. Move read_env_state from env.ml to env_state.ml. Add support for lutin loops in the parser (not yet handled tough). In gen_stubs.ml, try to automatically call lustre whenever no C poc file exists for the invoked program. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.58 Version-Log: Change the env parser so that : 1) lists can end with a semi-column 2) We can deal with dynamic weigths (for loops). The support for handling them is not written yet tough. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.55 Version-Log: Change the env format sligthly again : - adds the arcs and node numbers. - allows lists to end by a ; - add xor's Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.54 Version-Log: Allow equalities between formula by translating [A = B] into [Or(And(A,B), And(Not(A), Not(B)))]. Fix a bug where lurette had a bad behaviour whenever a toss was performed on a domain which size was bigger than max_int or max_float. Fix a bug where lurette was not handling env with both boolean and numerical as output vars. Also add a few comments in solver.ml along the way. Adds a local bool as an output of heater in order to test the fix above. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.50 Version-Log: Change the way pre are translated in the .env file. Now instead of writting "_pre2toto", one writes "pre(2,toto)". But internally, it is handled the same way as before (i.e., the first thing I do when parsing the env file is to transform "pre(2,toto)" into "_pre2toto" (it makes the hangling of pre vars much more homogeneous with the way the other vars are handled. Also fix a bug where it was not possible to have a pre on input vars because the update_pre was failing to proceed quietly whenever one of its var was not computable because its pre does have a value. Also give an appropriate error message whenever the user wrongly use a pre on a var that can not be computed. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.49 Version-Log: Add the possibility to put pragmas in the .env files. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.48 Version-Log: Clean up a little bit the ima format to make it sipler to parse and to avoid reducing the naming space as much as possible. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.47 Version-Log: Add support for (boolean and numeric) if-then-else. Remove the eval.ml module as the replacement of pre and input vars is now done in Solver.formula_to_bdd. Add a new module gne.ml that provides a garded normal expressions data structure that is used to handle if-then-elses. Also introduce a new field to env_state called bdd_tbl_global which is used to cache the result of formula_to_bdd for bdds that do not depend on pre nor input vars. The field bdd_tbl which cache the other reults is now cleared at each step because it is useless to store results that depends on pre and inputs. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.43 Version-Log: Add the possibility to specify the min lower and upper bounds in the env automata for output and local vars. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.40 Version-Log: Change sligthly the ima format to make it more consistent. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.39 Version-Log: Change the naming convention of prevars. Now, _pretoto is noted _pre1toto, and _pre_pre_pretoto is noted _pre3toto. Also fix a bug in the default initialization of ranges : min_float is the smallest positive float, not the smallet one !! Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.37 Version-Log: With this change, lurette is now able to handle numeric variables over intervals ! Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.35 Version-Log: Add support to handle numerical contraints. The numerical stuff is untested, but the boolean part works as before. source/rnumsolver.mli: source/rnumsolver.ml: New files implementing a numeric solver based on intervals. source/*.ml: Change the var_type type from a string to a sum type containing the lower and upper bounds of numeric domains. Do not maintain a var_name to index correspondance, but a formula to index one. This is to be able to handle numerical constraint in bdds. This field is not set at init time anymore, but in formula_to_bdd. Add <>, <, and <= to the type of formula. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.23 Version-Log: Make the examples of Yvan work. Fix a bunch of bugs alonf the way... Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.21 Version-Log: Change the comments layout so that ocamldoc is able to process them nicely. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.17 Version-Log: Handle pre in formula and expressions. Also add (in green) the environment local vars in the sim2chro output. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.13 Version-Log: Now lurette can hanble multiple environements that can either be run as a product or in parallel. Project-Description: Lurette
-