surete tp1

surete/tp1/sequential/Makefile

@@ -0,0 +1,22 @@
+LUCIOLE=luciole
+LUSTRE=lv6
+LESAR=lesar
+
+run:
+	 $(LUCIOLE) sequential.lus $(node)
+#	 $(LUCIOLE) $(LUSTRE) sequential.lus -node $(node) -exec
+
+always:
+	 make node=always run
+	 
+count_true:
+	 make node=count_true run
+	 
+count_succ_true:
+	 make node=count_succ_true run
+	 
+bounds:
+	 make node=bounds run
+	 
+clean:
+	 rm luciole.rif

surete/tp1/sequential/always.ec

@@ -0,0 +1,13 @@
+node always
+  (i: bool)
+returns
+  (o: bool);
+
+var
+  V4_prev: bool;
+
+let
+  o = (if i then V4_prev else false);
+  V4_prev = (true -> (pre o));
+tel
+

surete/tp1/sequential/bounds.ec

@@ -0,0 +1,17 @@
+node bounds
+  (i: int)
+returns
+  (min: int;
+  max: int);
+
+var
+  V18_prev_min: int;
+  V19_prev_max: int;
+
+let
+  min = (if (i < V18_prev_min) then i else V18_prev_min);
+  max = (if (i > V19_prev_max) then i else V19_prev_max);
+  V18_prev_min = (i -> (pre min));
+  V19_prev_max = (i -> (pre max));
+tel
+

surete/tp1/sequential/count_succ_true.ec

@@ -0,0 +1,15 @@
+node count_succ_true
+  (i: bool)
+returns
+  (o: int);
+
+var
+  V12_prev_i: bool;
+  V13_prev_o: int;
+
+let
+  o = (if (i and V12_prev_i) then (V13_prev_o + 1) else V13_prev_o);
+  V12_prev_i = (false -> (pre i));
+  V13_prev_o = (0 -> (pre o));
+tel
+

surete/tp1/sequential/count_true.ec

@@ -0,0 +1,13 @@
+node count_true
+  (i: bool)
+returns
+  (o: int);
+
+var
+  V8_prev: int;
+
+let
+  o = (if i then (V8_prev + 1) else V8_prev);
+  V8_prev = (0 -> (pre o));
+tel
+

surete/tp1/sequential/sequential.lus

@@ -0,0 +1,32 @@
+node always(i : bool) returns (o : bool);
+var prev : bool;
+let
+  prev = true -> pre o;
+  o = if i then prev else false; 
+tel
+
+node count_true(i : bool) returns (o : int);
+var prev : int;
+let
+  prev = 0 -> pre o;
+  o = if i then prev + 1 else prev;
+tel
+
+node count_succ_true(i : bool) returns (o : int);
+var
+  prev_i : bool;
+  prev_o : int;
+let
+  prev_i = false -> pre i;
+  prev_o = 0 -> pre o;
+  o = if i and prev_i then prev_o + 1 else prev_o;
+tel
+
+node bounds(i : int) returns (min, max : int);
+var prev_min, prev_max : int;
+let
+  prev_min = i -> pre min;
+  prev_max = i -> pre max;
+  min = if (i < prev_min) then i else prev_min;
+  max = if (i > prev_max) then i else prev_max;
+tel

surete/tp1/temp_prop/after.ec

@@ -0,0 +1,13 @@
+node after
+  (a: bool)
+returns
+  (o: bool);
+
+var
+  V4_prev_o: bool;
+
+let
+  o = (V4_prev_o or a);
+  V4_prev_o = (false -> (pre o));
+tel
+

surete/tp1/temp_prop/always_since.ec

@@ -0,0 +1,14 @@
+node always_since
+  (a: bool;
+  b: bool)
+returns
+  (o: bool);
+
+var
+  V9_prev_o: bool;
+
+let
+  o = (if b then a else (V9_prev_o and a));
+  V9_prev_o = (false -> (pre o));
+tel
+

surete/tp1/temp_prop/build.sh

@@ -0,0 +1,15 @@
+#!/bin/sh
+set -e
+cd "$(dirname "$(realpath "$0")")"
+
+
+if [ $# -lt 1 ]
+then echo "Usage: ./build.sh <node>" && exit 1
+fi
+
+
+node="$1"
+src=./nodes.lus
+
+
+luciole $src "$node"

surete/tp1/temp_prop/nodes.lus

@@ -0,0 +1,30 @@
+
+node after (a: bool) returns (o: bool);
+var prev_o: bool;
+let
+  prev_o = false -> pre o;
+  o = prev_o or a;
+tel;
+
+node always_since (a: bool; b: bool) returns (o: bool);
+var prev_o: bool;
+let
+  prev_o = false -> pre o;
+  o = if b then a else prev_o and a;
+tel;
+
+node once_since(a: bool; reset: bool) returns (o: bool);
+var a_happened: bool;
+let
+  a_happened = a -> if reset then false else (pre a_happened or a);
+  o = (a and not reset) -> a_happened;
+tel;
+
+node always_from_to(b: bool; reset: bool; c: bool) returns (x: bool);
+var
+  c_happened: bool;
+  prev_b: bool;
+let
+  c_happened = c -> if reset then false else (c or pre c_happened);*
+  prev_b = b -> if reset then true else (b and prev_b);
+tel;

surete/tp1/temp_prop/once_since.ec

@@ -0,0 +1,15 @@
+node once_since
+  (a: bool;
+  reset: bool)
+returns
+  (o: bool);
+
+var
+  V14_a_happened: bool;
+
+let
+  o = ((a and (not reset)) -> V14_a_happened);
+  V14_a_happened = (a -> (if reset then false else ((pre V14_a_happened) or a))
+  );
+tel
+