40 lines
1.1 KiB
Markdown
40 lines
1.1 KiB
Markdown
|
|
||
|
|
```c
|
||
|
|
module Offices
|
||
|
|
|
||
|
|
type office = One | Two | Three
|
||
|
|
type person = Ana | Nuno | Pedro | Maria
|
||
|
|
|
||
|
|
predicate hasOffice (person) (office)
|
||
|
|
|
||
|
|
axiom A1 : forall p:person. exists o:office. hasOffice p o
|
||
|
|
axiom A2 : forall p:person, o1 o2 : office.
|
||
|
|
hasOffice p o1 /\ hasOffice p o2 -> o1 = o2
|
||
|
|
|
||
|
|
axiom B : forall o1 o2 : office. hasOffice Pedro o1 /\ hasOffice Nuno o2 ->
|
||
|
|
o1 <> o2
|
||
|
|
|
||
|
|
predicate alone (p:person) = forall o:office. forall p1:person.
|
||
|
|
(hasOffice p o) /\ hasOffice p1 o -> p = p1
|
||
|
|
|
||
|
|
axiom C : alone Ana -> alone Pedro
|
||
|
|
axiom D : forall p1 p2 p3: person, o:office.
|
||
|
|
hasOffice p1 o /\ hasOffice p2 o /\ hasOffice p3 o ->
|
||
|
|
p1 = p2 \/ p1 = p3 \/ p3 = p2
|
||
|
|
|
||
|
|
goal sanity_test : false (*check if the model makes sense*)
|
||
|
|
|
||
|
|
goal g1 : hasOffice Maria One -> alone Maria
|
||
|
|
goal g2 : forall o1:office. (hasOffice Ana o1 /\ hasOffice Nuno o1) ->
|
||
|
|
exists o2:office. hasOffice Pedro o2 /\ hasOffice Maria o2
|
||
|
|
|
||
|
|
predicate empty (o:office) = forall p:person. not (hasOffice p o)
|
||
|
|
|
||
|
|
lemma atMostOneEmpty : forall o1 o2: office. empty o1 /\ empty o2 ->
|
||
|
|
o1 = o2
|
||
|
|
|
||
|
|
end
|
||
|
|
```
|
||
|
|
|
||
|
|
|