Skip to content
Snippets Groups Projects
Commit c530ae32 authored by erwan's avatar erwan
Browse files

Test: add a missing file to fic the CI

parent 97b9b2ac
No related branches found
No related tags found
No related merge requests found
Pipeline #26805 failed
include "../lustre/oracle_utils.lus"
-----------------------------------------------------------------------------
node theorem_6_29<<const m : int; const n: int>> (Enab, Acti: bool^m^n) returns (res:bool);
var
Silent:bool;
MoveNb:int ;
let
Silent = silent<<m,n>>(Enab);
MoveNb = 1 -> pre(MoveNb) + 1;
res = (k>=n)=>((((3*n*(n-1))/2)<MoveNb)=>Silent) ; -- Theorem 6.29
tel
-----------------------------------------------------------------------------
node lemma_6_28<<const m : int; const n: int>> (Enab, Acti: bool^m^n) returns (res:bool);
var
Xn:int;
Silent:bool;
MoveNb:int;
let
Xn = 0 -> if(Acti[0][0]) then pre(Xn) + 1 else pre(Xn) ;
Silent = silent<<m,n>>(Enab);
MoveNb = move_count(Acti);
res = (((n*(n-1)/2) + Xn*n)<MoveNb) => Silent ; -- Lemma 6.28
tel
-----------------------------------------------------------------------------
node dijkstra_ring_oracle<<const an:int; const pn:int>> (Enab, Acti: bool^an^pn)
returns (ok:bool);
let
ok = lemma_6_28 <<an,pn>> (Enab, Acti) and
theorem_6_29<<an,pn>> (Enab, Acti);
tel
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment