e8da2e15 by Ulrich Schoepp

Loesung Aufgabe 11-2d)

1 parent 5e3ed226
MODULE main
VAR
lineP : {a, b};
x : {0, 1, 2};
y : {0, 1, 2};
INIT
x=0 & y=0 & lineP=a
TRANS
lineP=a & next(lineP)=b & next(x)=1 & next(y)=y
| lineP=b & next(lineP)=a & next(x)=x & next(y)=2
| next(lineP)=lineP & next(x)=y & next(y)=y
SPEC
AG(y!=0 -> AG(x!=0))
MODULE main
VAR
lineP : {a, b};
x : {0, 1, 2};
y : {0, 1, 2};
selector: {p, q};
ASSIGN
init(lineP) := a;
init(x) := 0;
init(y) := 0;
next(lineP) := case selector=p & lineP=a : {a, b};
selector=p & lineP=b : {a, b};
selector=q : lineP;
esac;
next(x) := case selector=p & lineP=a : 1;
selector=p & lineP=b : x;
selector=q : y;
esac;
next(y) := case selector=p & lineP=b : 2;
TRUE: y;
esac;
SPEC
AG(y!=0 -> AG(x!=0))
MODULE P(x, y)
VAR
lineP : {a, b};
ASSIGN
init(lineP) := a;
next(lineP) := case lineP=a : b;
lineP=b : a;
esac;
next(x) := case lineP=a : 1;
TRUE : x;
esac;
next(y) := case lineP=b : 2;
TRUE: y;
esac;
MODULE Q(x, y)
ASSIGN
next(x) := y;
next(y) := y;
MODULE main
VAR
x : {0, 1, 2};
y : {0, 1, 2};
p: process P(x, y);
q: process Q(x, y);
ASSIGN
init(x) := 0;
init(y) := 0;
SPEC
AG(y!=0 -> AG(x!=0))
Styling with Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!