- 17 Mar, 2010 40 commits
-
-
Erwan Jahier authored
Parent-Version: 0.113 Version-Log: source/parse_env.ml: When floats output vars are not constraint, use [-10^11, 10^11] as default domain. The rational for this change is that sim2chro does not seem to be able to print bigger floats (probably because it does not understand the 123e+234 notation. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.112 Version-Log: source/show_luc.ml: source/lurette.ml: source/parse_env.ml: Enhance error msgs during the .luc parsing. Add the line number. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.111 Version-Log: source/parse_poc.ml: (new file) source/gen_stubs.ml: put everything that is related to poc parsing into parse_poc.ml. source/gen_fake_lutin.ml: (new file) source/parse_poc.ml: (new file) source/Makefile.gen_fake_lutin: (new file) When no .lut is provided, we generate a fake one. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.110 Version-Log: source/util.ml: source/formula.ml: source/lurette.ml: Only print one counter example if the test failed. source/lurettetop.ml: source/gen_stubs.ml: try to guess the node name in lurettetop rather than in gen_stubs if not given. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.109 Version-Log: source/util.ml: source/lurettetop.ml: source/gen_stubs.ml: ihm/xlurette/xlurette_glade_main.ml: ihm/xlurette/xlurette.glade: Add the possibility to specify te sut and the oracle main node (to feed the lustre compiler). Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.108 Version-Log: ihm/xlurette/xlurette_glade_main.ml: source/lurettetop.ml: Retreive and print the pid of lurette to be able in xlurette to kill the current run. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.107 Version-Log: source/lurette.ml: source/command_line.ml source/command_line.mli source/util.ml: source/lurettetop.ml: use crete_process instead un sys.command to call lurette from lurettetop ihm/xlurette/xlurette_glade_main.ml: Put the newly generated random seed into the manual text box. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.106 Version-Log: source/lurettetop.ml: ihm/xlurette/.ml: fix a bug when reading the .lurette_rc where the the env were added instead of beinf overrided when they were both specified in the rc file and as a comd line option. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.105 Version-Log: source/lurettetop.ml: Add a --prefix <string> option that is added before the call to lurette (usefull, eg, for timing purpuses). source/lurettetop.ml: source/lurette.ml: source/command_line.ml: ihm/xlurette/* Add a ---show-step options that let one control whether or not the step number is printed. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.104 Version-Log: ihm/xlurette/*: Look up the pipe every 1/10 sec. instead of reading it after each command until a certain string is encoutered. It make the code more robust (no protocol), it avoid that xlurette is blocked during the process. Moreover, it let the progress bar works gently. Add a stop button that sends a sigint to lurettetop that ougth to stop the current execution (does not work, why?). Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.103 Version-Log: source/lurettetop.ml: source/util.ml: use explicit file name so that, e.g., show_luc, is always able to find the file it is supposed to show. Allow users to put extension or not for the sut or oracle files, being at the prompt or at the invocation. cp lurette.ml and lurette.mli in the temp dir and compile it there to avoid that everyone is writing on the source dir which prevent the next user to use lurette... Makefile.common.in: INCDIRS Ocamlmakeke file var is not supposed to contains path to .h C files to include but .mli ocml ones !!! Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.102 Version-Log: Add autoconf aupport. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.101 Version-Log: Add cuddaux and mlcuddidl to the project. Also clean-up Makefiles etc in order to make the installation process as automatic as possible. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.100 Version-Log: Rename any occurence of ima by luc or lucky. Project-Description: Lurette
-
Erwan Jahier authored
Parent-Version: 0.99 Version-Log: source/gen_stubs: Make sure we are in the rigth directory we calling lus2ec and ec2c. Project-Description: Lurette
-
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
-