- 17 Mar, 2010 40 commits
-
-
Erwan Jahier authored
Parent-Version: 0.98 Version-Log: source/solver.ml: source/rnumsolver.mli,.ml: source/constraint.ml,.mli: Split the Constraint.t type into t and ineq where inequalities are in ineq. The rational is that most operations on constaint.t are actually done on ineq. This change therefore avoid pattern like <<_ -> assert false>> and let the type checher check that sort of things. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.97 Version-Log: source/rnumsolver.ml: Remove valI and ValF from the range type as now, when a var is bound, it is put into store.substl. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.96 Version-Log: Handling equalities smartlier. . Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.95 Version-Log: source/ne.ml,mli: source/value.ml,mli: (new files) put everything that is related to normal expressions and values in thoses 2 new modules. source/ne.ml,mli: source/gne.ml,mli: Make the normal expressions and the guarded normal expression abstract. source/solver.ml: also fix a bug in the previous change (forgot to try make test ...) Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.94 Version-Log: Continue to prepare things for the next change (which will try to handle equalities smartly). test/test*.res: fix the expected results as this change adds a random toss that disturbs the random values. source/solver.ml: source/rnumsolver.ml: Add code to handle the fact that the negation of a equality is the disjunction of two inegalities, which can not be added to store as it is. So we first try with >, and if it fails, we try with < (or the other way aroung, depending on a fair toss). Also split up the code in Solver.draw_in_bdd depending on the fact that the current constraint is a boolean, an eq, or an ineg. source/solver.ml: split toss_up_one_var into toss_up_one_var and toss_up_one_var_index, one performing the the toss from a var, the other one from a var index. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.93 Version-Log: Prepare things for the next change (which will try to handle equalities smartly). source/solver.ml: source/rnumsolver.ml: atomic_formula do not need both < and > (ditto for <= and >=). Indeed, I just need to take the opposite, and everything is fine. One advantage is that there are less cases to handle. But the key advantage is that it make the representation of constraint normal, which is important at least when I will try to detect equalities. Also add a subst list and constraint list fields to the store that will ebe used in the forthcoming change. They will resp. be used for removeing a dimension when an equality is encountered and to delay constraint with more than one variable. source/constraint.ml,mli: (new files) Move there from formula.ml everything that is related to the internal representation of constraints. Also change the name of atomic_formula to linear_constraint, which is more informative. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.92 Version-Log: source/formula.ml: source/solver.ml: source/parse_env.ml: Handle boolean equalities with Bdd.eq instead of manually converting it with <<and>>, <<not>> and <<or>>. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.91 Version-Log: source/parse_env.ml: Allow expr a the lhs of comparison operators. Make comparison operators prefix instead on infix as it considerably simplifies the parsing. Also introduce a == keyword that operates over bool to disambiguate things (= is the equality for nums, and == the one for bool. Now the lucky grammar is truely LL(1), which is nice. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.90 Version-Log: source/parse_env.ml: Allow a space between a '-' and a numeric value. Project-Description: Lurette
-
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.88 Version-Log: Chech that automata run concurenty do not share any variables. 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.86 Version-Log: Save and restore sessions without messing up directory names (namely, avoid name clashes in the /tmp dir). Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.85 Version-Log: Finish to implement xlurette. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.84 Version-Log: source/gen_stubs.ml: Add a lurette_stub__ prefix to most function names to make sure that there is no name clashes. In particular, oracle can now be called oracle.lus ... (but not lurette_stub__oracle.lus, which is not so bad...). Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.83 Version-Log: empty Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.82 Version-Log: source/lurette.ml: source/lurettetop.ml: source/command_line.ml, .mli: source/solver.ml: source/env_state.ml: source/rnumsolver.ml: Add 2 news options, --draw-edges ans --draw-verteces that makes lurette draw among the verteces or on the edges of the convex hull of solutons. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.81 Version-Log: source/lurette.ml: source/ima_exe.ml: Check that nodes did not changed before redrawing anything also add a <<q>> command to exit from ima_exe more gently. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.80 Version-Log: source/control.ml: Give a proper error message when one uses a ctrl expr that is not defined. 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.78 Version-Log: source/lurettetop.ml: Add a pack command and a --restore option to lurettetop that respectively save temporarily created files during a session and restore them later on. Also clean-up temporarily created files when lurettetop resumes. 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.76 Version-Log: source/lurettetop.ml: Building every temporary files in /tmp/lurette2313/. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.75 Version-Log: *.ml: Avoid using Sys.command when possible. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.74 Version-Log: makefile.lurette: bin/makefile.lurette_lib: put all files that do not depend on lurette_stubs into a lib. source/lurettetop.ml: Add a few new options (show, step, ...) Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.73 Version-Log: source/lurettetop.ml: [new file] A top level loop for using lurette. also remame all .env files using .ima instead of .env as extension. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.72 Version-Log: gen_stubs.ml: sim2chro.ml: Do not sort varialble lexicographically but according to sut order. gen_stubs.ml: When converting subst list to tuple, do not put fake values if the list is empty, but raise a failure (assert false). Do not parse idl output to guess the conversion between ml and C type but hard code it instead. The rational is that I was manually calling camlidl here which was confusing make sometimes. make_lurette: exit properly before running lurette whenever something bad happen during the make. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.71 Version-Log: sim2cro.ml: switch inputs and output in the sim2chro display. The rational is that local vars, are closer from ima outputs than sut ones. and should then be displayed close to them. gen_stubs.ml: indent generated code better. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.70 Version-Log: automata.ml,mli: env.ml,mli: ima_exe.ml,mli: lurette.ml,mli: Fix a bug where the control expr were evaluated twice, which migth produce strange behavior whenever a CS var was drawn to 0 in the place, and a value different from 0 in the second place. The fix consist in attaching the control.state at automata.t leaves, instead of the control expr labels (which was a bit silly BTW). show_env.ml: Fix a small bug in the dot output. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.69 Version-Log: ima_exe.ml: lurette.ml: env_state.ml: Factoring out code into two new functions, clear_step and clear_all. env_state.ml: Do not use to 2 ranges of indexes (one for atomic formula that depends on pre, one if it is not) but maintain a list a unused indexes instead. 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.67 Version-Log: Add a verbose option in ima_exe. Fix a bug in show_env.ml introduced in the previuos pci. Add support to dynamically load another ima from ima_exe (will usefull for Ludic). Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.66 Version-Log: Draw loop nodes as circles and other nodes as boxes in the dot output of the ima files. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.65 Version-Log: solver.ml: Fix a bug is draw_in_bdd where it was unable to draw in a true formula when it was a top level one. The reason was that the tossing of remaining vars was not done at draw_in_bdd top level, which is wrong since true can appear on ima transitions. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.64 Version-Log: Outputs error message on stderr rather than on stdout. 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.62 Version-Log: Reimplement the rif parsing in ima_exe.ml so that it is correct wrt the BLA-RIF doc. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.61 Version-Log: Reorganise things a little bit so that show_ima does not depend on cudd, etc. 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
-