Added SDC tests

7 years ago · b0d719dcf2
parent 3a8a3e1ff9
commit b0d719dcf2
8 changed files with 327 additions and 1 deletions
--- a/test/CTestTestfile.cmake
+++ b/test/CTestTestfile.cmake
@ -965,6 +965,11 @@ ADD_TEST(compile_javac_run_tuple_args "scripts/compile_javac_run" "good/tuple_ar
 ADD_TEST(compile_javac_run_type_alias "scripts/compile_javac_run" "good/type_alias.ept")
 ADD_TEST(compile_javac_run_updown "scripts/compile_javac_run" "good/updown.ept")
 ADD_TEST(compile_javac_run_when_merge1 "scripts/compile_javac_run" "good/when_merge1.ept")
+ADD_TEST(compile_sdc_run_alloc "scripts/compile_sdc_run" "sdc/alloc.ept")
+ADD_TEST(compile_sdc_run_lnum_simple "scripts/compile_sdc_run" "sdc/lnum_simple.ept")
 ADD_TEST(compile_sdc_run_modular "scripts/compile_sdc_run" "sdc/modular.ept")
 ADD_TEST(compile_sdc_run_office "scripts/compile_sdc_run" "sdc/office.ept")
+ADD_TEST(compile_sdc_run_optim "scripts/compile_sdc_run" "sdc/optim.ept")
+ADD_TEST(compile_sdc_run_radiotrans "scripts/compile_sdc_run" "sdc/radiotrans.ept")
+ADD_TEST(compile_sdc_run_servers "scripts/compile_sdc_run" "sdc/servers.ept")
 ADD_TEST(compile_sdc_run_tracking "scripts/compile_sdc_run" "sdc/tracking.ept")
--- a/test/sdc/alloc.ept
+++ b/test/sdc/alloc.ept
@ -0,0 +1,51 @@
+node alloc(r,e : bool) returns (g : bool)
+let
+  automaton
+    state Idle
+      do g = false until r then Alloc
+    state Alloc
+      do g = true until e then Idle
+  end
+tel
+
+node main_alloc(r1,r2,e1,e2 : bool) returns (g1,g2 : bool)
+    contract
+    assume not (r1 & r2)
+    enforce not (g1 & g2)
+    with (c1,c2:bool)
+let
+  g1 = inlined alloc(r1 & c1, e1);
+  g2 = inlined alloc(r2 & c2, e2);
+tel
+
+node task<<pr,pe:int>>() returns (r,e:bool)
+let
+    automaton
+    state I
+      var c : int;
+    do
+      r = c = pr;
+      e = false;
+      c = 1 fby c + 1
+    until r then A
+    state A
+        var c : int;
+    do
+      r = false;
+      e = c = pe;
+      c = 1 fby c + 1;
+    until e then I
+    end
+tel
+    
+(* CHECK main *)
+
+node main() returns (ok:bool)
+var r1,r2,e1,e2,g1,g2:bool;
+let
+  (g1,g2) = main_alloc(r1,r2 & not r1,e1,e2);
+  (* task 1 *)
+  (r1,e1) = task<<5,15>>();
+  (r2,e2) = task<<11,27>>();
+  ok = not (g1 & g2);
+tel
--- a/test/sdc/lnum_simple.ept
+++ b/test/sdc/lnum_simple.ept
@ -0,0 +1,47 @@
+(* SDC sS:d={P:D} *)
+
+node f(x:int) = (y:int)
+  contract
+  assume x >= 10
+  enforce y <= x
+  with (c:bool)
+let
+  y = 0 -> if c then pre y + 1 else 0;
+tel
+
+
+node tasks(nb_req, ended : int) = (waiting, active : int)
+      contract
+      assume (nb_req >= 0) & (ended <= (0 fby active)) & (ended >= 0)
+      enforce (active <= 10)
+      with (act : bool)
+var activated : int;
+let
+  waiting = (0 -> pre waiting) + nb_req - activated;
+  activated = 0 -> if (pre waiting > 0) & act then 1 else 0;
+  active = (0 -> pre active) + activated - ended;
+tel  
+
+node period<<n:int>>() = (s:bool)
+var c:int;
+let
+  c = 1 fby (if s then 1 else c + 1);
+  s = c = n;
+tel
+
+fun min(x,y:int) = (z:int)
+let
+    z = if x < y then x else y;
+tel
+
+node main() = (ok:bool;active,ended:int)
+contract assume (active >= 0) & (ended <= (0 fby active)) & (ended >= 0)
+var x,y,nb_req,waiting:int;
+let
+  y = f(x);
+  x = 20;
+  nb_req = 0 -> if (pre waiting < 100) & period<<17>>() then 23 else 0;
+  ended = 0;
+  (waiting,active) = tasks(nb_req,ended);
+  ok = (y <= x) & (active <= 9)
+tel
--- a/test/sdc/modular.ept
+++ b/test/sdc/modular.ept
@ -27,6 +27,7 @@ let
    z = f(u & c, m)
 tel

+(* CHECK main *)
 node main() = (ok:bool)
 var u : bool;
    m : t;
--- a/test/sdc/optim.ept
+++ b/test/sdc/optim.ept
@ -0,0 +1,24 @@
+node f(x:bool) = (last y:int)
+  contract
+  enforce y > 0 with (c:bool)
+let
+    automaton
+    state A
+    do y = 1;
+    until  c then B
+    | not c then C
+    state B
+    do y = 2;
+    until true then A
+    state C
+    do y = 3;
+    until true then A
+    end
+tel
+
+
+node main() = (y:int)
+let
+    y = f(true)
+tel
+    
--- a/test/sdc/radiotrans.ept
+++ b/test/sdc/radiotrans.ept
@ -0,0 +1,141 @@
+  (* Example from Nicolas Berthier *)
+
+node transceiver(enter_tx,
+		 enter_rx,
+		 exit_rx,
+		 calibrate,
+		 sleep,
+		 wake_up,
+		 irq_tx_done,
+		 irq_on_packet,
+		 irq_end_of_packet,
+		 irq_end_of_calibration,
+		 irq_fifo_threshold,
+		 ok:bool) returns (red:bool)
+let
+  automaton
+    state Idle
+      do
+	red = false;
+      until enter_tx & ok then Tx
+          | calibrate & ok then Calibrate
+          | sleep & ok then Sleep
+          | enter_rx & ok then Rx
+    state Tx
+      do
+	red = true;
+      until irq_tx_done then Idle
+    state Calibrate
+      do
+	red = false;
+      until irq_end_of_calibration then Idle
+    state Sleep
+      do
+	red = false;
+      until wake_up & ok then Idle
+    state Rx
+      do
+	red = true;
+      until irq_on_packet then Rx_Packet
+          | exit_rx & ok then Idle
+    state Rx_Packet
+      do
+	red = true;
+      until irq_end_of_packet then Idle
+  end
+tel
+
+node adc(adc_on,adc_off,ok:bool) returns (o:bool)
+let
+  automaton
+    state Off
+      do
+	o = false;
+      until adc_on & ok then On
+    state On
+      do
+	o = true;
+      until adc_off & ok then Off
+  end
+tel
+
+node main_rt(enter_tx,
+	     enter_rx,
+	     exit_rx,
+	     calibrate,
+	     sleep,
+	     wake_up,
+	     irq_tx_done,
+	     irq_on_packet,
+	     irq_end_of_packet,
+	     irq_end_of_calibration,
+	     irq_fifo_threshold,adc_on,adc_off:bool)
+    returns (a_on,red:bool)
+
+contract
+    enforce (not (a_on & red)) with (ok_r,ok_a:bool)
+
+let
+  a_on = inlined adc(adc_on,adc_off,ok_a);
+  red = inlined transceiver(enter_tx,
+			    enter_rx,
+			    exit_rx,
+			    calibrate,
+			    sleep,
+			    wake_up,
+			    irq_tx_done,
+			    irq_on_packet,
+			    irq_end_of_packet,
+			    irq_end_of_calibration,
+			    irq_fifo_threshold,ok_r);
+tel
+
+node period<<n,ini:int>>() = (s:bool)
+var c:int;
+let
+  c = ini fby (if s then 1 else c + 1);
+  s = c = n;
+tel
+
+    
+(* CHECK main *)
+node main() returns (ok:bool)
+var enter_tx,
+  enter_rx,
+  exit_rx,
+  calibrate,
+  sleep,
+  wake_up,
+  irq_tx_done,
+  irq_on_packet,
+  irq_end_of_packet,
+  irq_end_of_calibration,
+  irq_fifo_threshold,adc_on,adc_off:bool;
+  a_on,red:bool;
+let
+  (a_on,red) = main_rt(enter_tx,
+	                 enter_rx,
+	                 exit_rx,
+	                 calibrate,
+	                 sleep,
+	                 wake_up,
+	                 irq_tx_done,
+	                 irq_on_packet,
+	                 irq_end_of_packet,
+	                 irq_end_of_calibration,
+	                 irq_fifo_threshold,adc_on,adc_off);
+  ok = not (a_on & red);
+  enter_tx = period<<27,25>>();
+  enter_rx = period<<27,9>>();
+  exit_rx = period<<27,1>>();
+  calibrate = period<<27,19>>();
+  sleep = period<<27,14>>();
+  wake_up = period<<27,11>>();
+  irq_tx_done = period<<27,21>>();
+  irq_on_packet = period<<27,8>>();
+  irq_end_of_packet = period<<27,4>>();
+  irq_end_of_calibration = period<<27,16>>();
+  irq_fifo_threshold = period<<27,3>>();
+  adc_on = period<<17,13>>();
+  adc_off = period<<17,4>>();
+tel
--- a/test/sdc/servers.ept
+++ b/test/sdc/servers.ept
@ -0,0 +1,43 @@
+type mode = H | M | L
+
+node server(max:int) = (load:int)
+  contract
+  assume (max >= 5)
+  enforce (load <= max)
+  with (c:mode)
+let
+  switch c
+  | H do load = 20
+  | M do load = 10
+  | L do load = 0
+  end
+tel
+
+type degmode = Normal | Degraded
+  
+node degraded_server(max:int) = (load:int)
+  contract
+  assume (max >= 10)
+  enforce (load <= max)
+with (cm:mode;cd:degmode)
+let
+    switch cd
+    | Normal do
+        switch cm
+        | H do load = 20
+        | M do load = 10
+        | L do load = 0
+        end
+    | Degraded do load = 2
+    end
+tel
+
+(* CHECK main *)
+node main() = (ok:bool)
+  var max, load1, load2 : int;
+let
+    load1 = 0;
+  load2 = degraded_server(max);
+  max = 10;
+  ok = (load1 <= max) & (load2 <= max);
+tel
--- a/test/sdc/tracking.ept
+++ b/test/sdc/tracking.ept
@ -111,7 +111,21 @@ let
 tel 


-
+(* CHECK main *)
+node main() = (ok:bool)
+var i_objvt, i_deadline, i_indice :level; s, e : bool;
+  objectives:bool; st_objvt, st_deadline, st_indice :level; res: int; wEx: elevel; win : wSize; running : bool;
+  l : int;
+let
+  (objectives,st_objvt,st_deadline,st_indice,res,wEx,win,running) = tracking(i_objvt,i_deadline,i_indice,s,e);
+  i_objvt = None fby None fby High fby None fby Bad fby None fby None fby Low fby None fby Low fby None fby Normal fby None fby i_objvt;
+  i_deadline = None fby Normal fby None fby None fby Normal fby None fby High fby None fby Low fby None fby None fby Bad fby None fby None fby None fby High fby None fby i_deadline;
+  i_indice = None fby None fby None fby Normal fby High fby Low fby None fby None fby Bad fby Bad fby None fby i_indice;
+  l = 0 fby (if l = 17 then 0 else l + 1);
+  s = (l = 7);
+  e = (l = 17);
+  ok = objectives;
+tel

 (*