mod ONE-PERSON is
protecting NAT + STRING .
sorts Person Status .
op person : String Nat Status -> Person [ctor] .
ops single engaged married separated divorced deceased
widow widower : -> Status [ctor] .
var X : String . var N : Nat . var S : Status .
crl [birth-day] :
person(X, N, S) => person(X, N + 1, S) if N <= 1000 /\ S =/= deceased .
crl [successful-proposal] :
person(X, N, S) => person(X, N, engaged)
if N >= 15 /\ (S == single or S == divorced) .
rl [marriage] : person(X, N, engaged) => person(X, N, married) .
*** Rules for death, separation, broken-engagement, divorce,
*** death of spouse(?) should be added!!
endm
mod ONE-PERSON-EXT is
protecting ONE-PERSON .
var X : String . var N : Nat . var S : Status .
rl [broken-engagement] :
person(X, N, engaged) => person(X, N, single) .
rl [separation] :
person(X, N, married) => person(X, N, separated) .
rl [divorce] :
person(X, N, separated) => person(X, N, divorced) .
crl [death] :
person(X, N, S) => person(X, N, deceased)
if S =/= deceased . *** You only die once
rl [death-of-fiance] :
person(X, N, engaged) => person(X, N, single) .
rl [death-of-male-spouse] :
person(X, N, married) => person(X, N, widow) .
rl [death-of-female-spouse] :
person(X, N, married) => person(X, N, widower) .
endm
search person("Babko", 84, widow) =>1 P:Person .
search person("Edward", 30, single) =>* person("Edward", 33, S) .
show path 46 .
show path labels 46 .
search person("Edward", 30, single) =>* person("Edward", N, S)
such that N < 30 .