From 5cffc94e42fda5d0d5d5510d43caf28e80fbe24c Mon Sep 17 00:00:00 2001 From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr> Date: Fri, 29 Apr 2022 13:48:26 +0200 Subject: [PATCH] cosmetic changes --- src/dot2lus.ml | 2 +- src/dune | 16 ---------------- test/Makefile.inc | 19 +++++++++++++------ test/token/Makefile | 3 +++ test/token/p.lus | 8 +++++--- test/token/root.lus | 11 +++++++---- test/token/verify.lus | 2 +- 7 files changed, 30 insertions(+), 31 deletions(-) delete mode 100644 src/dune diff --git a/src/dot2lus.ml b/src/dot2lus.ml index 94b12beb..e406a6f5 100644 --- a/src/dot2lus.ml +++ b/src/dot2lus.ml @@ -142,7 +142,7 @@ let output_topology output (graph : Topology.t) name = graph.nodes |> List.iteri (fun i n -> let algo = algo_name n in - let neighbors = graph.succ n.id |> List.map (fun (_, id) -> index_of_id id) in + let neighbors = graph.succ n.id |> List.map (fun id -> index_of_id id) in let deg = List.length neighbors in let nl = sprint_neighbor_list neighbors "p_c" in let pnl = sprint_neighbor_list neighbors "prev_p_c" in diff --git a/src/dune b/src/dune deleted file mode 100644 index f4c25e25..00000000 --- a/src/dune +++ /dev/null @@ -1,16 +0,0 @@ -;; Time-stamp: <modified the 21/11/2021 (at 17:50) by Erwan Jahier> - -(executable - (name dot2lus) - (flags -noassert) - (link_flags (-linkall)) - (libraries ocamlgraph lutils sasacore algo) -) - -(install - (section bin) - (package sasa) - (files (dot2lus.exe as salut)) -; (files sasaRun.cmxa) -) - diff --git a/test/Makefile.inc b/test/Makefile.inc index 821770eb..99a6691a 100644 --- a/test/Makefile.inc +++ b/test/Makefile.inc @@ -21,7 +21,7 @@ clean: rm -f $(TOPOLOGY).ml config.ml rm -f *.rif *.seed rm -f $(TOPOLOGY).lus - rm -f $(TOPOLOGY)_verify.lv4 + rm -f *_verify.lv4 test: $(TOPOLOGY).cmxs $(TOPOLOGY).lus lurette -sut "sasa $(TOPOLOGY).dot $(SASAFLAGS)" -oracle "lv6 $(TOPOLOGY)_oracle.lus -n oracle" @@ -33,16 +33,23 @@ verify: $(TOPOLOGY)_verify.lv4 kind2 $< -$(TOPOLOGY).lus: $(TOPOLOGY).dot +# %(TOPOLOGY).lus: $(TOPOLOGY).dot +%.lus: %.dot $(D2L) $(DOT2LUSFLAGS) $< -$(TOPOLOGY).cmxs: state.ml $(SASA_ALGOS) config.ml $(TOPOLOGY).ml - ocamlfind ocamlopt -package algo -shared $^ -o $@ +LIB=-package algo +OCAMLOPT=ocamlfind ocamlopt -bin-annot -$(TOPOLOGY).ml config.ml: $(TOPOLOGY).dot +%.cmxs: %.ml + $(OCAMLOPT) $(LIB) -shared state.ml $(shell sasa -algo $*.dot) config.ml $< -o $@ + + + +%.ml: %.dot sasa -reg $< # XXX: this method of adding kind2 annotations is brittle -$(TOPOLOGY)_verify.lv4: $(TOPOLOGY)_oracle.lus $(TOPOLOGY).lus verify.lus +%_verify.lv4: %_oracle.lus %.lus verify.lus lv6 $< -n verify --lustre-v4 -o $@ sed -i -e "s/tel/--%MAIN ;\n--%PROPERTY ok;\ntel/" $@ + diff --git a/test/token/Makefile b/test/token/Makefile index 1450b750..b7104cac 100644 --- a/test/token/Makefile +++ b/test/token/Makefile @@ -1,5 +1,8 @@ TOPOLOGY ?= ring3 DOT2LUSFLAGS ?= SASA_ALGOS := p.ml root.ml +DECO_PATTERN="0:root.ml 1-:p.ml" + include ../Makefile.inc +# -include ../../../test/Makefile.dot diff --git a/test/token/p.lus b/test/token/p.lus index cd8fe958..196daf81 100644 --- a/test/token/p.lus +++ b/test/token/p.lus @@ -1,11 +1,13 @@ function p_enable<<const degree:int>>(this : state; neighbors : state^degree) returns (enabled : bool^actions_number); let - enabled = [ this <> neighbors[0] ]; + enabled = [ this <> neighbors[0] ]; tel; -function p_step<<const degree:int>>(this : state; neighbors : state^degree; action : action) +function p_step<<const degree:int>>( + this : state; + neighbors : state^degree; action : action) returns (new : state); let - new = neighbors[0]; + new = neighbors[0]; tel; diff --git a/test/token/root.lus b/test/token/root.lus index 1e00e0cd..44121e80 100644 --- a/test/token/root.lus +++ b/test/token/root.lus @@ -5,17 +5,20 @@ const actions_number = 1; function action_of_int(i : int) returns (a : action); let - a = T; + a = T; tel; function root_enable<<const degree:int>>(this : state; neighbors : state^degree) returns (enabled : bool^actions_number); let - enabled = [ this = neighbors[0] ]; + enabled = [ this = neighbors[0] ]; tel; -function root_step<<const degree:int>>(this : state; neighbors : state^degree; action : action) +function root_step<<const degree:int>>( + this : state; + neighbors : state^degree; + action : action) returns (new : state); let - new = (this + 1) mod card; + new = (this + 1) mod card; tel; diff --git a/test/token/verify.lus b/test/token/verify.lus index e0c1969c..9a9ab63d 100644 --- a/test/token/verify.lus +++ b/test/token/verify.lus @@ -20,7 +20,7 @@ let legitimate = tokens = 1; closure = true -> (pre(legitimate) => legitimate); - steps = (-1 -> pre(steps)) + 1; + steps = 0 -> pre(steps) ; ok = tokens >= 1 -- there should always be at least one token holder and closure and (steps >= 3*card*(card-1)/2 - card - 1 => legitimate); -- worst-case stabilization -- GitLab