-
Notifications
You must be signed in to change notification settings - Fork 1
/
bitml-predicate.maude
65 lines (54 loc) · 2.13 KB
/
bitml-predicate.maude
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
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
***
*** Given a Configuration, check if it satisfies a Predicate
***
set print attribute on . *** enable print attribute (see equation with Failure("..."))
fmod BITML-PREDICATE-SAT is
protecting BITML-SYNTAX .
protecting BITML-AUX .
protecting SATISFACTION .
subsort Configuration < State .
var b b' : Bool .
var P P' : Predicate .
var S S' : Configuration .
var a : Secret .
var a^ : Set{Secret} .
vars N x y s t : Nat .
vars n m : Int .
var A : Participant .
vars E E' E'' : Expression .
vars p p' : Predicate .
op predicate_ : Predicate -> Prop .
***
*** A configuration satisfies a predicate if it evaluates to Success(true)
***
eq S |= predicate P = [ P ] { S } == Success(true) .
ceq S | S' |= predicate P = S |= predicate P or-else S' |= predicate P if S =/= 0 /\ S' =/= 0 .
eq S |= predicate P = false [owise] .
***
*** Simplifications
***
eq ! ! P = P .
eq ! True = False .
eq ! False = True .
eq True && P = P .
eq False && P = False .
***
*** Evaluation of predicates
***
op [_] {_} : Predicate Configuration -> Try .
eq [ True ] { S } = Success(true) .
eq [ False ] { S } = Success(false) .
ceq [ P && P' ] { S } = Success(b and b') if Success(b) := [ P ] { S } /\ Success(b') := [ P' ] { S } .
ceq [ ! P ] { S } = Success(not b) if Success(b) := [ P ] { S } .
ceq [ E == E' ] { S } = Success(n == m) if Success(n) := [ E ] { S } /\ Success(m) := [ E' ] { S } .
ceq [ E < E' ] { S } = Success(n < m) if Success(n) := [ E ] { S } /\ Success(m) := [ E' ] { S } .
eq [ P ] { S } = Failure("Unable to evaluate the predicate") [owise print "Error evaluating " P " in " S] .
***
*** Evaluation of expressions
***
op [_] {_} : Expression Configuration -> Try .
eq [ const(n) ] { S } = Success(n) .
eq [ size(a) ] { (A : a # N) | S } = Success(N) .
ceq [ E + E' ] { S } = Success(n + m) if Success(n) := [ E ] { S } /\ Success(m) := [ E' ] { S } .
eq [ E ] { S } = Failure("Unable to evaluate the expression") [owise print "Error evaluating " E " in " S] .
endfm