diff --git a/.gitignore b/.gitignore index ff68d4104f3c8b28790f0d0c119fa6a27624038a..0b5c024eccfbd9f780b5f789262da9cc91a125e4 100644 --- a/.gitignore +++ b/.gitignore @@ -15,14 +15,20 @@ rdbg-session*.ml *.jpg *.bak *.save -*.lus +*.res *.lut +clique*.lus +ER*.lus flymd.html log *.sh +*.c +*.h test/**/*.ml !test/**/p.ml +!test/**/root.ml !test/**/state.ml +!test/**/config.ml results Makefile.local .ocamldebug diff --git a/salut/lib/sas.lus b/salut/lib/sas.lus index e8ea5cc1fdd13cccd90dcb6e2366387f52653d51..c08c234a4921b3ca1b7b2c9603ad54652e354261 100644 --- a/salut/lib/sas.lus +++ b/salut/lib/sas.lus @@ -1,6 +1,6 @@ include "utils.lus" include "bitset.lus" -include "../../test/lustre/round.lus" +-- include "../../test/lustre/round.lus" -- No nodes enabled, the network is silent. function silent<<const an:int; const pn:int>>(enab: bool^an^pn) diff --git a/salut/test/Makefile.inc b/salut/test/Makefile.inc index 544d39d973f9b356f24ff09d2c1946d1c5f8e744..f351140cf3cc5876e667c27927b2e5b5a16b2272 100644 --- a/salut/test/Makefile.inc +++ b/salut/test/Makefile.inc @@ -31,7 +31,8 @@ genclean: LIB=-package algo OCAMLOPT=ocamlfind ocamlopt -bin-annot -LIB_LUS=$(HOME)/sasa/test/lustre/round.lus $(HOME)/sasa/salut/lib/sas.lus +SELF_DIR := $(dir $(lastword $(MAKEFILE_LIST))) +LIB_LUS=${SELF_DIR}../../test/lustre/round.lus ${SELF_DIR}../lib/sas.lus # $(HOME)/sasa/test/lustre/oracle_utils.lus diff --git a/test/unison/config.ml b/test/unison/config.ml new file mode 100644 index 0000000000000000000000000000000000000000..7dc3ade929911d0621a183dbb1fdb30793b48849 --- /dev/null +++ b/test/unison/config.ml @@ -0,0 +1,17 @@ + +let potential = None (* None => only -sd, -cd, -lcd, -dd, or -custd are possible *) +let fault = None (* None => the simulation stop once a legitimate configuration is reached *) + +let fault = None + +let legitimate pidl from_pid = + (* a legitimate configuration is reached when all states have the same values *) + let v = fst(from_pid (List.hd pidl)) in + List.fold_left + (fun acc pid -> acc && fst(from_pid pid) = v) + true + (List.tl pidl) + +let legitimate = Some legitimate +let init_search_utils = None +