Skip to content
Snippets Groups Projects
Commit 2f4e7e29 authored by erwan's avatar erwan
Browse files

Compute rounds in the SUT, as in sasa

parent e20c28d0
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 60 additions and 63 deletions
src/dot2lus.ml
+ 8
− 3
View file @ 2f4e7e29
......@@ -47,6 +47,7 @@ let output_prelude lustre_topology lustre_const (graph : Topology.t) =
Printf.fprintf lustre_const "const max_degree = %d;\n" dmax;
Printf.fprintf lustre_const "const min_degree = %d;\n" dmin;
Printf.fprintf lustre_const "const mean_degree = %f;\n" (Topology.get_mean_degree graph);
Printf.fprintf lustre_const "const diameter = %d;\n" (Diameter.get graph);
Printf.fprintf lustre_const "const is_directed = %b;\n" graph.directed;
Printf.fprintf lustre_const "const is_cyclic = %b;\n" (Topology.is_cyclic graph);
Printf.fprintf lustre_const "const is_connected = %b;\n" (Topology.is_connected graph);
......@@ -58,6 +59,7 @@ let output_prelude lustre_topology lustre_const (graph : Topology.t) =
| "max_degree"
| "min_degree"
| "mean_degree"
| "diameter"
| "is_directed"
| "is_cyclic"
| "is_connected"
......@@ -122,16 +124,19 @@ let output_topology lustre_topology (graph : Topology.t) name =
name action_number state_type;
Printf.fprintf lustre_topology
"returns (p_c : %s^card; Enab_p : bool^%s^card);\n"
"returns (p_c : %s^card; Enab_p : bool^%s^card; round:bool; round_nb:int);\n"
state_type action_number;
output_string lustre_topology "var\n";
output_string lustre_topology "var";
Printf.fprintf lustre_topology "\tprev_p_c : %s^card;\n\n" state_type;
graph.nodes
|> List.iteri (fun i _ -> Printf.fprintf lustre_topology "\tsel_%d : bool;\n" i);
output_string lustre_topology "let\n";
output_string lustre_topology "let
round = round<<actions_number,card>>(Enab_p, p);
round_nb = round_count(round, silent<<actions_number,card>>(Enab_p));
";
output_string lustre_topology "\tprev_p_c = initials -> pre(p_c);\n\n";
graph.nodes
......
test/Makefile.inc
+ 17
− 9
View file @ 2f4e7e29
......@@ -22,7 +22,7 @@ genclean:
rm -f *.rif *.seed
rm -f $(TOPOLOGY).lus
rm -f *_verify.lv4
rm -f *.c *.h *_const.lus *.cmt *.exec *.sh
rm -f *.c *.h *_const.lus *.cmt *.exec *.sh rdbg-session* *.log *.pdf
# generating lv6 files of out dot files
%_const.lus: %.dot
......@@ -31,6 +31,9 @@ genclean:
LIB=-package algo
OCAMLOPT=ocamlfind ocamlopt -bin-annot
LIB_LUS=$(HOME)/sasa/test/lustre/round.lus $(HOME)/sasa/salut/lib/sas.lus
# $(HOME)/sasa/test/lustre/oracle_utils.lus
##########################################################################################"
......@@ -38,14 +41,19 @@ OCAMLOPT=ocamlfind ocamlopt -bin-annot
%.simu:
make $*.dot $*_const.lus
luciole-rif lv6 $*.lus $*_const.lus -n $* -exec
luciole-rif lv6 $(LIB_LUS) $*.lus $*_const.lus -n $* -exec
%.rdbg:
make $*.dot $*_const.lus
rdbgui4sasa -sut-nd "lv6 $(LIB_LUS) $*_const.lus $*.lus -n $* -exec"
##########################################################################################"
# Use lurette to compare the lustre and the ocaml version of the algorithm
# nb : <dirname>/<dirname>_oracle.lus should be written
%.lurette:
make $*.dot $*_const.lus $*.cmxs $*_oracle.lus
lurette -sut "sasa $*.dot $(SASAFLAGS)" -oracle "lv6 $*.lus $*_oracle.lus -n oracle -2c-exec"
%.lurette: %_oracle.lus
make $*.dot $*_const.lus $*.cmxs
lurette -sut "sasa -seed 4 $*.dot $(SASAFLAGS)" -oracle "lv6 $(LIB_LUS) $*.lus $*_oracle.lus -n oracle -2c-exec"
%.cmxs: %.ml
$(OCAMLOPT) $(LIB) -shared state.ml $(shell sasa -algo $*.dot) config.ml $< -o $@
......@@ -65,7 +73,7 @@ prop = verify
endif
%.expand.kind2: %_verify.lv4
time kind2 $<
time kind2 --modular true --compositional true $<
%.kind2: %.dot
make $*_verify.noexpand.lv4
......@@ -74,13 +82,13 @@ endif
# XXX: this method of adding kind2 annotations is brittle
%_verify.lv4: %.lus %_const.lus verify.lus
lv6 $^ -n $(prop) --lustre-v4 -en -o $@
lv6 $(LIB_LUS) $*.lus $^ $*_const.lus -n $(prop) --lustre-v4 -en -o $@
sed -i -e "s/tel/--%MAIN ;\n--%PROPERTY ok;\ntel/" $@
# Do not expand nodes
%_verify.noexpand.lv4: verify.lus
make $*_const.lus
lv6 $*.lus $^ $*_const.lus -n $(prop) -rnc --lustre-v4 -o $@
lv6 $(LIB_LUS) $*.lus $^ $*_const.lus -n $(prop) -rnc --lustre-v4 -o $@
tac $@ | sed -z "s/tel/tel\n--%MAIN ;\n--%PROPERTY ok;/" | tac > $@.tmp
mv $@.tmp $@
......@@ -90,7 +98,7 @@ endif
# to use lesar, perform bit-blasting via ec2ec -usrint
%_verify.ec: %.dot verify.lus
make $*_const.lus
lv6 $*.lus $*_const.lus verify.lus -n $(prop) -ec -o $@.tmp
lv6 $(LIB_LUS) $*.lus $*_const.lus verify.lus -n $(prop) -ec -o $@.tmp
echo "include \"../../lib/bit-blast/signed_binary5.lus\"" > $@.tmp2
echo "include \"../../lib/bit-blast/binary.lus\"" >> $@.tmp2
ec2ec -usrint $@.tmp >> $@.tmp2
......
test/coloring/Makefile
+ 6
− 3
View file @ 2f4e7e29
......@@ -7,8 +7,13 @@ DECO_PATTERN="0-:p.ml"
include ../Makefile.inc
-include ../Makefile.dot
##############################################################################
# Non-regression tests
test: clique3.kind2 clique3.lesar # clique3.lurette
clean: genclean
rm -f ring*.* er*.* grid*.*
rm -f ring*.* er*.* grid*.* clique*.*
.PRECIOUS: %.lus
.PRECIOUS: %.dot
......@@ -24,8 +29,6 @@ simu: clique3.simu
#compare: clique3.lurette
# cat dijkstra-ring.rif
# make clique3.simu
kind2: clique3.kind2
## do not work because there is a modulo in p.lus, which is not (yet) implemented in ../../bit-blast/*.lus
lesar: clique3.lesar
test/coloring/clique3.dot deleted 100644 → 0
+ 0
− 12
View file @ e20c28d0
graph graph0 {
graph [min_deg=2 mean_deg=2. max_deg=2 is_connected=true is_cyclic=true is_tree=false links_number=3]
p0 [algo="p.ml"]
p1 [algo="p.ml"]
p2 [algo="p.ml"]
p0 -- p1
p0 -- p2
p1 -- p2
}
test/coloring/clique3_oracle.lus deleted 100644 → 0
+ 0
− 26
View file @ e20c28d0
include "clique3.lus"
include "verify.lus"
node topology = clique3;
const an = actions_number;
const pn = card;
node oracle(
p0_color:int;p1_color:int;p2_color:int;
Enab_p0_recolor,Enab_p1_recolor,Enab_p2_recolor:bool;
p0_recolor,p1_recolor,p2_recolor:bool)
returns (ok:bool);
var
Acti:bool^an^pn;
Enab:bool^an^pn;
Stat : state^pn;
nodes : state^pn;
enables : bool^an^pn;
let
Acti = [[p0_recolor],[p1_recolor],[p2_recolor]];
Enab = [[Enab_p0_recolor],[Enab_p1_recolor],[Enab_p2_recolor]];
Stat = [ p0_color, p1_color, p2_color ];
nodes, enables = topology(pre(Acti), Stat);
ok = enables = Enab and boolred<<pn,pn,pn>>(map<<=,pn>>(nodes, Stat));
tel
test/coloring/verify.lus
+ 2
− 1
View file @ 2f4e7e29
......@@ -7,12 +7,13 @@ var
legitimate, closure : bool;
moves : int;
pot :int;
r:bool;rn:int;
let
-- assert(true -> daemon_is_locally_central<<actions_number,card>>(activations, pre enables, adjacency));
assert(true -> daemon_is_central<<actions_number,card>>(activations, pre enables));
assert(rangei<<0,card>>(inits));
config, enables = topology(activations, inits);
config, enables,r,rn = topology(activations, inits);
legitimate = silent<<actions_number,card>>(enables);
closure = true -> (pre(legitimate) => legitimate);
......
test/dijkstra-ring/Makefile
+ 8
− 1
View file @ 2f4e7e29
......@@ -7,11 +7,18 @@ DECO_PATTERN="0:root.ml 1-:p.ml"
include ../Makefile.inc
-include ../Makefile.dot
##############################################################################
# Non-regression tests
test: diring4.lurette diring4.kind2
clean: genclean
rm -f diring*.*
## Some examples of use of ../Makefile.inc
##############################################################################
# Other examples of use
## Some examples of use of ../Makefile.inc
# run a simulation with luciole
simu: diring4.simu
......
test/dijkstra-ring/dijkstra_ring_oracle.lus
+ 17
− 7
View file @ 2f4e7e29
......@@ -4,20 +4,25 @@
include "../../lib/utils.lus"
include "cost.lus"
node _dijkstra_ring_oracle(
node dijkstra_ring_oracle(
legitimate : bool;
ocaml_cost : real;
ocaml_enabled : bool^actions_number^card;
active : bool^actions_number^card;
ocaml_config : state^card;
ocaml_config : state^card;
round:bool;
round_nb:int;
)
returns (ok : bool);
returns (ok : bool;
);
var
lustre_config : state^card;
lustre_enabled : bool^actions_number^card;
lustre_cost:int;
lustre_round:bool;
lustre_round_nb:int;
let
lustre_config, lustre_enabled =
lustre_config, lustre_enabled, lustre_round, lustre_round_nb =
topology(active -> pre active, -- ignored at the first step
ocaml_config -- used at the first step only
);
......@@ -26,11 +31,14 @@ let
-- compare the sasa dot interpretation and the salut dot to lustre compilation
and lustre_config = ocaml_config
-- compare the lustre and the ocaml version of the processes
and Lustre::real2int(ocaml_cost) = lustre_cost;
and Lustre::real2int(ocaml_cost) = lustre_cost
and round = lustre_round
and round_nb = lustre_round_nb
;
-- compare the cost functions
tel
node dijkstra_ring_oracle(
node _dijkstra_ring_oracle(
legitimate : bool;
ocaml_cost : real;
ocaml_enabled : bool^actions_number^card;
......@@ -41,9 +49,11 @@ returns (ok : bool);
var
lustre_config : state^card;
lustre_enabled : bool^actions_number^card;
lustre_round:bool;
lustre_round_nb:int;
let
ok= lustre_enabled[0][0] or true;
lustre_config, lustre_enabled =
lustre_config, lustre_enabled, lustre_round, lustre_round_nb =
topology(active -> pre active, -- ignored at the first step
ocaml_config -- used at the first step only
);
......
test/dijkstra-ring/verify.lus
+ 2
− 1
View file @ 2f4e7e29
......@@ -14,12 +14,13 @@ var
enabled : bool^actions_number^card;
legitimate, at_least_1, closure, converge : bool;
steps, cost : int;
round:bool; round_nb:int;
let
assert(true -> daemon_is_distributed<<actions_number,card>>(active, pre enabled));
-- assert(true -> daemon_is_synchronous<<actions_number,card>>(active, pre enabled));
assert(rangei<<0,card>>(init_config));
config, enabled = topology(active, init_config);
config, enabled, round, round_nb = topology(active, init_config);
assert(config = init_config -> true);
-- stability in this algo means mutual exclusion: exactly 1 node is enabled at a time
......
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