+ mcrl2 files

mCRL2/VendingMachine/VendingMachine.mcrl2proj

@@ -0,0 +1,4 @@
+<root>
+ <spec>VendingMachine_spec.mcrl2</spec>
+ <properties/>
+</root>

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
+;