diff --git a/EWD123/controller/controller.go b/go/EWD123/controller/controller.go similarity index 100% rename from EWD123/controller/controller.go rename to go/EWD123/controller/controller.go diff --git a/EWD123/ewd123.go b/go/EWD123/ewd123.go similarity index 100% rename from EWD123/ewd123.go rename to go/EWD123/ewd123.go diff --git a/EWD123/ewd123a/ewd123a.go b/go/EWD123/ewd123a/ewd123a.go similarity index 100% rename from EWD123/ewd123a/ewd123a.go rename to go/EWD123/ewd123a/ewd123a.go diff --git a/EWD123/ewd123b/ewd123b.go b/go/EWD123/ewd123b/ewd123b.go similarity index 100% rename from EWD123/ewd123b/ewd123b.go rename to go/EWD123/ewd123b/ewd123b.go diff --git a/EWD123/ewd123c/ewd123c.go b/go/EWD123/ewd123c/ewd123c.go similarity index 100% rename from EWD123/ewd123c/ewd123c.go rename to go/EWD123/ewd123c/ewd123c.go diff --git a/EWD123/ewd123d/ewd123d.go b/go/EWD123/ewd123d/ewd123d.go similarity index 100% rename from EWD123/ewd123d/ewd123d.go rename to go/EWD123/ewd123d/ewd123d.go diff --git a/EWD123/ewd123dekker/ewd123dekker.go b/go/EWD123/ewd123dekker/ewd123dekker.go similarity index 100% rename from EWD123/ewd123dekker/ewd123dekker.go rename to go/EWD123/ewd123dekker/ewd123dekker.go diff --git a/mCRL2/TrafiicLights/TrafficLights v1_spec.lts b/mCRL2/TrafiicLights/TrafficLights v1_spec.lts new file mode 100644 index 0000000..bc62f41 Binary files /dev/null and b/mCRL2/TrafiicLights/TrafficLights v1_spec.lts differ diff --git a/mCRL2/TrafiicLights/TrafficLights v2_spec.lts b/mCRL2/TrafiicLights/TrafficLights v2_spec.lts new file mode 100644 index 0000000..ff183e6 Binary files /dev/null and b/mCRL2/TrafiicLights/TrafficLights v2_spec.lts differ diff --git a/mCRL2/TrafiicLights/TrafficLights v3_spec.lts b/mCRL2/TrafiicLights/TrafficLights v3_spec.lts new file mode 100644 index 0000000..750d28a Binary files /dev/null and b/mCRL2/TrafiicLights/TrafficLights v3_spec.lts differ diff --git a/mCRL2/TrafiicLights/TrafficLights v4_spec.lts b/mCRL2/TrafiicLights/TrafficLights v4_spec.lts new file mode 100644 index 0000000..c4422c5 Binary files /dev/null and b/mCRL2/TrafiicLights/TrafficLights v4_spec.lts differ diff --git a/mCRL2/TrafiicLights/TrafficLights v4_spec_bb.lts b/mCRL2/TrafiicLights/TrafficLights v4_spec_bb.lts new file mode 100644 index 0000000..92c9b80 Binary files /dev/null and b/mCRL2/TrafiicLights/TrafficLights v4_spec_bb.lts differ diff --git a/mCRL2/VendingMachine/02_VM bounded.lps b/mCRL2/VendingMachine/02_VM bounded.lps new file mode 100644 index 0000000..94e9265 Binary files /dev/null and b/mCRL2/VendingMachine/02_VM bounded.lps differ diff --git a/mCRL2/VendingMachine/02_VM bounded.lts b/mCRL2/VendingMachine/02_VM bounded.lts new file mode 100644 index 0000000..dcd93c9 Binary files /dev/null and b/mCRL2/VendingMachine/02_VM bounded.lts differ diff --git a/mCRL2/VendingMachine/VendingMachine.mcrl2proj b/mCRL2/VendingMachine/VendingMachine.mcrl2proj new file mode 100644 index 0000000..6bb9ccb --- /dev/null +++ b/mCRL2/VendingMachine/VendingMachine.mcrl2proj @@ -0,0 +1,4 @@ + + VendingMachine_spec.mcrl2 + + diff --git a/mCRL2/VendingMachine/VendingMachine_spec.mcrl2 b/mCRL2/VendingMachine/VendingMachine_spec.mcrl2 new file mode 100644 index 0000000..cc5bbaf --- /dev/null +++ b/mCRL2/VendingMachine/VendingMachine_spec.mcrl2 @@ -0,0 +1,80 @@ +% +% VM.mcrl2 +% +% A Simple Vending Machine. +% +% Copyright (c) 2019-2019 HS Emden-Leer +% All Rights Reserved. +% +% @version 1.00 - 01 Apr 2019 - GJV - initial version +% + +% ----------------------------------------------------------------------------------------------------------------------- +% +% Definition of the coins +% +sort + Coin = struct _5c | _10c | _20c | _50c | Euro; + +map + value: Coin -> Int; % the value of a coin as an integer + +eqn + value(_5c) = 5; + value(_10c) = 10; + value(_20c) = 20; + value(_50c) = 50; + value(Euro) = 100; + + +% ----------------------------------------------------------------------------------------------------------------------- +% +% Definition of the products +% +sort + Product = struct tea | coffee | cake | apple; + +map + price: Product -> Int; % the price of a product as an integer + +eqn + value(tea) = 10; + value(coffee) = 25; + value(cake) = 60; + value(apple) = 80; + +% ----------------------------------------------------------------------------------------------------------------------- +% +% Definition of the actions +% +act + accept: Coin; % accept a coin inserted into the machine + return: Coin; % returns change + offer: Product; % offer the possibility to order a certain product + serve: Product; % serve a certain product + returnChange: Int; % request to return the current credit as change + +% +% Definition of the processes +% +proc + VendingMachine = VM(0); + + VM(credit : Int) = + (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); + + + ReturnChange(credit : Int) = + sum c : Coin.((credit >= value(c) && credit < next(c)) -> return(c).( + ((credit - value(c)) >0) -> ReturnChange(credit - value(c)) <> VM(credit - value(c)) + )); + +% ----------------------------------------------------------------------------------------------------------------------- + +init + VendingMachine +;