Commit 8e21b389 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.20 Thu, 06 Dec 2001 16:10:48 +0100 by jahier

Parent-Version:      0.19
Version-Log:

Just a couple of cosmetic changes.

Project-Description: Lurette
parent 70df449f
......@@ -2,30 +2,30 @@
;; REALLY bad things.
(Created-By-Prcs-Version 1 3 3)
(test/vrai.h 1120 1006183551 31_vrai.h 1.1)
(source/env_state.ml 1514 1007638809 51_env_state. 1.2)
(source/env_state.ml 1468 1007648245 51_env_state. 1.3)
(source/graph.ml 2397 1003932490 14_graph.ml 1.2)
(test/tram_env_porte.env 882 1007638809 b/11_tram_env_p 1.2)
(source/util.ml 3166 1007638809 35_util.ml 1.3)
(source/util.ml 3552 1007648245 35_util.ml 1.4)
(source/wtree.ml 9181 1007379917 b/1_wtree.ml 1.1)
(source/solver.ml 1834 1007638809 39_solver.ml 1.2)
(source/lurette.ml 9612 1007638809 12_lurette.ml 1.11)
(source/solver.mli 617 1007379917 38_solver.mli 1.1)
(source/solver.ml 2091 1007651448 39_solver.ml 1.3)
(source/lurette.ml 8309 1007648245 12_lurette.ml 1.12)
(source/solver.mli 707 1007651448 38_solver.mli 1.2)
(source/env.mli 2838 1007379917 15_env.mli 1.5)
(test/vrai.lus 65 1006182545 28_vrai.lus 1.1)
(lurette.depfull.dot 1146 1007379917 b/5_lurette.de 1.1)
(lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
(test/tram_env_tramway.env 1228 1007638809 b/10_tram_env_t 1.2)
(source/env.ml 8243 1007638809 16_env.ml 1.9)
(make_lurette 1027 1007398490 27_make_luret 1.5)
(test/vrai_tram.lus 453 1007379917 b/6_vrai_tram. 1.1)
(test/edge.c 1693 1006263320 32_edge.c 1.1)
(lurette.dep.dot 485 1007379917 b/4_lurette.de 1.1)
(lurette.dep.dot 49 1007651448 b/4_lurette.de 1.2)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(source/parse_env.mli 865 1007638809 40_parse_env. 1.2)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(test/edge.h 1052 1006263320 33_edge.h 1.1)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/eval.ml 7923 1007638809 49_eval.ml 1.2)
(source/gen_stubs.ml 32046 1007638809 24_generate_l 1.11)
(source/gen_stubs.ml 32119 1007648245 24_generate_l 1.12)
(source/parse_env.ml 6609 1007638809 41_parse_env. 1.2)
(interface/TAGS 1956 1007380262 26_TAGS 1.3)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
......@@ -37,19 +37,19 @@
(interface/sut_idl_stub.ml 338 1006263457 34_sut_idl_st 1.1)
(source/eval.mli 859 1007638809 48_eval.mli 1.2)
(README 0 1002791390 10_README 1.1)
(OcamlMakefile 15997 1007638809 17_OcamlMakef 1.5)
(OcamlMakefile 16039 1007651448 17_OcamlMakef 1.7)
(source/show_env.ml 3303 1007379917 43_show_env.m 1.1)
(test/tram_simple.c 5627 1006433610 37_tram_simpl 1.1)
(doc/synthese 2556 1007379917 b/2_synthese 1.1)
(interface/Makefile 215 1007380262 25_Makefile 1.5)
(source/show_env.mli 848 1007379917 42_show_env.m 1.1)
(test/tram_simple.h 1746 1006433610 36_tram_simpl 1.1)
(Makefile 1269 1007638809 18_Makefile 1.10)
(Makefile 1350 1007648245 18_Makefile 1.11)
(test/vrai_tram.c 2855 1007379917 b/8_vrai_tram. 1.1)
(source/print.mli 108 1007379917 46_print.mli 1.1)
(source/graph.mli 1305 1003932490 13_graph.mli 1.2)
(source/formula.ml 3115 1007638809 45_formula.ml 1.2)
(test/vrai.c 1405 1006183551 30_vrai.c 1.1)
(source/lurette.mli 371 1007398490 11_lurette.ml 1.7)
(source/lurette.mli 370 1007648245 11_lurette.ml 1.8)
(source/print.ml 1098 1007379917 47_print.ml 1.1)
(test/vrai_tram.h 2293 1007379917 b/7_vrai_tram. 1.1)
......@@ -5,7 +5,7 @@
# For updates see:
# http://miss.wu-wien.ac.at/~mottl/ocaml_sources
#
# $Id: OcamlMakefile 1.6 Thu, 06 Dec 2001 15:17:25 +0100 jahier $
# $Id: OcamlMakefile 1.7 Thu, 06 Dec 2001 16:10:48 +0100 jahier $
#
###########################################################################
......@@ -475,21 +475,23 @@ pncl: profiling-native-code-library
###########################################################################
# R1
# Generates emacs tags (R1)
tags:
$(OTAGS) -v $(SOURCES)
# Generates the modules dependency graph using ocamldot
# (results in lurette.dep.ps and lurette.depfull.ps)
# (results in lurette.dep.ps and lurette.depfull.ps). (R1)
dot:
touch $(RESULT).dep.dot ; touch $(RESULT).dep.ps ; \rm $(RESULT).dep.ps $(RESULT).dep.dot ; \
touch $(RESULT).depfull.dot ; touch $(RESULT).depfull.ps ; \rm $(RESULT).depfull.ps $(RESULT).depfull.dot ; \
touch $(RESULT).dep.dot ; touch $(RESULT).dep.ps ; \
\rm $(RESULT).dep.ps $(RESULT).dep.dot ; \
touch $(RESULT).depfull.dot ; touch $(RESULT).depfull.ps ; \
\rm $(RESULT).depfull.ps $(RESULT).depfull.dot ; \
ocamldep $(SOURCES) | $(OCAMLDOT) -fullgraph -lr > $(RESULT).depfull.dot ; \
ocamldep $(SOURCES) | $(OCAMLDOT) > $(RESULT).dep.dot ; \
dot -Tps $(RESULT).depfull.dot > $(RESULT).depfull.ps ; \
dot -Tps $(RESULT).dep.dot > $(RESULT).dep.ps
dot -Tps $(RESULT).dep.dot > $(RESULT).dep.ps
#
# (R1)
try:
$(LURETTE_DIR)/make_lurette tram_simple tram_oracle; \
./lurette 50 10 10 tram_env_porte.env x tram_env_usager.env tram_env_tramway.env
......
digraph G {
size="7.5,10" ;
rankdir = TB ;
"Lurette" -> "Env" ;
"Lurette" -> "Show_env" ;
"Show_env" -> "Env_state" ;
"Env" -> "Eval" ;
"Env" -> "Parse_env" ;
"Parse_env" -> "Formula" ;
"Wtree" -> "Graph" ;
"Wtree" -> "Solver" ;
"Solver" -> "Formula" ;
"Solver" -> "Util" ;
"Eval" -> "Env_state" ;
"Env_state" -> "Wtree" ;
"Print" -> "Wtree" ;
"Formula" -> "Lurette_stub" ;
"Lurette_stub" -> "Oracle_idl_stub" ;
"Lurette_stub" -> "Sut_idl_stub" ;
}
digraph G {
size="7.5,10" ;
rankdir = LR ;
"Lurette_stub" -> "Oracle_idl_stub" ;
"Lurette_stub" -> "Sut_idl_stub" ;
"Formula" -> "Lurette_stub" ;
"Print" -> "Formula" ;
"Print" -> "Wtree" ;
"Env_state" -> "Formula" ;
"Env_state" -> "Graph" ;
"Env_state" -> "Lurette_stub" ;
"Env_state" -> "Wtree" ;
"Eval" -> "Env_state" ;
"Eval" -> "Formula" ;
"Eval" -> "Lurette_stub" ;
"Eval" -> "Wtree" ;
"Solver" -> "Formula" ;
"Solver" -> "Lurette_stub" ;
"Solver" -> "Util" ;
"Wtree" -> "Formula" ;
"Wtree" -> "Graph" ;
"Wtree" -> "Solver" ;
"Wtree" -> "Util" ;
"Parse_env" -> "Formula" ;
"Env" -> "Env_state" ;
"Env" -> "Eval" ;
"Env" -> "Formula" ;
"Env" -> "Graph" ;
"Env" -> "Lurette_stub" ;
"Env" -> "Parse_env" ;
"Env" -> "Solver" ;
"Env" -> "Util" ;
"Env" -> "Wtree" ;
"Show_env" -> "Env_state" ;
"Show_env" -> "Formula" ;
"Show_env" -> "Graph" ;
"Lurette" -> "Env" ;
"Lurette" -> "Env_state" ;
"Lurette" -> "Formula" ;
"Lurette" -> "Lurette_stub" ;
"Lurette" -> "Oracle_idl_stub" ;
"Lurette" -> "Show_env" ;
"Lurette" -> "Sut_idl_stub" ;
"Lurette" -> "Util" ;
}
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 19)
(Parent-Version lurette 0 18)
(Project-Version lurette 0 20)
(Parent-Version lurette 0 19)
(Version-Log "
Fix a bug where the variables were not given in the good order to
the oracle.
Give a diagnostic when the oracle is broken.
Put everything related to sim2chro in tis own module.
Just a couple of cosmetic changes.
")
(New-Version-Log "")
(Checkin-Time "Thu, 06 Dec 2001 15:17:25 +0100")
(Checkin-Time "Thu, 06 Dec 2001 16:10:48 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -34,8 +29,8 @@ Put everything related to sim2chro in tis own module.
(source/util.ml (lurette/35_util.ml 1.4 644))
(source/solver.mli (lurette/38_solver.mli 1.1 644))
(source/solver.ml (lurette/39_solver.ml 1.2 644))
(source/solver.mli (lurette/38_solver.mli 1.2 644))
(source/solver.ml (lurette/39_solver.ml 1.3 644))
(source/parse_env.mli (lurette/40_parse_env. 1.2 644))
(source/parse_env.ml (lurette/41_parse_env. 1.2 644))
......@@ -61,7 +56,7 @@ Put everything related to sim2chro in tis own module.
(source/gen_stubs.ml (lurette/24_generate_l 1.12 644))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.6 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.7 644))
(Makefile (lurette/18_Makefile 1.11 644))
(test/Makefile (../Makefile) :symlink)
(interface/Makefile (lurette/25_Makefile 1.5 644))
......@@ -77,8 +72,8 @@ Put everything related to sim2chro in tis own module.
;; Misc
(README (lurette/10_README 1.1 644))
(ID_EN_VRAC (lurette/0_ID_EN_VRAC 1.1 644))
(lurette.dep.dot (lurette/b/4_lurette.de 1.1 644))
(lurette.depfull.dot (lurette/b/5_lurette.de 1.1 644))
(lurette.dep.dot (lurette/b/4_lurette.de 1.2 644))
(lurette.depfull.dot (lurette/b/5_lurette.de 1.2 644))
(TAGS (lurette/21_TAGS 1.6 644))
(interface/TAGS (lurette/26_TAGS 1.3 644))
......
......@@ -10,9 +10,9 @@
*)
open Formula
open Lurette_stub
exception False_formula
(****************************************************************************)
(****************************************************************************)
let formula_list_to_conj fl =
match fl with
......@@ -25,21 +25,28 @@ let formula_list_to_conj fl =
let rec (solve_formula_one: formula -> subst list * env_loc) =
(*
** [solve_formula f] randomly assigns values to free variables occuring
** in the formula `f'.
** in `f'.
*)
fun f ->
match f with
Bvar(var_name) -> ([(var_name, Bool(true))], [])
| Not(Bvar(var_name)) -> ([(var_name, Bool(false))], [])
| And(f1, f2) ->
let (out1, loc1) = solve_formula_one f1 in
let (out2, loc2) = solve_formula_one f2 in
((List.append out1 out2), (List.append loc1 loc2))
| False -> assert false
| _ -> assert false
( match f with
Bvar(var_name) -> ([(var_name, Lurette_stub.Bool(true))], [])
| Not(Bvar(var_name)) -> ([(var_name, Lurette_stub.Bool(false))], [])
| And(f1, f2) ->
let (out1, loc1) = solve_formula_one f1 in
let (out2, loc2) = solve_formula_one f2 in
((List.append out1 out2), (List.append loc1 loc2))
| True -> ([], [])
| False -> ([], [])
| Or(f1, f2) -> assert false
| Eq(e1, e2) -> assert false
| Ge(e1, e2) -> assert false
| G(e1, e2) -> assert false
)
(*
** XXX
** XXX FIXME !!!
** XXX FIX US !!!
** XXX
*)
......@@ -52,7 +59,6 @@ let (solve_formula: int -> formula list -> (subst list * subst list) list) =
let f = formula_list_to_conj fl in
Util.unfold (solve_formula_one) f p
(****************************************************************************)
(****************************************************************************)
......@@ -62,4 +68,6 @@ let rec (is_satisfiable : formula list -> bool) =
** returns true if the formula is satisfiable
*)
not (List.mem False fl)
(* XXX *)
(* XXX FIX ME !!! *)
......@@ -7,16 +7,21 @@
** File: solver.mli
** Main author: jahier@imag.fr
**
** Formula solver.
*)
open Formula
val is_satisfiable : formula list -> bool
(*
** succeeds if the list of formula (interpreted as a conjunct) is
** satisfiable.
*)
val solve_formula: int -> formula list -> (subst list * subst list) list
(*
** [solve_formula p fl] randomly assigns p values to free variables occuring
** in the conjounction of formula appearing in `fl'.
*)
(*
** [solve_formula p fl] randomly assigns p values to free variables occuring
** in the conjunction of the formula of `fl'.
*)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment