-
Notifications
You must be signed in to change notification settings - Fork 0
/
Lift.i.dfy
44 lines (34 loc) · 1.08 KB
/
Lift.i.dfy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
include "Temporal.s.dfy"
module Temporal__Lift_i {
import opened Temporal__Temporal_s
type StatePredicate<!S> = S -> bool
type Action<!S> = (S,S) -> bool
type Behavior<S> = int -> S
function{:axiom} ambientBehavior<S>() : Behavior<S>
function Lift<S>(p: StatePredicate<S>) : temporal
{
i => p(ambientBehavior()(i))
}
function{:opaque} LiftAction<S>(a: Action<S>) : temporal
{
var b := ambientBehavior();
i => a(b(i), b(i+1))
}
function LiftSpec<S>(init:StatePredicate<S>, next:Action<S>) : temporal
{
and(Lift(init), always(LiftAction(next)))
}
lemma InferAlways<S>(action:Action<S>)
requires forall s, s' :: action(s, s')
ensures sat(always(LiftAction(action)))
{
reveal_LiftAction();
}
lemma InferUntil<S>(init:StatePredicate<S>, next:Action<S>,
f:StatePredicate<S>, g:StatePredicate<S>)
requires forall s, s' :: next(s, s') && f(s) ==> (f(s) || g(s))
requires sat(LiftSpec(init, next))
ensures sat(until(Lift(f), Lift(g)))
{
}
}