diff --git a/mCRL2/VendingMachine/.DS_Store b/mCRL2/VendingMachine/.DS_Store
new file mode 100644
index 0000000..5008ddf
Binary files /dev/null and b/mCRL2/VendingMachine/.DS_Store differ
diff --git a/mCRL2/VendingMachine/VendingMachine_spec.lps b/mCRL2/VendingMachine/VendingMachine_spec.lps
new file mode 100644
index 0000000..4ef8f62
Binary files /dev/null and b/mCRL2/VendingMachine/VendingMachine_spec.lps differ
diff --git a/mCRL2/VendingMachine/VendingMachine_spec.lts b/mCRL2/VendingMachine/VendingMachine_spec.lts
new file mode 100644
index 0000000..2d52125
Binary files /dev/null and b/mCRL2/VendingMachine/VendingMachine_spec.lts differ
diff --git a/mCRL2/VendingMachine/VendingMachine_spec.mcrl2 b/mCRL2/VendingMachine/VendingMachine_spec.mcrl2
index 7bfedb3..6b7cdef 100644
--- a/mCRL2/VendingMachine/VendingMachine_spec.mcrl2
+++ b/mCRL2/VendingMachine/VendingMachine_spec.mcrl2
@@ -18,7 +18,7 @@ sort
 
 map
 	value: Coin  -> Int;	% the value of a coin as an integer
-	next:  Coin  -> Coin;
+	next:  Coin -> Int;
 
 eqn
 	value(_5c) = 5;
@@ -27,10 +27,11 @@ eqn
 	value(_50c) = 50;
 	value(Euro) = 100;
 
-	next(Euro) = _50c;
-	next(_50c) = _20c;
-	next(_20c) = _10c;
-	next(_10c) = _5c;
+	next(Euro) = 10000;
+	next(_50c) = 100;
+	next(_20c) = 50;
+	next(_10c) = 20;
+	next(_5c) = 10;
 
 
 % -----------------------------------------------------------------------------------------------------------------------
@@ -68,15 +69,15 @@ proc
 
 	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);
+		+ sum p : Product.(
+			(credit >= price(p)) -> offer(p).serve(p).VM(credit - price(p))
+		)
 	
 
 	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))
+			((credit - value(c)) > 0) -> ReturnChange(credit - value(c)) <> VM(credit - value(c))
 	));
 
 % -----------------------------------------------------------------------------------------------------------------------