lurette.prj 11 KB
Newer Older
1
2
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
3
(Project-Description "Lurette")
4
5
6
(Project-Version lurette 0 122)
(Parent-Version lurette 0 121)
(Version-Log " 
7

8
9
10
11
When delayed constraints are remaining at bdd leaves, we were
printing a message saying that one shoud use a polyhedron solver
based instead.  Now, I really call such a polyhedron solver in order
to solve those constraints.
12

13
14
This means that I use to different solvers to handle interval and
polyhedron of dimension > 1. 
15

16
17
18
19
20
21
22
It also means that the satisfiability of constraints over polyhedra
is only checked at bdd leaves, which, in some circumstances, migth be
inefficient. The point is that, if we chose to check the formula
satisfiability during the bdd traversal, we take the risk that a very
polyhedron is created whereas it was not necessary (because of
forthcoming equalities). And creating polyhedron with big (>15) 
dimension simply runs forever, which is really bad.
23

24
nb : drawing in poyhedron not yet plugged.
25

26
27
28
29
30
31
32
33
34
35
source/polyhedron.ml: 
source/polyhedron.mli: (new files)
    misc functions over polyhedra. The rational for creating that file
    is that rnumsolver is already much too big (and should be splitted 
    some more btw).


source/solver.ml:
   One of the main change is that now, draw_in_bdd returns 2 stores.
   One is Range based, the other one is polyhedron-based.
36

37
38
39
40
41
source/rnumsolver.mli:
source/rnumsolver.ml:
   Add the function switch_to_polyhedron_representation which
   handle delayed constraint if necessary. It is meant to be called
   at bdd leaves.
42

43
44
45
46
47
48
49
50
51
52
53
54
55
source/solver.ml:
source/rnumsolver.ml:
   Also do not use split_store anymore but add_constraint. This allows
   a much more elegant and efficient implementation of draw_in_bdd and
   draw_in_bdd_eq (Now the store is buid when and only when a new branch
   should be tried because of backtracking). It is also more efficient.

source/constraint.mli
source/constraint.ml
source/ne.mli
source/ne.ml
   Implement get_vars that retreive the variables occuring in a contraint
   or an expression.
56
57
58
")
(New-Version-Log ""
)
59
(Checkin-Time "Mon, 17 Feb 2003 14:50:50 +0100")
60
61
62
63
64
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
(Files

65
66
67

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

68

69
70
;; Sources files for luc_exe
  (source/luc_exe.mli (lurette/b/31_ima_exe.ml 1.2 644))
71
  (source/luc_exe.ml (lurette/b/32_ima_exe.ml 1.24 644))
72

73
  (source/command_line_luc_exe.ml (lurette/b/33_command_li 1.9 644))
74
  (source/command_line_luc_exe.mli (lurette/b/34_command_li 1.6 644))
75
76

;; Sources files for lurette only
77
  (source/lurette.mli (lurette/11_lurette.ml 1.12 644))
78
  (source/lurette.ml (lurette/12_lurette.ml 1.61 644))
79

80
81
  (source/command_line.ml (lurette/b/20_command_li 1.10 644))
  (source/command_line.mli (lurette/b/21_command_li 1.9 644))
82

83
;; Sources files common to lurette and luc_exe
84
85
  (source/graph.mli (lurette/13_graph.mli 1.10 644))
  (source/graph.ml (lurette/14_graph.ml 1.8 644))
86

87
  (source/env.mli (lurette/15_env.mli 1.17 644))
88
  (source/env.ml (lurette/16_env.ml 1.29 644))
89

90
  (source/util.ml (lurette/35_util.ml 1.37 444))
91

92
  (source/solver.mli (lurette/38_solver.mli 1.13 644))
93
  (source/solver.ml (lurette/39_solver.ml 1.40 644))
94

95
96
  (source/polyhedron.ml (lurette/d/25_polyhedron 1.1 644))
  (source/polyhedron.mli (lurette/d/26_polyhedron 1.1 644))
97

98
99
100
101
102
  (source/rnumsolver.mli (lurette/b/26_rnumsolver 1.12 644))
  (source/rnumsolver.ml (lurette/b/27_rnumsolver 1.19 644))

  (source/pnumsolver.ml (lurette/d/23_pnumsolver 1.2 644))
  (source/pnumsolver.mli (lurette/d/24_pnumsolver 1.2 644))
103

104
  (source/parse_env.mli (lurette/40_parse_env. 1.11 644))
105
  (source/parse_env.ml (lurette/41_parse_env. 1.35 644))
106

107
  (source/show_env.mli (lurette/42_show_env.m 1.8 644))
108
  (source/show_env.ml (lurette/43_show_env.m 1.16 644))
109

110
  (source/formula.mli (lurette/44_formula.ml 1.19 644))
111
  (source/formula.ml (lurette/45_formula.ml 1.24 644))
112

113
  (source/print.mli (lurette/46_print.mli 1.12 644))
114
  (source/print.ml (lurette/47_print.ml 1.21 644))
115

116
117
  (source/eval.mli (lurette/48_eval.mli 1.10 644))
  (source/eval.ml (lurette/49_eval.ml 1.13 644))
118

119
  (source/env_state.mli (lurette/50_env_state. 1.25 644))
120
  (source/env_state.ml (lurette/51_env_state. 1.35 644))
121

122
  (source/automata.mli (lurette/b/46_automata.m 1.3 644))
123
  (source/automata.ml (lurette/b/47_automata.m 1.6 644))
124

125
  (source/sim2chro.mli (lurette/b/23_sim2chro.m 1.6 644))
126
  (source/sim2chro.ml (lurette/b/24_sim2chro.m 1.14 644))
127

128
129
  (source/gne.mli (lurette/b/36_gne.mli 1.4 644))
  (source/gne.ml (lurette/b/37_gne.ml 1.4 644))
130

131
  (source/lurettetop.ml (lurette/c/1_lurettetop 1.24 644))
132
  (source/gen_stubs.ml (lurette/24_generate_l 1.41 644))
133

134
135
  (source/control.mli (lurette/c/3_control.ml 1.3 644))
  (source/control.ml (lurette/c/4_control.ml 1.4 644))
136

137
138
  (source/constraint.mli (lurette/c/18_constraint 1.5 644))
  (source/constraint.ml (lurette/c/19_constraint 1.6 644))
139

140
141
  (source/ne.ml (lurette/c/21_ne.ml 1.5 644))
  (source/ne.mli (lurette/c/22_ne.mli 1.4 644))
142

143
  (source/value.ml (lurette/c/23_value.ml 1.2 644))
144
  (source/value.mli (lurette/c/24_value.mli 1.1 644))
145

146
147
  (source/prevar.ml (lurette/d/18_prevar.ml 1.1 644))
  (source/prevar.mli (lurette/d/19_prevar.mli 1.1 644))
148
149
150
151

  (source/parse_poc.ml (lurette/d/15_parse_poc. 1.1 644))
  (source/gen_fake_lutin.ml (lurette/d/16_gen_fake_l 1.1 644))

152
; little script that sets env vars and starts the lurette build
153
  (make_lurette (lurette/27_make_luret 1.17 755))
154
155

;; Make files
156
  (configure.in (lurette/d/11_configure. 1.1 644))
157
  (Makefile.common.in (lurette/d/12_Makefile.c 1.2 644))
158
  (OcamlMakefile (lurette/17_OcamlMakef 1.46 644))
159
  (Makefile.lurette (lurette/b/38_Makefile.l 1.16 644))
160
  (user-rules (lurette/c/14_myrules 1.23 644))
161
  (user-rules.skel (lurette/c/25_user-rules 1.2 644))
162
  (Makefile (lurette/d/13_Makefile 1.1 644))
163

164
  (source/Makefile.lurettetop (lurette/d/14_Makefile.l 1.2 644))
165
  (source/Makefile.gen_fake_lutin (lurette/d/17_Makefile.g 1.1 644))
166
  (source/Makefile.show_luc (lurette/b/40_Makefile.s 1.8 644))
167
  (source/Makefile.lucky (lurette/b/41_Makefile.i 1.12 644))
168
  (source/Makefile.gen_stubs (lurette/b/42_Makefile.g 1.5 644))
169
  (source/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.12 644))
170
  (source/Makefile (lurette/c/20_Makefile 1.10 644))
171
172
173
174

;; Documentation
  (doc/Interface_draft (lurette/19_Interface_ 1.1 644))
  (doc/archi.fig (lurette/20_archi.fig 1.1 644))
175
176
  (doc/synthese (lurette/b/2_synthese 1.1 644))
  (doc/automata_format (lurette/b/3_automata_f 1.1 644))
177
178
  (doc/ocamldoc.sty (lurette/b/12_ocamldoc.s 1.1 644))
  (doc/ocamldoc.hva (lurette/b/13_ocamldoc.h 1.1 644))
179
180

;; Misc
181
  (README (lurette/10_README 1.5 644))  
182
  (ID_EN_VRAC (lurette/0_ID_EN_VRAC 1.1 644))
183
184
  (lurette.dep.dot (lurette/b/4_lurette.de 1.2 644))
  (lurette.depfull.dot (lurette/b/5_lurette.de 1.2 644))
185
  (TAGS (lurette/21_TAGS 1.6 644))
186

187
188
189
190
  (test/time-ossau.exp (lurette/b/48_time.exp 1.27 644))
  (test/time-ossau.res (lurette/b/49_time.res 1.30 644))
  (test/time-ecrins.res (lurette/d/20_time-ecrin 1.4 644))
  (test/time-ecrins.exp (lurette/d/21_time-ecrin 1.4 644))
191

192
;; Various files used for testing purposes
193
194
195
196
197
  (test/usager.luc (lurette/b/14_usager.env 1.9 644))
  (test/tram.luc (lurette/b/15_tram.env 1.8 644))
  (test/porte.luc (lurette/b/16_porte.env 1.8 644))
  (test/passerelle.luc (lurette/b/17_passerelle 1.8 644))
  (test/temp_int.luc (lurette/b/50_temp_int.e 1.3 644))
198
  (test/temp_float.luc (lurette/b/51_temp_float 1.4 644))
199

200
201
  (test/ControleurPorte.h (lurette/b/18_Controleur 1.1 644))
  (test/ControleurPorte.c (lurette/b/19_Controleur 1.1 644))
202
  (test/ControleurPorte.lus (lurette/c/17_Controleur 1.1 644))
203

204
205
206
  (test/vrai_tram.lus (lurette/b/6_vrai_tram. 1.2 644))
  (test/vrai_tram.h (lurette/b/7_vrai_tram. 1.3 644))
  (test/vrai_tram.c (lurette/b/8_vrai_tram. 1.3 644))
207
  (test/tram_simple.h (lurette/b/25_tram_simpl 1.1 644))
208

209
210
211
  (test/heater_int.rif.exp (lurette/b/28_heater_int 1.10 644))
  (test/ControleurPorte.rif.exp (lurette/b/29_Controleur 1.11 644))
  (test/heater_float.rif.exp (lurette/b/30_heater_flo 1.11 644))
212
  (test/heater_int.lus (lurette/b/43_heater_int 1.1 644))
213
  (test/heater_float.lus (lurette/b/44_heater_flo 1.2 644))
214
  (test/test_gen_stubs.h (lurette/b/45_test_gen_s 1.1 644))
215

216
  (test/giro/allocator.lus (lurette/c/5_allocator. 1.1 644))
217
  (test/giro/giro.luc (lurette/c/6_giro.ima 1.4 644))
218
219
220
221
222
  (test/giro/onlyroll.lus (lurette/c/7_onlyroll.l 1.1 644))

  (demo/chaudiere/chaudiere_oracle.lus (lurette/c/8_chaudiere_ 1.1 644))
  (demo/chaudiere/chaudiere_ctrl.lus (lurette/c/9_chaudiere_ 1.1 644))
  (demo/chaudiere/buggy_chaudiere_ctrl.lus (lurette/c/10_buggy_chau 1.1 644))
223
  (demo/chaudiere/chaudiere.luc (lurette/c/11_chaudiere. 1.5 644))
224

225
  (test/Makefile (lurette/c/0_Makefile 1.8 644))
226
227

;; xlurette
228
  (ihm/xlurette/xlurette_glade_main.ml (lurette/c/12_xlurette_g 1.15 644))
229
230
  (ihm/xlurette/xlurette.glade (lurette/c/13_xlurette.g 1.9 644))
  (ihm/xlurette/xlurette_glade_interface.ml (lurette/c/15_xlurette_g 1.8 644))
231
  (ihm/xlurette/makefile (lurette/c/16_makefile 1.7 644))
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276


;; cudaux 
  (cuddaux/cuddauxTDGenCof.c (lurette/c/26_cuddauxTDG 1.1 644))
  (cuddaux/cuddauxMisc.c (lurette/c/27_cuddauxMis 1.1 644))
  (cuddaux/cuddauxInt.h (lurette/c/28_cuddauxInt 1.1 644))
  (cuddaux/cuddauxGenCof.c (lurette/c/29_cuddauxGen 1.1 644))
  (cuddaux/cuddauxCompose.c (lurette/c/30_cuddauxCom 1.1 644))
  (cuddaux/cuddauxBridge.c (lurette/c/31_cuddauxBri 1.1 644))
  (cuddaux/cuddauxAddIte.c (lurette/c/32_cuddauxAdd 1.1 644))
  (cuddaux/cuddaux.h (lurette/c/33_cuddaux.h 1.1 644))
  (cuddaux/README (lurette/c/34_README 1.1 644))
  (cuddaux/Makefile (lurette/c/35_Makefile 1.1 644))
  (cuddaux/Changes (lurette/c/36_Changes 1.1 644))


;; mlcuddidl
  (mlcuddidl/session.ml (lurette/c/37_session.ml 1.1 644))
  (mlcuddidl/sedscript (lurette/c/38_sedscript 1.1 644))
  (mlcuddidl/rdd_caml.c (lurette/c/39_rdd_caml.c 1.1 640))
  (mlcuddidl/rdd.mli (lurette/c/40_rdd.mli 1.1 640))
  (mlcuddidl/rdd.ml (lurette/c/41_rdd.ml 1.1 640))
  (mlcuddidl/rdd.idl (lurette/c/42_rdd.idl 1.1 644))
  (mlcuddidl/mtbdd.mli (lurette/c/43_mtbdd.mli 1.1 644))
  (mlcuddidl/mtbdd.ml (lurette/c/44_mtbdd.ml 1.1 644))
  (mlcuddidl/manager_caml.c (lurette/c/45_manager_ca 1.1 640))
  (mlcuddidl/manager.mli (lurette/c/46_manager.ml 1.1 640))
  (mlcuddidl/manager.ml (lurette/c/47_manager.ml 1.1 640))
  (mlcuddidl/manager.idl (lurette/c/48_manager.id 1.1 644))
  (mlcuddidl/macros.m4 (lurette/c/49_macros.m4 1.1 644))
  (mlcuddidl/idd_caml.c (lurette/c/50_idd_caml.c 1.1 640))
  (mlcuddidl/idd.mli (lurette/c/51_idd.mli 1.1 640))
  (mlcuddidl/idd.ml (lurette/d/0_idd.ml 1.1 640))
  (mlcuddidl/idd.idl (lurette/d/1_idd.idl 1.1 644))
  (mlcuddidl/cudd_caml.h (lurette/d/2_cudd_caml. 1.1 644))
  (mlcuddidl/cudd_caml.c (lurette/d/3_cudd_caml. 1.1 644))
  (mlcuddidl/bdd_caml.c (lurette/d/4_bdd_caml.c 1.1 640))
  (mlcuddidl/bdd.mli (lurette/d/5_bdd.mli 1.1 640))
  (mlcuddidl/bdd.ml (lurette/d/6_bdd.ml 1.1 640))
  (mlcuddidl/bdd.idl (lurette/d/7_bdd.idl 1.1 644))
  (mlcuddidl/README (lurette/d/8_README 1.1 644))
  (mlcuddidl/Makefile (lurette/d/9_Makefile 1.1 644))
  (mlcuddidl/Changes (lurette/d/10_Changes 1.1 644))


277
  (TODO (lurette/d/22_TODO 1.3 644))
278

279
280
281
)
(Merge-Parents)
(New-Merge-Parents)