Studium
/
Parallele_Verteilte_Systeme
2
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

A2a fertig

This commit is contained in:
Johannes Theiner 2020-04-25 10:57:28 +02:00
parent f9778818f3
commit cf0f988c9c
4 changed files with 10 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

BIN
mCRL2/VendingMachine/.DS_Store vendored Normal file
View File

Binary file not shown.

BIN
mCRL2/VendingMachine/VendingMachine_spec.lps Normal file
View File

Binary file not shown.

BIN
mCRL2/VendingMachine/VendingMachine_spec.lts Normal file
View File

Binary file not shown.

19
mCRL2/VendingMachine/VendingMachine_spec.mcrl2
View File

@ -18,7 +18,7 @@ sort
map map
value: Coin -> Int; % the value of a coin as an integer value: Coin -> Int; % the value of a coin as an integer
next: Coin -> Coin; next: Coin -> Int;
eqn eqn
value(_5c) = 5; value(_5c) = 5;
@ -27,10 +27,11 @@ eqn
value(_50c) = 50; value(_50c) = 50;
value(Euro) = 100; value(Euro) = 100;
next(Euro) = _50c; next(Euro) = 10000;
next(_50c) = _20c; next(_50c) = 100;
next(_20c) = _10c; next(_20c) = 50;
next(_10c) = _5c; next(_10c) = 20;
next(_5c) = 10;
% ----------------------------------------------------------------------------------------------------------------------- % -----------------------------------------------------------------------------------------------------------------------
@ -68,15 +69,15 @@ proc
VM(credit : Int) = VM(credit : Int) =
(credit < 200) -> sum c : Coin.accept(c).VM(credit + value(c)) (credit < 200) -> sum c : Coin.accept(c).VM(credit + value(c))
+ sum p : Product.(
(credit > 0) -> returnChange(credit).ReturnChange(credit + price(p))
)
+ (credit > 0) -> returnChange(credit).ReturnChange(credit); + (credit > 0) -> returnChange(credit).ReturnChange(credit);
+ sum p : Product.(
(credit >= price(p)) -> offer(p).serve(p).VM(credit - price(p))
)
ReturnChange(credit : Int) = ReturnChange(credit : Int) =
sum c : Coin.((credit >= value(c) && credit < next(c)) -> return(c).( sum c : Coin.((credit >= value(c) && credit < next(c)) -> return(c).(
((credit - value(c)) >0) -> ReturnChange(credit - value(c)) <> VM(credit - value(c)) ((credit - value(c)) > 0) -> ReturnChange(credit - value(c)) <> VM(credit - value(c))
)); ));
% ----------------------------------------------------------------------------------------------------------------------- % -----------------------------------------------------------------------------------------------------------------------