Commit 91b5bbd5 authored by erwan's avatar erwan
Browse files

test: add an example to illustrate the use of lurette coverage

to check is the worst-case has been reached
parent 771cdf80
Pipeline #72317 passed with stages
in 5 minutes and 34 seconds
# Time-stamp: <modified the 11/05/2021 (at 16:46) by Erwan Jahier>
# Time-stamp: <modified the 28/07/2021 (at 11:44) by Erwan Jahier>
test: ring.cmxs lurette1 rdbg_test
......@@ -52,4 +52,4 @@ lurette1: ring.lut ring_oracle.lus
-include Makefile.untracked
clean: genclean
rm -f ring_oracle.lus ring.ml
rm -f ring.ml
-- Automatically generated by /home/jahier/.opam/4.12.0/bin/sasa version "v4.5.2" ("6122a58")
-- on crevetete the 28/7/2021 at 11:23:11
--sasa -glos ring.dot
include "dijkstra_ring_oracle.lus"
const an=1; -- actions number
const pn=8; -- processes number
const degree=2;
const min_degree=2;
const mean_degree=2.000000;
const diameter=7;
const card=8;
const links_number=8;
const is_cyclic=true;
const is_connected=true;
const is_a_tree=false;
const f=false;
const t=true;
const adjacency=[
[f,t,f,f,f,f,f,f],
[f,f,t,f,f,f,f,f],
[f,f,f,t,f,f,f,f],
[f,f,f,f,t,f,f,f],
[f,f,f,f,f,t,f,f],
[f,f,f,f,f,f,t,f],
[f,f,f,f,f,f,f,t],
[t,f,f,f,f,f,f,f]];
const k=3;
node oracle(legitimate:bool;
root_c:int;p2_c:int;p3_c:int;p4_c:int;p5_c:int;p6_c:int;p7_c:int;p8_c:int;
Enab_root_T,Enab_p2_T,Enab_p3_T,Enab_p4_T,Enab_p5_T,Enab_p6_T,Enab_p7_T,Enab_p8_T:bool;
root_T,p2_T,p3_T,p4_T,p5_T,p6_T,p7_T,p8_T:bool)
returns (ok, WCReached:bool);
var
Acti:bool^an^pn;
Enab:bool^an^pn;
let
Acti = [[root_T],[p2_T],[p3_T],[p4_T],[p5_T],[p6_T],[p7_T],[p8_T]];
Enab = [[Enab_root_T],[Enab_p2_T],[Enab_p3_T],[Enab_p4_T],[Enab_p5_T],[Enab_p6_T],[Enab_p7_T],[Enab_p8_T]];
ok, WCReached = dijkstra_ring_oracle_cov(legitimate, Enab, Acti);
tel
Markdown is supported
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