%Patch files loaded: patch2 version 1.2.2.36 $$$TimerGeneral.pvs TimerGeneral [K:posreal] : THEORY BEGIN IMPORTING Held_For[K] t, t_h: VAR clock P:var pred[clock] timeout : var posreal%time CurrentP:var bool previous:var clock TimerUpdate(CurrentP,timeout,previous):clock= TABLE %------------------------------------% |[previous=timeout]| %----------------------------------------------------% |CurrentP |next(previous) |previous || %----------------------------------------------------% |NOT CurrentP |0 |0 || %----------------------------------------------------% ENDTABLE Timer(P,timeout)(t):RECURSIVE clock= TABLE %--------------------------------------------------------------------------------% |[init(t) | NOT init(t) ]| %--------------------------------------------------------------------------------% |TimerUpdate(P(t),timeout,0) | TimerUpdate(P(t),timeout,Timer(P,timeout)(pre(t)))|| %--------------------------------------------------------------------------------% ENDTABLE MEASURE rank(t) Timer_Lemma2: lemma Timer(P,timeout)(t)>0 IMPLIES P(t) Timer_Lemma3: lemma Timer(P,timeout)(t)>=timeout IMPLIES t>=0 Timer_Lemma4: lemma t >= floor((t_h - timeout) / K) * K & t <= t_h AND P(t) AND NOT init(t) AND Timer(P,timeout)(pre(t))>=timeout-(t_h-t) IMPLIES t>=timeout-(t_h-t) Timer_General1: THEOREM FORALL(t|NOT init(t)): Held_For(P,timeout)(t) IMPLIES P(t) AND Timer(P,timeout)(pre(t))>=timeout Timer_General2: THEOREM FORALL(t|NOT init(t)): P(t) AND Timer(P,timeout)(pre(t))>=timeout IMPLIES Held_For(P,timeout)(t) Timer_General: THEOREM IF init(t) THEN FALSE ELSE P(t) AND Timer(P,timeout)(pre(t))>=timeout ENDIF = Held_For(P,timeout)(t) END TimerGeneral $$$TimerGeneral.prf (|Clocks| (|clock_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|pre_TCC1| "" (SKOLEM-TYPEPRED) (("" (SKOLEM-TYPEPRED) (("" (SPLIT) (("1" (GRIND) (("1" (DELETE -3) (("1" (CASE "n!1>0") (("1" (ASSERT) (("1" (LEMMA "both_sides_times_pos_ge1") (("1" (INST -1 "K" "n!1-1" "0") (("1" (SIMPLIFY) (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (INST 1 "n!1-1") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "init") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|next_TCC1| "" (SKOLEM-TYPEPRED) (("" (SPLIT) (("1" (SKOLEM-TYPEPRED) (("1" (INST 1 "n!1+1") (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (SKOLEM-TYPEPRED) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) (|rank_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|clock_induct| "" (SKOSIMP) (("" (SKOLEM!) (("" (INST -1 "x!1" "rank(x!1)") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|clock_induction| "" (SKOSIMP) (("" (LEMMA "clock_induct" ("P" "P!1")) (("" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (DELETE 2) (("2" (INDUCT "n") (("1" (SKOSIMP) (("1" (INST -2 "x!1") (("1" (GRIND) (("1" (LEMMA "div_eq_zero" ("x" "x!1" "n0z" "K")) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (GROUND) (("2" (INST -1 "pre(x!1)") (("1" (INST -4 "x!1") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|clock_strong_induction| "" (LEMMA "clock_induction") (("" (SKOSIMP*) (("" (INST -1 "(LAMBDA (n:clock): (FORALL (m:clock): m <= n IMPLIES P!1(m)))") (("" (BETA) (("" (SPLIT) (("1" (INST -1 "t!1") (("1" (INST -1 "t!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST -3 0) (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (INST -3 "m!1") (("3" (ASSERT) (("3" (SKOSIMP) (("3" (INST -1 "z!1") (("3" (GRIND) (("3" (HIDE 2 3 4) (("3" (TYPEPRED "m!1" "z!1" "t!2" "K") (("3" (BOTH-SIDES "/" "K" -7) (("1" (BOTH-SIDES "/" "K" -9) (("1" (BOTH-SIDES "/" "K" -10) (("1" (BOTH-SIDES "/" "K" 2) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) (|Held_For| (|heldfor_TCC1| "" (TERMINATION-TCC) NIL NIL) (|le_inner_clockvar| "" (GRIND) (("" (CASE "floor(n!2)<=n!1") (("1" (GRIND) (("1" (CASE "floor(n!2)=n!2") (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" 1) (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL) ("2" (GRIND) (("2" (BOTH-SIDES "/" "K" -11) (("2" (GRIND) (("2" (BOTH-SIDES "/" "K" -9) (("2" (GRIND) (("2" (CASE "n!1 * K / K=n!1") (("1" (REPLACE -1 -10 LR) (("1" (CASE "n!2* K / K=n!2") (("1" (REPLACE -1 -13 LR) (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" -12) (("1" (CASE "(K + n!1 * K) / K=n!1+1") (("1" (REPLACE -1 -13 LR) (("1" (GRIND) NIL NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|ge_inner_clockvar| "" (GRIND) (("" (CASE "floor(n!2)>=n!1+1") (("1" (GRIND) (("1" (CASE "floor(n!2)=n!2") (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" 1) (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL) ("2" (GRIND) (("2" (BOTH-SIDES "/" "K" -11) (("2" (GRIND) (("2" (BOTH-SIDES "/" "K" -9) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) (|Held_For2|) (|TimerGeneral| (|TimerUpdate_TCC1| "" (COND-DISJOINT-TCC) NIL NIL) (|TimerUpdate_TCC2| "" (COND-COVERAGE-TCC) NIL NIL) (|TimerUpdate_TCC3| "" (SKOSIMP) (("" (INST 2 "0") (("" (GRIND) NIL NIL)) NIL)) NIL) (|TimerUpdate_TCC4| "" (COND-COVERAGE-TCC) NIL NIL) (|TimerUpdate_TCC5| "" (COND-DISJOINT-TCC) NIL NIL) (|Timer_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|Timer_TCC2| "" (TERMINATION-TCC) NIL NIL) (|Timer_TCC3| "" (COND-DISJOINT-TCC) NIL NIL) (|Timer_Lemma2| "" (INDUCT "t" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL) (|Timer_Lemma3| "" (INDUCT "t" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL) (|Timer_Lemma4| "" (INDUCT "t" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (SKOSIMP) (("2" (SKOSIMP) (("2" (INST -1 "P!1" "t_h!1" "timeout!1") (("2" (BDDSIMP) (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL) ("3" (ASSERT) (("3" (EXPAND "Timer" -4) (("3" (GRIND) NIL NIL)) NIL)) NIL) ("4" (CASE "timeout!1 - (t_h!1 - t!1)>0 OR timeout!1 - (t_h!1 - t!1)<=0") (("1" (BDDSIMP) (("1" (LEMMA "Timer_Lemma2") (("1" (INST -1 "P!1" "pre(t!1)" "timeout!1") (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (HIDE -5) (("2" (GRIND) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL) ("5" (GRIND) NIL NIL) ("6" (CASE "t!1<=t_h!1-timeout!1 OR t!1>t_h!1-timeout!1") (("1" (BDDSIMP) (("1" (HIDE -5) (("1" (GRIND) NIL NIL)) NIL) ("2" (CASE "t!1>floor((t_h!1 - timeout!1) / K) * K") (("1" (HIDE -6) (("1" (GRIND) (("1" (HIDE -2 -3 -4 -5) (("1" (HIDE 2 3) (("1" (GRIND) (("1" (TYPEPRED "t!1") (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" -4) (("1" (BOTH-SIDES "/" "K" 2) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (CASE "t_h!1 - timeout!1>floor((t_h!1 - timeout!1) / K) * K") (("1" (HIDE -6) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -1 -2 -3 -4 -5) (("2" (HIDE 2 3 4 5) (("2" (BOTH-SIDES "/" "K" 1) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Timer_General1| "" (SKOSIMP) (("" (EXPAND "Held_For") (("" (SKOSIMP) (("" (CASE "FORALL (t: clock[K] | NOT init(t)& t >= t_j!1 & t <= t!1 ):Timer(P!1,timeout!1)(pre(t))>=timeout!1-(t!1-t) AND P!1(t)") (("1" (INST -1 "t!1") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL) ("2" (BDDSIMP) (("1" (HIDE 1) (("1" (REVEAL 1) (("1" (HIDE 2) (("1" (INDUCT "t" 1 "clock_induction") (("1" (TYPEPRED "t!2") (("1" (PROPAX) NIL NIL)) NIL) ("2" (TYPEPRED "t!2") (("2" (PROPAX) NIL NIL)) NIL) ("3" (GRIND) NIL NIL) ("4" (GRIND) NIL NIL) ("5" (GRIND) NIL NIL) ("6" (GRIND) NIL NIL) ("7" (GRIND) NIL NIL) ("8" (SKOSIMP) (("8" (BDDSIMP) (("1" (INST -5 "t!2") (("1" (GRIND) NIL NIL)) NIL) ("2" (EXPAND "init") (("2" (REPLACE -1 * LR) (("2" (EXPAND "pre") (("2" (CASE "t!2>t_j!1 OR t!2=t_j!1") (("1" (BDDSIMP) (("1" (CASE "t_j!1=0") (("1" (GRIND) NIL NIL) ("2" (ASSERT) (("2" (SIMPLIFY) (("2" (HIDE 3) (("2" (GRIND) (("2" (TYPEPRED "t_j!1") (("2" (GRIND) (("2" (CASE "K>n!1*K") (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" -1) (("1" (BOTH-SIDES "/" "K" 1) (("1" (GRIND) NIL NIL)) NIL) ("2" (GRIND) (("2" (BOTH-SIDES "*" "K" 1) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "timeout!1 - (t!1 - t!2)<=0") (("1" (GRIND) NIL NIL) ("2" (HIDE 3) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (INST -6 "t!2") (("3" (GRIND) NIL NIL)) NIL) ("4" (CASE "NOT init(pre(t!2))") (("1" (GRIND) NIL NIL) ("2" (EXPAND "Timer" 2) (("2" (ASSERT) (("2" (EXPAND "TimerUpdate") (("2" (ASSERT) (("2" (EXPAND "init") (("2" (EXPAND "pre") (("2" (EXPAND "next") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("5" (INST -4 "t!2") (("5" (GRIND) NIL NIL)) NIL) ("6" (HIDE 3) (("6" (GRIND) NIL NIL)) NIL) ("7" (INST -4 "t!2") (("7" (GRIND) NIL NIL)) NIL) ("8" (CASE "t!2=t_j!1 OR t!2>t_j!1") (("1" (BDDSIMP) (("1" (REPLACE -1 * LR) (("1" (CASE "timeout!1 - (t!1 - t_j!1)<=0") (("1" (GRIND) NIL NIL) ("2" (HIDE 4) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE 3) (("2" (GRIND) (("2" (TYPEPRED "t!2") (("2" (TYPEPRED "t_j!1") (("2" (GRIND) (("2" (BOTH-SIDES "/" "K" 2) (("2" (BOTH-SIDES "/" "K" -7) (("2" (BOTH-SIDES "/" "K" -8) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 4) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Timer_General2| "" (SKOLEM!) (("" (BDDSIMP) (("" (EXPAND "Held_For") (("" (INST 1 "floor((t!1-timeout!1)/K)*K") (("1" (CASE "FORALL (t_h: clock[K] | t_h >= floor((t!1 - timeout!1) / K) * K & t_h <= t!1 & NOT init(t_h)): P!1(t_h) AND Timer(P!1,timeout!1)(pre(t_h))>=timeout!1-(t!1-t_h) IMPLIES FORALL (t: clock[K] | t >= floor((t!1 - timeout!1) / K) * K & t <= t_h): P!1(t)") (("1" (INST -1 "t!1") (("1" (BDDSIMP) (("1" (CASE "t!1-timeout!1>=floor((t!1 - timeout!1) / K) * K") (("1" (GRIND) NIL NIL) ("2" (HIDE 2) (("2" (NAME-REPLACE "y!1" "t!1-timeout!1") (("2" (HIDE -2 -3) (("2" (GRIND) (("2" (BOTH-SIDES "/" "K") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL) ("2" (HIDE 2) (("2" (CASE "t!1-timeout!1>=floor((t!1 - timeout!1) / K) * K") (("1" (GRIND) NIL NIL) ("2" (HIDE -2 -1) (("2" (GRIND) (("2" (HIDE 2) (("2" (BOTH-SIDES "/" "K") (("2" (NAME-REPLACE "y!1" "(t!1 - timeout!1) / K") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (HIDE -2) (("2" (INDUCT "t_h" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL) ("3" (GRIND) NIL NIL) ("4" (SKOSIMP) NIL NIL) ("5" (SKOSIMP) (("5" (BDDSIMP) (("1" (CASE "t!2=K") (("1" (REPLACE -1 * LR) (("1" (REPLACE -1 * RL) (("1" (REPLACE -1 * LR) (("1" (CASE "timeout!1 - (t!1 - K)<=0 OR timeout!1 - (t!1 - K)>0") (("1" (BDDSIMP) (("1" (CASE "floor((t!1 - timeout!1) / K) * K>=K") (("1" (SKOSIMP) (("1" (TYPEPRED "t!3") (("1" (CASE "t!3>=K") (("1" (HIDE -13) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -12) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -7) (("2" (CASE "t!1-timeout!1>=K") (("1" (HIDE 2 3) (("1" (NAME-REPLACE "y!1" "t!1-timeout!1") (("1" (GRIND) (("1" (BOTH-SIDES "/" "K") (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" -1) (("1" (NAME-REPLACE "z!1" "y!1/K") (("1" (GRIND) NIL NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (BOTH-SIDES "*" "K" -1) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (CASE "t!3=K or t!3=0") (("1" (BDDSIMP) (("1" (ASSERT) NIL NIL) ("2" (ASSERT) (("2" (GRIND) NIL NIL)) NIL)) NIL) ("2" (TYPEPRED "t!3") (("2" (BDDSIMP) (("2" (CASE "t!3pre(t!2)") (("1" (BDDSIMP) (("1" (INST -2 "t!3") NIL NIL) ("2" (ASSERT) (("2" (TYPEPRED "t!3") (("2" (CASE "t!3=t!2") (("1" (GRIND) NIL NIL) ("2" (TYPEPRED "t!2") (("2" (GRIND) (("2" (HIDE -1 -2 -3 -4 -5 -6) (("2" (CASE "n!2<=n!1") (("1" (CASE "n!2>n!1-1") (("1" (GRIND) NIL NIL) ("2" (BOTH-SIDES "*" "K" 1) (("2" (GRIND) NIL NIL)) NIL)) NIL) ("2" (BOTH-SIDES "*" "K" 1) (("2" (ASSERT) (("2" (GRIND) (("2" (BOTH-SIDES "/" "K" -1) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("3" (CASE "timeout!1 - (t!1 - t!2)=0 OR timeout!1 - (t!1 - t!2)>0 OR timeout!1 - (t!1 - t!2)<0") (("1" (BDDSIMP) (("1" (CASE "t!2=t!1-timeout!1") (("1" (REPLACE -1 * LR) (("1" (REPLACE -1 * RL) (("1" (REPLACE -1 * LR) (("1" (REPLACE -1 * RL) (("1" (ASSERT) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL) ("2" (LEMMA "Timer_Lemma2") (("2" (INST -1 "P!1" "pre(t!2)" "timeout!1") (("2" (BDDSIMP) (("1" (EXPAND "Timer" -6) (("1" (GRIND) NIL NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("3" (HIDE -5 -6 1 2) (("3" (CASE "t!2 floor((t!1 - timeout!1) / K) * K OR t!2 = floor((t!1 - timeout!1) / K) * K") (("1" (BDDSIMP) (("1" (HIDE -2) (("1" (GRIND) NIL NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL) ("4" (CASE "timeout!1 - (t!1 - t!2)=0 OR timeout!1 - (t!1 - t!2)<0 OR timeout!1 - (t!1 - t!2)>0") (("1" (BDDSIMP) (("1" (CASE "t!2=t!1-timeout!1") (("1" (REPLACE -1 * LR) (("1" (REPLACE -1 * RL) (("1" (HIDE -6) (("1" (CASE "floor((t!1 - timeout!1) / K) * K=t!2") (("1" (GRIND) NIL NIL) ("2" (CASE "floor((t!1 - timeout!1) / K) * K=floor((t!2)/K)*K") (("1" (CASE "t!2=floor((t!2) / K) * K") (("1" (GRIND) NIL NIL) ("2" (ASSERT) (("2" (HIDE 2 3 4 5) (("2" (TYPEPRED "t!2") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL) ("2" (CASE "t!2 floor((t!1 - timeout!1) / K) * K OR t!2 = floor((t!1 - timeout!1) / K) * K") (("1" (BDDSIMP) (("1" (HIDE -5) (("1" (HIDE 2 3) (("1" (TYPEPRED "t!2") (("1" (GRIND) (("1" (CASE "n!1>=floor((t!1 - timeout!1) / K)+1") (("1" (ASSERT) (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" 2) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2 3) (("2" (HIDE -5 -6) (("2" (BOTH-SIDES "/" "K" -4) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -5) (("2" (GRIND) NIL NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (HIDE -4) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (BDDSIMP) (("1" (INST 1 "floor((t!1 - timeout!1) / K)") (("1" (CASE "t!1>=timeout!1") (("1" (HIDE -3) (("1" (GRIND) (("1" (CASE "t!1-timeout!1>=0") (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" -1) (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "Timer_Lemma4") (("2" (INST -1 "P!1" "t!1" "t!1" "timeout!1") (("2" (BDDSIMP) (("1" (TYPEPRED "t!1") (("1" (PROPAX) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL) ("3" (ASSERT) NIL NIL) ("4" (ASSERT) NIL NIL) ("5" (CASE "t!1-timeout!1>= floor((t!1 - timeout!1) / K) * K") (("1" (ASSERT) NIL NIL) ("2" (HIDE 2 3 4) (("2" (HIDE -2) (("2" (GRIND) (("2" (NAME-REPLACE "y!1" "t!1-timeout!1") (("2" (GRIND) (("2" (BOTH-SIDES "/" "K" 1) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "Timer_Lemma4") (("2" (INST -1 "P!1" "t!1" "t!1" "timeout!1") (("2" (BDDSIMP) (("1" (TYPEPRED "t!1") (("1" (PROPAX) NIL NIL)) NIL) ("2" (ASSERT) (("2" (CASE "(t!1-timeout!1)/K>=0") (("1" (NAME-REPLACE "y!1" "(t!1-timeout!1)/K") (("1" (HIDE -4) (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" 1) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (HIDE -3) (("2" (GRIND) (("2" (CASE "t!1-timeout!1>=0") (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" -1) (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (ASSERT) NIL NIL) ("4" (ASSERT) NIL NIL) ("5" (CASE "t!1-timeout!1>=floor((t!1 - timeout!1) / K) * K") (("1" (ASSERT) NIL NIL) ("2" (HIDE 2 3) (("2" (BOTH-SIDES "/" "K" 1) (("2" (NAME-REPLACE "y!1" "(t!1 - timeout!1) / K") (("2" (HIDE -2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Timer_General| "" (INDUCT "t" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (SKOSIMP) (("2" (LEMMA "Timer_General1") (("2" (LEMMA "Timer_General2") (("2" (SKOSIMP) (("2" (INST -1 "P!1" "timeout!1" "t!1") (("2" (INST - "P!1" "timeout!1" "t!1") (("2" (TYPEPRED "t!1") (("2" (ASSERT) (("2" (HIDE -5) (("2" (CASE "(P!1(t!1) AND Timer(P!1, timeout!1)(pre(t!1)) >= timeout!1) IFF Held_For(P!1, timeout!1)(t!1)") (("1" (GRIND) NIL NIL) ("2" (HIDE 3) (("2" (BDDSIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|TimerGeneral_SRS_TCC1| "" (COND-DISJOINT-TCC) NIL NIL) (|TimerGeneral_SRS_TCC2| "" (COND-COVERAGE-TCC) NIL NIL) (SDD_TCC1 "" (TERMINATION-TCC) NIL NIL) (SDD_TCC2 "" (COND-DISJOINT-TCC) NIL NIL) (|Timer1_is_Timer| "" (INDUCT "t" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL) (|Timer2_lemma| "" (INDUCT "t" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (SKOLEM-TYPEPRED) (("2" (BDDSIMP) (("2" (SKOSIMP) (("2" (SKOSIMP) (("2" (INST -3 "P!1" "timeout1!1" "timeout2!1") (("2" (EXPAND "SDD" 2) (("2" (EXPAND "Timer" 2) (("2" (ASSERT) (("2" (LEMMA "Timer1_is_Timer") (("2" (INST - "P!1" "pre(t!1)" "timeout1!1" "timeout2!1") (("2" (REPLACE -1 * RL) (("2" (REPLACE -4 * RL) (("2" (LEMMA "Timer_General") (("2" (INST?) (("2" (LIFT-IF) (("2" (SPLIT) (("1" (FLATTEN) NIL NIL) ("2" (FLATTEN) (("2" (REPLACE -1 * RL) (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Final_lemma2| "" (LEMMA "Timer1_is_Timer") (("" (SKOLEM-TYPEPRED) (("" (INST?) (("" (REPLACE -7 * RL) (("" (LEMMA "Timer_General") (("" (INST?) (("" (LIFT-IF) (("" (SPLIT) (("1" (FLATTEN) NIL NIL) ("2" (FLATTEN) (("2" (REPLACE -1 *) (("2" (LEMMA "Timer2_lemma") (("2" (INST?) (("2" (REPLACE -1 * RL) (("2" (LEMMA "Timer_General") (("2" (INST -1 "LAMBDA (x: clock[K]): NOT Held_For(P!1, timeout1!1)(x)" "t!1" "timeout2!1") (("2" (LIFT-IF) (("2" (SPLIT) (("1" (FLATTEN) NIL NIL) ("2" (HIDE -2 -3) (("2" (FLATTEN) (("2" (BETA) (("2" (HIDE -2 -3 -4 -5 -6 -7 -8) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (GOAL "" (INDUCT "t" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (SKOSIMP) (("2" (SKOSIMP) (("2" (INST -1 "timeout1!1" "timeout2!1") (("2" (LEMMA "Final_lemma2") (("2" (INST -1 "PP" "timeout1!1" "timeout2!1" "t!1") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$Clocks.pvs Clocks[ K: posreal ]: THEORY BEGIN non_neg: TYPE = { x: real | x>=0 } CONTAINING 0 time: TYPE = non_neg t: VAR time n: VAR nat clock: TYPE = { t: time | EXISTS(n: nat): t=n*K } CONTAINING 0 x: VAR clock init(x): bool = (x=0) noninit_elem: TYPE ={ x | not init(x) } y: VAR noninit_elem pre(y): clock = y - K next(x): noninit_elem = x + K rank(x): nat = x/K %------------------ % induction rules %------------------ clock_induct : LEMMA FORALL (P : pred[clock]) : (FORALL x, n : rank(x) = n implies P(x)) implies (FORALL x : P(x)) % The general clock induction proposition clock_induction: PROPOSITION FORALL (P: pred[clock]): (FORALL (t: clock): init(t) IMPLIES P(t)) AND (FORALL (t: noninit_elem): P(pre(t)) IMPLIES P(t)) IMPLIES (FORALL (t: clock): P(t)) clock_strong_induction: PROPOSITION FORALL (P: pred[clock]): (FORALL (x:clock): (FORALL (z:clock): z < x IMPLIES P(z)) IMPLIES P(x)) IMPLIES (FORALL (t: clock): P(t)) END Clocks $$$Clocks.prf (|Clocks| (|clock_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|pre_TCC1| "" (SKOLEM-TYPEPRED) (("" (SKOLEM-TYPEPRED) (("" (SPLIT) (("1" (GRIND) (("1" (DELETE -3) (("1" (CASE "n!1>0") (("1" (ASSERT) (("1" (LEMMA "both_sides_times_pos_ge1") (("1" (INST -1 "K" "n!1-1" "0") (("1" (SIMPLIFY) (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (INST 1 "n!1-1") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "init") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|next_TCC1| "" (SKOLEM-TYPEPRED) (("" (SPLIT) (("1" (SKOLEM-TYPEPRED) (("1" (INST 1 "n!1+1") (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (SKOLEM-TYPEPRED) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) (|rank_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|clock_induct| "" (SKOSIMP) (("" (SKOLEM!) (("" (INST -1 "x!1" "rank(x!1)") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|clock_induction| "" (SKOSIMP) (("" (LEMMA "clock_induct" ("P" "P!1")) (("" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (DELETE 2) (("2" (INDUCT "n") (("1" (SKOSIMP) (("1" (INST -2 "x!1") (("1" (GRIND) (("1" (LEMMA "div_eq_zero" ("x" "x!1" "n0z" "K")) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (GROUND) (("2" (INST -1 "pre(x!1)") (("1" (INST -4 "x!1") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|clock_strong_induction| "" (LEMMA "clock_induction") (("" (SKOSIMP*) (("" (INST -1 "(LAMBDA (n:clock): (FORALL (m:clock): m <= n IMPLIES P!1(m)))") (("" (BETA) (("" (SPLIT) (("1" (INST -1 "t!1") (("1" (INST -1 "t!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST -3 0) (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (INST -3 "m!1") (("3" (ASSERT) (("3" (SKOSIMP) (("3" (INST -1 "z!1") (("3" (GRIND) (("3" (HIDE 2 3 4) (("3" (TYPEPRED "m!1" "z!1" "t!2" "K") (("3" (BOTH-SIDES "/" "K" -7) (("1" (BOTH-SIDES "/" "K" -9) (("1" (BOTH-SIDES "/" "K" -10) (("1" (BOTH-SIDES "/" "K" 2) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) (|Held_For| (|heldfor_TCC1| "" (TERMINATION-TCC) NIL NIL) (|le_inner_clockvar| "" (GRIND) (("" (CASE "floor(n!2)<=n!1") (("1" (GRIND) (("1" (CASE "floor(n!2)=n!2") (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" 1) (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL) ("2" (GRIND) (("2" (BOTH-SIDES "/" "K" -11) (("2" (GRIND) (("2" (BOTH-SIDES "/" "K" -9) (("2" (GRIND) (("2" (CASE "n!1 * K / K=n!1") (("1" (REPLACE -1 -10 LR) (("1" (CASE "n!2* K / K=n!2") (("1" (REPLACE -1 -13 LR) (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" -12) (("1" (CASE "(K + n!1 * K) / K=n!1+1") (("1" (REPLACE -1 -13 LR) (("1" (GRIND) NIL NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|ge_inner_clockvar| "" (GRIND) (("" (CASE "floor(n!2)>=n!1+1") (("1" (GRIND) (("1" (CASE "floor(n!2)=n!2") (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" 1) (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL) ("2" (GRIND) (("2" (BOTH-SIDES "/" "K" -11) (("2" (GRIND) (("2" (BOTH-SIDES "/" "K" -9) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) (|Held_For2|) (|DelayedTrip| (|TimerUpdate_TCC1| "" (COND-DISJOINT-TCC) NIL NIL) (|TimerUpdate_TCC2| "" (COND-COVERAGE-TCC) NIL NIL) (|TimerUpdate_TCC3| "" (SKOSIMP) (("" (INST 2 "0") (("" (GRIND) NIL NIL)) NIL)) NIL) (|TimerUpdate_TCC4| "" (COND-COVERAGE-TCC) NIL NIL) (|TimerUpdate_TCC5| "" (COND-DISJOINT-TCC) NIL NIL) (|Timer_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|Timer_TCC2| "" (TERMINATION-TCC) NIL NIL) (|Timer_TCC3| "" (COND-DISJOINT-TCC) NIL NIL) (|Timer_Lemma2| "" (INDUCT "t" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL) (|Timer_Lemma3| "" (INDUCT "t" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL) (|Timer_Lemma4| "" (INDUCT "t" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (SKOSIMP) (("2" (SKOSIMP) (("2" (INST -1 "P!1" "t_h!1" "timeout!1") (("2" (BDDSIMP) (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL) ("3" (ASSERT) (("3" (EXPAND "Timer" -4) (("3" (GRIND) NIL NIL)) NIL)) NIL) ("4" (CASE "timeout!1 - (t_h!1 - t!1)>0 OR timeout!1 - (t_h!1 - t!1)<=0") (("1" (BDDSIMP) (("1" (LEMMA "Timer_Lemma2") (("1" (INST -1 "P!1" "pre(t!1)" "timeout!1") (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (HIDE -5) (("2" (GRIND) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL) ("5" (GRIND) NIL NIL) ("6" (CASE "t!1<=t_h!1-timeout!1 OR t!1>t_h!1-timeout!1") (("1" (BDDSIMP) (("1" (HIDE -5) (("1" (GRIND) NIL NIL)) NIL) ("2" (CASE "t!1>floor((t_h!1 - timeout!1) / K) * K") (("1" (HIDE -6) (("1" (GRIND) (("1" (HIDE -2 -3 -4 -5) (("1" (HIDE 2 3) (("1" (GRIND) (("1" (TYPEPRED "t!1") (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" -4) (("1" (BOTH-SIDES "/" "K" 2) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (CASE "t_h!1 - timeout!1>floor((t_h!1 - timeout!1) / K) * K") (("1" (HIDE -6) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -1 -2 -3 -4 -5) (("2" (HIDE 2 3 4 5) (("2" (BOTH-SIDES "/" "K" 1) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Timer_General1| "" (SKOSIMP) (("" (EXPAND "Held_For_New") (("" (SKOSIMP) (("" (CASE "FORALL (t: clock[K] | NOT init(t)& t >= t_j!1 & t <= t!1 ):Timer(P!1,timeout!1)(pre(t))>=timeout!1-(t!1-t) AND P!1(t)") (("1" (INST -1 "t!1") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL) ("2" (BDDSIMP) (("1" (HIDE 1) (("1" (REVEAL 1) (("1" (HIDE 2) (("1" (INDUCT "t" 1 "clock_induction") (("1" (TYPEPRED "t!2") (("1" (PROPAX) NIL NIL)) NIL) ("2" (TYPEPRED "t!2") (("2" (PROPAX) NIL NIL)) NIL) ("3" (GRIND) NIL NIL) ("4" (GRIND) NIL NIL) ("5" (GRIND) NIL NIL) ("6" (GRIND) NIL NIL) ("7" (GRIND) NIL NIL) ("8" (SKOSIMP) (("8" (BDDSIMP) (("1" (INST -5 "t!2") (("1" (GRIND) NIL NIL)) NIL) ("2" (EXPAND "init") (("2" (REPLACE -1 * LR) (("2" (EXPAND "pre") (("2" (CASE "t!2>t_j!1 OR t!2=t_j!1") (("1" (BDDSIMP) (("1" (CASE "t_j!1=0") (("1" (GRIND) NIL NIL) ("2" (ASSERT) (("2" (SIMPLIFY) (("2" (HIDE 3) (("2" (GRIND) (("2" (TYPEPRED "t_j!1") (("2" (GRIND) (("2" (CASE "K>n!1*K") (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" -1) (("1" (BOTH-SIDES "/" "K" 1) (("1" (GRIND) NIL NIL)) NIL) ("2" (GRIND) (("2" (BOTH-SIDES "*" "K" 1) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "timeout!1 - (t!1 - t!2)<=0") (("1" (GRIND) NIL NIL) ("2" (HIDE 3) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (INST -6 "t!2") (("3" (GRIND) NIL NIL)) NIL) ("4" (CASE "NOT init(pre(t!2))") (("1" (GRIND) NIL NIL) ("2" (EXPAND "Timer" 2) (("2" (ASSERT) (("2" (EXPAND "TimerUpdate") (("2" (ASSERT) (("2" (EXPAND "init") (("2" (EXPAND "pre") (("2" (EXPAND "next") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("5" (INST -4 "t!2") (("5" (GRIND) NIL NIL)) NIL) ("6" (HIDE 3) (("6" (GRIND) NIL NIL)) NIL) ("7" (INST -4 "t!2") (("7" (GRIND) NIL NIL)) NIL) ("8" (CASE "t!2=t_j!1 OR t!2>t_j!1") (("1" (BDDSIMP) (("1" (REPLACE -1 * LR) (("1" (CASE "timeout!1 - (t!1 - t_j!1)<=0") (("1" (GRIND) NIL NIL) ("2" (HIDE 4) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE 3) (("2" (GRIND) (("2" (TYPEPRED "t!2") (("2" (TYPEPRED "t_j!1") (("2" (GRIND) (("2" (BOTH-SIDES "/" "K" 2) (("2" (BOTH-SIDES "/" "K" -7) (("2" (BOTH-SIDES "/" "K" -8) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 4) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Timer_General2| "" (SKOLEM!) (("" (BDDSIMP) (("" (EXPAND "Held_For_New") (("" (INST 1 "floor((t!1-timeout!1)/K)*K") (("1" (CASE "FORALL (t_h: clock[K] | t_h >= floor((t!1 - timeout!1) / K) * K & t_h <= t!1 & NOT init(t_h)): P!1(t_h) AND Timer(P!1,timeout!1)(pre(t_h))>=timeout!1-(t!1-t_h) IMPLIES FORALL (t: clock[K] | t >= floor((t!1 - timeout!1) / K) * K & t <= t_h): P!1(t)") (("1" (INST -1 "t!1") (("1" (BDDSIMP) (("1" (CASE "t!1-timeout!1>=floor((t!1 - timeout!1) / K) * K") (("1" (GRIND) NIL NIL) ("2" (HIDE 2) (("2" (NAME-REPLACE "y!1" "t!1-timeout!1") (("2" (HIDE -2 -3) (("2" (GRIND) (("2" (BOTH-SIDES "/" "K") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL) ("2" (HIDE 2) (("2" (CASE "t!1-timeout!1>=floor((t!1 - timeout!1) / K) * K") (("1" (GRIND) NIL NIL) ("2" (HIDE -2 -1) (("2" (GRIND) (("2" (HIDE 2) (("2" (BOTH-SIDES "/" "K") (("2" (NAME-REPLACE "y!1" "(t!1 - timeout!1) / K") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (HIDE -2) (("2" (INDUCT "t_h" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL) ("3" (GRIND) NIL NIL) ("4" (SKOSIMP) NIL NIL) ("5" (SKOSIMP) (("5" (BDDSIMP) (("1" (CASE "t!2=K") (("1" (REPLACE -1 * LR) (("1" (REPLACE -1 * RL) (("1" (REPLACE -1 * LR) (("1" (CASE "timeout!1 - (t!1 - K)<=0 OR timeout!1 - (t!1 - K)>0") (("1" (BDDSIMP) (("1" (CASE "floor((t!1 - timeout!1) / K) * K>=K") (("1" (SKOSIMP) (("1" (TYPEPRED "t!3") (("1" (CASE "t!3>=K") (("1" (HIDE -13) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -12) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -7) (("2" (CASE "t!1-timeout!1>=K") (("1" (HIDE 2 3) (("1" (NAME-REPLACE "y!1" "t!1-timeout!1") (("1" (GRIND) (("1" (BOTH-SIDES "/" "K") (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" -1) (("1" (NAME-REPLACE "z!1" "y!1/K") (("1" (GRIND) NIL NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (BOTH-SIDES "*" "K" -1) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (CASE "t!3=K or t!3=0") (("1" (BDDSIMP) (("1" (ASSERT) NIL NIL) ("2" (ASSERT) (("2" (GRIND) NIL NIL)) NIL)) NIL) ("2" (TYPEPRED "t!3") (("2" (BDDSIMP) (("2" (CASE "t!3pre(t!2)") (("1" (BDDSIMP) (("1" (INST -2 "t!3") NIL NIL) ("2" (ASSERT) (("2" (TYPEPRED "t!3") (("2" (CASE "t!3=t!2") (("1" (GRIND) NIL NIL) ("2" (TYPEPRED "t!2") (("2" (GRIND) (("2" (HIDE -1 -2 -3 -4 -5 -6) (("2" (CASE "n!2<=n!1") (("1" (CASE "n!2>n!1-1") (("1" (GRIND) NIL NIL) ("2" (BOTH-SIDES "*" "K" 1) (("2" (GRIND) NIL NIL)) NIL)) NIL) ("2" (BOTH-SIDES "*" "K" 1) (("2" (ASSERT) (("2" (GRIND) (("2" (BOTH-SIDES "/" "K" -1) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("3" (CASE "timeout!1 - (t!1 - t!2)=0 OR timeout!1 - (t!1 - t!2)>0 OR timeout!1 - (t!1 - t!2)<0") (("1" (BDDSIMP) (("1" (CASE "t!2=t!1-timeout!1") (("1" (REPLACE -1 * LR) (("1" (REPLACE -1 * RL) (("1" (REPLACE -1 * LR) (("1" (REPLACE -1 * RL) (("1" (ASSERT) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL) ("2" (LEMMA "Timer_Lemma2") (("2" (INST -1 "P!1" "pre(t!2)" "timeout!1") (("2" (BDDSIMP) (("1" (EXPAND "Timer" -6) (("1" (GRIND) NIL NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("3" (HIDE -5 -6 1 2) (("3" (CASE "t!2 floor((t!1 - timeout!1) / K) * K OR t!2 = floor((t!1 - timeout!1) / K) * K") (("1" (BDDSIMP) (("1" (HIDE -2) (("1" (GRIND) NIL NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL) ("4" (CASE "timeout!1 - (t!1 - t!2)=0 OR timeout!1 - (t!1 - t!2)<0 OR timeout!1 - (t!1 - t!2)>0") (("1" (BDDSIMP) (("1" (CASE "t!2=t!1-timeout!1") (("1" (REPLACE -1 * LR) (("1" (REPLACE -1 * RL) (("1" (HIDE -6) (("1" (CASE "floor((t!1 - timeout!1) / K) * K=t!2") (("1" (GRIND) NIL NIL) ("2" (CASE "floor((t!1 - timeout!1) / K) * K=floor((t!2)/K)*K") (("1" (CASE "t!2=floor((t!2) / K) * K") (("1" (GRIND) NIL NIL) ("2" (ASSERT) (("2" (HIDE 2 3 4 5) (("2" (TYPEPRED "t!2") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL) ("2" (CASE "t!2 floor((t!1 - timeout!1) / K) * K OR t!2 = floor((t!1 - timeout!1) / K) * K") (("1" (BDDSIMP) (("1" (HIDE -5) (("1" (HIDE 2 3) (("1" (TYPEPRED "t!2") (("1" (GRIND) (("1" (CASE "n!1>=floor((t!1 - timeout!1) / K)+1") (("1" (ASSERT) (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" 2) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2 3) (("2" (HIDE -5 -6) (("2" (BOTH-SIDES "/" "K" -4) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -5) (("2" (GRIND) NIL NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (HIDE -4) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (BDDSIMP) (("1" (INST 1 "floor((t!1 - timeout!1) / K)") (("1" (CASE "t!1>=timeout!1") (("1" (HIDE -3) (("1" (GRIND) (("1" (CASE "t!1-timeout!1>=0") (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" -1) (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "Timer_Lemma4") (("2" (INST -1 "P!1" "t!1" "t!1" "timeout!1") (("2" (BDDSIMP) (("1" (TYPEPRED "t!1") (("1" (PROPAX) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL) ("3" (ASSERT) NIL NIL) ("4" (ASSERT) NIL NIL) ("5" (CASE "t!1-timeout!1>= floor((t!1 - timeout!1) / K) * K") (("1" (ASSERT) NIL NIL) ("2" (HIDE 2 3 4) (("2" (HIDE -2) (("2" (GRIND) (("2" (NAME-REPLACE "y!1" "t!1-timeout!1") (("2" (GRIND) (("2" (BOTH-SIDES "/" "K" 1) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "Timer_Lemma4") (("2" (INST -1 "P!1" "t!1" "t!1" "timeout!1") (("2" (BDDSIMP) (("1" (TYPEPRED "t!1") (("1" (PROPAX) NIL NIL)) NIL) ("2" (ASSERT) (("2" (CASE "(t!1-timeout!1)/K>=0") (("1" (NAME-REPLACE "y!1" "(t!1-timeout!1)/K") (("1" (HIDE -4) (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" 1) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (HIDE -3) (("2" (GRIND) (("2" (CASE "t!1-timeout!1>=0") (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" -1) (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (ASSERT) NIL NIL) ("4" (ASSERT) NIL NIL) ("5" (CASE "t!1-timeout!1>=floor((t!1 - timeout!1) / K) * K") (("1" (ASSERT) NIL NIL) ("2" (HIDE 2 3) (("2" (BOTH-SIDES "/" "K" 1) (("2" (NAME-REPLACE "y!1" "(t!1 - timeout!1) / K") (("2" (HIDE -2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Timer_General| "" (INDUCT "t" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (SKOSIMP) (("2" (LEMMA "Timer_General1") (("2" (LEMMA "Timer_General2") (("2" (SKOSIMP) (("2" (INST -1 "P!1" "timeout!1" "t!1") (("2" (INST - "P!1" "timeout!1" "t!1") (("2" (TYPEPRED "t!1") (("2" (ASSERT) (("2" (HIDE -5) (("2" (CASE "(P!1(t!1) AND Timer(P!1, timeout!1)(pre(t!1)) >= timeout!1) IFF Held_For_New(P!1, timeout!1)(t!1)") (("1" (GRIND) NIL NIL) ("2" (HIDE 3) (("2" (BDDSIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|DelayedTrip_SRS_TCC1| "" (COND-DISJOINT-TCC) NIL NIL) (|DelayedTrip_SRS_TCC2| "" (COND-COVERAGE-TCC) NIL NIL) (SDD_TCC1 "" (TERMINATION-TCC) NIL NIL) (SDD_TCC2 "" (COND-DISJOINT-TCC) NIL NIL) (|Timer1_is_Timer| "" (INDUCT "t" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL) (|Timer2_lemma| "" (INDUCT "t" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (SKOLEM-TYPEPRED) (("2" (BDDSIMP) (("2" (SKOSIMP) (("2" (SKOSIMP) (("2" (INST -3 "P!1" "timeout1!1" "timeout2!1") (("2" (EXPAND "SDD" 2) (("2" (EXPAND "Timer" 2) (("2" (ASSERT) (("2" (LEMMA "Timer1_is_Timer") (("2" (INST - "P!1" "pre(t!1)" "timeout1!1" "timeout2!1") (("2" (REPLACE -1 * RL) (("2" (REPLACE -4 * RL) (("2" (LEMMA "Timer_General") (("2" (INST?) (("2" (LIFT-IF) (("2" (SPLIT) (("1" (FLATTEN) NIL NIL) ("2" (FLATTEN) (("2" (REPLACE -1 * RL) (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Final_lemma2| "" (LEMMA "Timer1_is_Timer") (("" (SKOLEM-TYPEPRED) (("" (INST?) (("" (REPLACE -7 * RL) (("" (LEMMA "Timer_General") (("" (INST?) (("" (LIFT-IF) (("" (SPLIT) (("1" (FLATTEN) NIL NIL) ("2" (FLATTEN) (("2" (REPLACE -1 *) (("2" (LEMMA "Timer2_lemma") (("2" (INST?) (("2" (REPLACE -1 * RL) (("2" (LEMMA "Timer_General") (("2" (INST -1 "LAMBDA (x: clock[K]): NOT Held_For_New(P!1, timeout1!1)(x)" "t!1" "timeout2!1") (("2" (LIFT-IF) (("2" (SPLIT) (("1" (FLATTEN) NIL NIL) ("2" (HIDE -2 -3) (("2" (FLATTEN) (("2" (BETA) (("2" (HIDE -2 -3 -4 -5 -6 -7 -8) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (GOAL "" (INDUCT "t" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (SKOSIMP) (("2" (SKOSIMP) (("2" (INST -1 "timeout1!1" "timeout2!1") (("2" (LEMMA "Final_lemma2") (("2" (INST -1 "PP" "timeout1!1" "timeout2!1" "t!1") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$Held_For.pvs Held_For_Rec [K:posreal] : THEORY BEGIN IMPORTING Clocks[K] t, t_now: VAR clock duration:VAR time P: VAR pred[clock] heldfor(P, t, t_now, duration): RECURSIVE bool = IF P(t) THEN IF (t_now - t >= duration) THEN TRUE ELSIF init(t) THEN FALSE ELSE heldfor(P,pre(t),t_now,duration) ENDIF ELSE FALSE ENDIF MEASURE rank(t) Held_For_Rec(P, duration): pred[clock] = (LAMBDA (t:clock): heldfor(P,t,t,duration)) t1,t2:VAR clock le_inner_clockvar: lemma forall (x:{y: posreal|(t1 t2<=t1 ge_inner_clockvar: lemma forall (x:{y: posreal|(t1=x => t2>=t1+K END Held_For_Rec Held_For [K:posreal] : THEORY BEGIN IMPORTING Clocks[K] t, t_now,t_n,t_j: VAR clock duration:VAR time P: VAR pred[clock] Held_For(P, duration): pred[clock]= (LAMBDA (t_n):EXISTS(t_j):(t_n-t_j>=duration) and FORALL(t:clock|t>=t_j&t<=t_n):P(t)) END Held_For $$$Held_For.prf (|Clocks| (|clock_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|pre_TCC1| "" (SKOLEM-TYPEPRED) (("" (SKOLEM-TYPEPRED) (("" (SPLIT) (("1" (GRIND) (("1" (DELETE -3) (("1" (CASE "n!1>0") (("1" (ASSERT) (("1" (LEMMA "both_sides_times_pos_ge1") (("1" (INST -1 "K" "n!1-1" "0") (("1" (SIMPLIFY) (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (INST 1 "n!1-1") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "init") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|next_TCC1| "" (SKOLEM-TYPEPRED) (("" (SPLIT) (("1" (SKOLEM-TYPEPRED) (("1" (INST 1 "n!1+1") (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (SKOLEM-TYPEPRED) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) (|rank_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|clock_induct| "" (SKOSIMP) (("" (SKOLEM!) (("" (INST -1 "x!1" "rank(x!1)") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|clock_induction| "" (SKOSIMP) (("" (LEMMA "clock_induct" ("P" "P!1")) (("" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (DELETE 2) (("2" (INDUCT "n") (("1" (SKOSIMP) (("1" (INST -2 "x!1") (("1" (GRIND) (("1" (LEMMA "div_eq_zero" ("x" "x!1" "n0z" "K")) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (GROUND) (("2" (INST -1 "pre(x!1)") (("1" (INST -4 "x!1") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|clock_strong_induction| "" (LEMMA "clock_induction") (("" (SKOSIMP*) (("" (INST -1 "(LAMBDA (n:clock): (FORALL (m:clock): m <= n IMPLIES P!1(m)))") (("" (BETA) (("" (SPLIT) (("1" (INST -1 "t!1") (("1" (INST -1 "t!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST -3 0) (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL) ("3" (SKOSIMP*) (("3" (INST -3 "m!1") (("3" (ASSERT) (("3" (SKOSIMP) (("3" (INST -1 "z!1") (("3" (GRIND) (("3" (HIDE 2 3 4) (("3" (TYPEPRED "m!1" "z!1" "t!2" "K") (("3" (BOTH-SIDES "/" "K" -7) (("1" (BOTH-SIDES "/" "K" -9) (("1" (BOTH-SIDES "/" "K" -10) (("1" (BOTH-SIDES "/" "K" 2) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) (|Held_For_Rec| (|heldfor_TCC1| "" (TERMINATION-TCC) NIL NIL) (|le_inner_clockvar| "" (GRIND) (("" (CASE "floor(n!2)<=n!1") (("1" (GRIND) (("1" (CASE "floor(n!2)=n!2") (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" 1) (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL) ("2" (GRIND) (("2" (BOTH-SIDES "/" "K" -11) (("2" (GRIND) (("2" (BOTH-SIDES "/" "K" -9) (("2" (GRIND) (("2" (CASE "n!1 * K / K=n!1") (("1" (REPLACE -1 -10 LR) (("1" (CASE "n!2* K / K=n!2") (("1" (REPLACE -1 -13 LR) (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" -12) (("1" (CASE "(K + n!1 * K) / K=n!1+1") (("1" (REPLACE -1 -13 LR) (("1" (GRIND) NIL NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|ge_inner_clockvar| "" (GRIND) (("" (CASE "floor(n!2)>=n!1+1") (("1" (GRIND) (("1" (CASE "floor(n!2)=n!2") (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" 1) (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL) ("2" (GRIND) (("2" (BOTH-SIDES "/" "K" -11) (("2" (GRIND) (("2" (BOTH-SIDES "/" "K" -9) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) (|Held_For|) (|DelayedTrip| (|TimerUpdate_TCC1| "" (COND-DISJOINT-TCC) NIL NIL) (|TimerUpdate_TCC2| "" (COND-COVERAGE-TCC) NIL NIL) (|TimerUpdate_TCC3| "" (SKOSIMP) (("" (INST 2 "0") (("" (GRIND) NIL NIL)) NIL)) NIL) (|TimerUpdate_TCC4| "" (COND-COVERAGE-TCC) NIL NIL) (|TimerUpdate_TCC5| "" (COND-DISJOINT-TCC) NIL NIL) (|Timer_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|Timer_TCC2| "" (TERMINATION-TCC) NIL NIL) (|Timer_TCC3| "" (COND-DISJOINT-TCC) NIL NIL) (|Timer_Lemma2| "" (INDUCT "t" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL) (|Timer_Lemma3| "" (INDUCT "t" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL) (|Timer_Lemma4| "" (INDUCT "t" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (SKOSIMP) (("2" (SKOSIMP) (("2" (INST -1 "P!1" "t_h!1" "timeout!1") (("2" (BDDSIMP) (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL) ("3" (ASSERT) (("3" (EXPAND "Timer" -4) (("3" (GRIND) NIL NIL)) NIL)) NIL) ("4" (CASE "timeout!1 - (t_h!1 - t!1)>0 OR timeout!1 - (t_h!1 - t!1)<=0") (("1" (BDDSIMP) (("1" (LEMMA "Timer_Lemma2") (("1" (INST -1 "P!1" "pre(t!1)" "timeout!1") (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (HIDE -5) (("2" (GRIND) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL) ("5" (GRIND) NIL NIL) ("6" (CASE "t!1<=t_h!1-timeout!1 OR t!1>t_h!1-timeout!1") (("1" (BDDSIMP) (("1" (HIDE -5) (("1" (GRIND) NIL NIL)) NIL) ("2" (CASE "t!1>floor((t_h!1 - timeout!1) / K) * K") (("1" (HIDE -6) (("1" (GRIND) (("1" (HIDE -2 -3 -4 -5) (("1" (HIDE 2 3) (("1" (GRIND) (("1" (TYPEPRED "t!1") (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" -4) (("1" (BOTH-SIDES "/" "K" 2) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (CASE "t_h!1 - timeout!1>floor((t_h!1 - timeout!1) / K) * K") (("1" (HIDE -6) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -1 -2 -3 -4 -5) (("2" (HIDE 2 3 4 5) (("2" (BOTH-SIDES "/" "K" 1) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Timer_General1| "" (SKOSIMP) (("" (EXPAND "Held_For") (("" (SKOSIMP) (("" (CASE "FORALL (t: clock[K] | NOT init(t)& t >= t_j!1 & t <= t!1 ):Timer(P!1,timeout!1)(pre(t))>=timeout!1-(t!1-t) AND P!1(t)") (("1" (INST -1 "t!1") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL) ("2" (BDDSIMP) (("1" (HIDE 1) (("1" (REVEAL 1) (("1" (HIDE 2) (("1" (INDUCT "t" 1 "clock_induction") (("1" (TYPEPRED "t!2") (("1" (PROPAX) NIL NIL)) NIL) ("2" (TYPEPRED "t!2") (("2" (PROPAX) NIL NIL)) NIL) ("3" (GRIND) NIL NIL) ("4" (GRIND) NIL NIL) ("5" (GRIND) NIL NIL) ("6" (GRIND) NIL NIL) ("7" (GRIND) NIL NIL) ("8" (SKOSIMP) (("8" (BDDSIMP) (("1" (INST -5 "t!2") (("1" (GRIND) NIL NIL)) NIL) ("2" (EXPAND "init") (("2" (REPLACE -1 * LR) (("2" (EXPAND "pre") (("2" (CASE "t!2>t_j!1 OR t!2=t_j!1") (("1" (BDDSIMP) (("1" (CASE "t_j!1=0") (("1" (GRIND) NIL NIL) ("2" (ASSERT) (("2" (SIMPLIFY) (("2" (HIDE 3) (("2" (GRIND) (("2" (TYPEPRED "t_j!1") (("2" (GRIND) (("2" (CASE "K>n!1*K") (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" -1) (("1" (BOTH-SIDES "/" "K" 1) (("1" (GRIND) NIL NIL)) NIL) ("2" (GRIND) (("2" (BOTH-SIDES "*" "K" 1) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "timeout!1 - (t!1 - t!2)<=0") (("1" (GRIND) NIL NIL) ("2" (HIDE 3) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (INST -6 "t!2") (("3" (GRIND) NIL NIL)) NIL) ("4" (CASE "NOT init(pre(t!2))") (("1" (GRIND) NIL NIL) ("2" (EXPAND "Timer" 2) (("2" (ASSERT) (("2" (EXPAND "TimerUpdate") (("2" (ASSERT) (("2" (EXPAND "init") (("2" (EXPAND "pre") (("2" (EXPAND "next") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("5" (INST -4 "t!2") (("5" (GRIND) NIL NIL)) NIL) ("6" (HIDE 3) (("6" (GRIND) NIL NIL)) NIL) ("7" (INST -4 "t!2") (("7" (GRIND) NIL NIL)) NIL) ("8" (CASE "t!2=t_j!1 OR t!2>t_j!1") (("1" (BDDSIMP) (("1" (REPLACE -1 * LR) (("1" (CASE "timeout!1 - (t!1 - t_j!1)<=0") (("1" (GRIND) NIL NIL) ("2" (HIDE 4) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE 3) (("2" (GRIND) (("2" (TYPEPRED "t!2") (("2" (TYPEPRED "t_j!1") (("2" (GRIND) (("2" (BOTH-SIDES "/" "K" 2) (("2" (BOTH-SIDES "/" "K" -7) (("2" (BOTH-SIDES "/" "K" -8) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 4) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Timer_General2| "" (SKOLEM!) (("" (BDDSIMP) (("" (EXPAND "Held_For") (("" (INST 1 "floor((t!1-timeout!1)/K)*K") (("1" (CASE "FORALL (t_h: clock[K] | t_h >= floor((t!1 - timeout!1) / K) * K & t_h <= t!1 & NOT init(t_h)): P!1(t_h) AND Timer(P!1,timeout!1)(pre(t_h))>=timeout!1-(t!1-t_h) IMPLIES FORALL (t: clock[K] | t >= floor((t!1 - timeout!1) / K) * K & t <= t_h): P!1(t)") (("1" (INST -1 "t!1") (("1" (BDDSIMP) (("1" (CASE "t!1-timeout!1>=floor((t!1 - timeout!1) / K) * K") (("1" (GRIND) NIL NIL) ("2" (HIDE 2) (("2" (NAME-REPLACE "y!1" "t!1-timeout!1") (("2" (HIDE -2 -3) (("2" (GRIND) (("2" (BOTH-SIDES "/" "K") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL) ("2" (HIDE 2) (("2" (CASE "t!1-timeout!1>=floor((t!1 - timeout!1) / K) * K") (("1" (GRIND) NIL NIL) ("2" (HIDE -2 -1) (("2" (GRIND) (("2" (HIDE 2) (("2" (BOTH-SIDES "/" "K") (("2" (NAME-REPLACE "y!1" "(t!1 - timeout!1) / K") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (HIDE -2) (("2" (INDUCT "t_h" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL) ("3" (GRIND) NIL NIL) ("4" (SKOSIMP) NIL NIL) ("5" (SKOSIMP) (("5" (BDDSIMP) (("1" (CASE "t!2=K") (("1" (REPLACE -1 * LR) (("1" (REPLACE -1 * RL) (("1" (REPLACE -1 * LR) (("1" (CASE "timeout!1 - (t!1 - K)<=0 OR timeout!1 - (t!1 - K)>0") (("1" (BDDSIMP) (("1" (CASE "floor((t!1 - timeout!1) / K) * K>=K") (("1" (SKOSIMP) (("1" (TYPEPRED "t!3") (("1" (CASE "t!3>=K") (("1" (HIDE -13) (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -12) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -7) (("2" (CASE "t!1-timeout!1>=K") (("1" (HIDE 2 3) (("1" (NAME-REPLACE "y!1" "t!1-timeout!1") (("1" (GRIND) (("1" (BOTH-SIDES "/" "K") (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" -1) (("1" (NAME-REPLACE "z!1" "y!1/K") (("1" (GRIND) NIL NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (BOTH-SIDES "*" "K" -1) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (CASE "t!3=K or t!3=0") (("1" (BDDSIMP) (("1" (ASSERT) NIL NIL) ("2" (ASSERT) (("2" (GRIND) NIL NIL)) NIL)) NIL) ("2" (TYPEPRED "t!3") (("2" (BDDSIMP) (("2" (CASE "t!3pre(t!2)") (("1" (BDDSIMP) (("1" (INST -2 "t!3") NIL NIL) ("2" (ASSERT) (("2" (TYPEPRED "t!3") (("2" (CASE "t!3=t!2") (("1" (GRIND) NIL NIL) ("2" (TYPEPRED "t!2") (("2" (GRIND) (("2" (HIDE -1 -2 -3 -4 -5 -6) (("2" (CASE "n!2<=n!1") (("1" (CASE "n!2>n!1-1") (("1" (GRIND) NIL NIL) ("2" (BOTH-SIDES "*" "K" 1) (("2" (GRIND) NIL NIL)) NIL)) NIL) ("2" (BOTH-SIDES "*" "K" 1) (("2" (ASSERT) (("2" (GRIND) (("2" (BOTH-SIDES "/" "K" -1) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("3" (CASE "timeout!1 - (t!1 - t!2)=0 OR timeout!1 - (t!1 - t!2)>0 OR timeout!1 - (t!1 - t!2)<0") (("1" (BDDSIMP) (("1" (CASE "t!2=t!1-timeout!1") (("1" (REPLACE -1 * LR) (("1" (REPLACE -1 * RL) (("1" (REPLACE -1 * LR) (("1" (REPLACE -1 * RL) (("1" (ASSERT) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL) ("2" (LEMMA "Timer_Lemma2") (("2" (INST -1 "P!1" "pre(t!2)" "timeout!1") (("2" (BDDSIMP) (("1" (EXPAND "Timer" -6) (("1" (GRIND) NIL NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("3" (HIDE -5 -6 1 2) (("3" (CASE "t!2 floor((t!1 - timeout!1) / K) * K OR t!2 = floor((t!1 - timeout!1) / K) * K") (("1" (BDDSIMP) (("1" (HIDE -2) (("1" (GRIND) NIL NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL) ("4" (CASE "timeout!1 - (t!1 - t!2)=0 OR timeout!1 - (t!1 - t!2)<0 OR timeout!1 - (t!1 - t!2)>0") (("1" (BDDSIMP) (("1" (CASE "t!2=t!1-timeout!1") (("1" (REPLACE -1 * LR) (("1" (REPLACE -1 * RL) (("1" (HIDE -6) (("1" (CASE "floor((t!1 - timeout!1) / K) * K=t!2") (("1" (GRIND) NIL NIL) ("2" (CASE "floor((t!1 - timeout!1) / K) * K=floor((t!2)/K)*K") (("1" (CASE "t!2=floor((t!2) / K) * K") (("1" (GRIND) NIL NIL) ("2" (ASSERT) (("2" (HIDE 2 3 4 5) (("2" (TYPEPRED "t!2") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL) ("2" (CASE "t!2 floor((t!1 - timeout!1) / K) * K OR t!2 = floor((t!1 - timeout!1) / K) * K") (("1" (BDDSIMP) (("1" (HIDE -5) (("1" (HIDE 2 3) (("1" (TYPEPRED "t!2") (("1" (GRIND) (("1" (CASE "n!1>=floor((t!1 - timeout!1) / K)+1") (("1" (ASSERT) (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" 2) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2 3) (("2" (HIDE -5 -6) (("2" (BOTH-SIDES "/" "K" -4) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -5) (("2" (GRIND) NIL NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (HIDE -4) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (BDDSIMP) (("1" (INST 1 "floor((t!1 - timeout!1) / K)") (("1" (CASE "t!1>=timeout!1") (("1" (HIDE -3) (("1" (GRIND) (("1" (CASE "t!1-timeout!1>=0") (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" -1) (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "Timer_Lemma4") (("2" (INST -1 "P!1" "t!1" "t!1" "timeout!1") (("2" (BDDSIMP) (("1" (TYPEPRED "t!1") (("1" (PROPAX) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL) ("3" (ASSERT) NIL NIL) ("4" (ASSERT) NIL NIL) ("5" (CASE "t!1-timeout!1>= floor((t!1 - timeout!1) / K) * K") (("1" (ASSERT) NIL NIL) ("2" (HIDE 2 3 4) (("2" (HIDE -2) (("2" (GRIND) (("2" (NAME-REPLACE "y!1" "t!1-timeout!1") (("2" (GRIND) (("2" (BOTH-SIDES "/" "K" 1) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "Timer_Lemma4") (("2" (INST -1 "P!1" "t!1" "t!1" "timeout!1") (("2" (BDDSIMP) (("1" (TYPEPRED "t!1") (("1" (PROPAX) NIL NIL)) NIL) ("2" (ASSERT) (("2" (CASE "(t!1-timeout!1)/K>=0") (("1" (NAME-REPLACE "y!1" "(t!1-timeout!1)/K") (("1" (HIDE -4) (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" 1) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (HIDE -3) (("2" (GRIND) (("2" (CASE "t!1-timeout!1>=0") (("1" (GRIND) (("1" (BOTH-SIDES "/" "K" -1) (("1" (GRIND) NIL NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (ASSERT) NIL NIL) ("4" (ASSERT) NIL NIL) ("5" (CASE "t!1-timeout!1>=floor((t!1 - timeout!1) / K) * K") (("1" (ASSERT) NIL NIL) ("2" (HIDE 2 3) (("2" (BOTH-SIDES "/" "K" 1) (("2" (NAME-REPLACE "y!1" "(t!1 - timeout!1) / K") (("2" (HIDE -2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Timer_General| "" (INDUCT "t" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (SKOSIMP) (("2" (LEMMA "Timer_General1") (("2" (LEMMA "Timer_General2") (("2" (SKOSIMP) (("2" (INST -1 "P!1" "timeout!1" "t!1") (("2" (INST - "P!1" "timeout!1" "t!1") (("2" (TYPEPRED "t!1") (("2" (ASSERT) (("2" (HIDE -5) (("2" (CASE "(P!1(t!1) AND Timer(P!1, timeout!1)(pre(t!1)) >= timeout!1) IFF Held_For(P!1, timeout!1)(t!1)") (("1" (GRIND) NIL NIL) ("2" (HIDE 3) (("2" (BDDSIMP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|DelayedTrip_SRS_TCC1| "" (COND-DISJOINT-TCC) NIL NIL) (|DelayedTrip_SRS_TCC2| "" (COND-COVERAGE-TCC) NIL NIL) (SDD_TCC1 "" (TERMINATION-TCC) NIL NIL) (SDD_TCC2 "" (COND-DISJOINT-TCC) NIL NIL) (|Timer1_is_Timer| "" (INDUCT "t" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL) (|Timer2_lemma| "" (INDUCT "t" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (SKOLEM-TYPEPRED) (("2" (BDDSIMP) (("2" (SKOSIMP) (("2" (SKOSIMP) (("2" (INST -3 "P!1" "timeout1!1" "timeout2!1") (("2" (EXPAND "SDD" 2) (("2" (EXPAND "Timer" 2) (("2" (ASSERT) (("2" (LEMMA "Timer1_is_Timer") (("2" (INST - "P!1" "pre(t!1)" "timeout1!1" "timeout2!1") (("2" (REPLACE -1 * RL) (("2" (REPLACE -4 * RL) (("2" (LEMMA "Timer_General") (("2" (INST?) (("2" (LIFT-IF) (("2" (SPLIT) (("1" (FLATTEN) NIL NIL) ("2" (FLATTEN) (("2" (REPLACE -1 * RL) (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Final_lemma2| "" (LEMMA "Timer1_is_Timer") (("" (SKOLEM-TYPEPRED) (("" (INST?) (("" (REPLACE -7 * RL) (("" (LEMMA "Timer_General") (("" (INST?) (("" (LIFT-IF) (("" (SPLIT) (("1" (FLATTEN) NIL NIL) ("2" (FLATTEN) (("2" (REPLACE -1 *) (("2" (LEMMA "Timer2_lemma") (("2" (INST?) (("2" (REPLACE -1 * RL) (("2" (LEMMA "Timer_General") (("2" (INST -1 "LAMBDA (x: clock[K]): NOT Held_For(P!1, timeout1!1)(x)" "t!1" "timeout2!1") (("2" (LIFT-IF) (("2" (SPLIT) (("1" (FLATTEN) NIL NIL) ("2" (HIDE -2 -3) (("2" (FLATTEN) (("2" (BETA) (("2" (HIDE -2 -3 -4 -5 -6 -7 -8) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (GOAL "" (INDUCT "t" 1 "clock_induction") (("1" (GRIND) NIL NIL) ("2" (SKOSIMP) (("2" (SKOSIMP) (("2" (INST -1 "timeout1!1" "timeout2!1") (("2" (LEMMA "Final_lemma2") (("2" (INST -1 "PP" "timeout1!1" "timeout2!1" "t!1") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL))