asm coffeeVendingMachine

import STDL/StandardLibrary
import STDL/LTLLibrary
import STDL/CTLLibrary

signature:
	enum domain CoinType = {HALF | ONE}
	enum domain Product = {COFFEE | TEA | MILK}
	domain QuantityDomain subsetof Integer	
	domain CoinDomain subsetof Integer 
	controlled available: Product -> QuantityDomain
	controlled coins: CoinDomain
	monitored insertedCoin: CoinType

definitions:
	domain QuantityDomain = {0 : 10}
	domain CoinDomain = {0 : 25}

	rule r_serveProduct($p in Product) =
		par
			coins := coins + 1
			available($p) := available($p) - 1
		endpar
		
	// Una volta che un prodotto è terminato, non può più essere nuovamente disponibile in futuro.
	LTLSPEC (forall $p in Product with g(available($p) = 0 implies g(available($p) = 0)))
//	// Nella macchinetta ci sono sempre almeno 5 unità
	LTLSPEC g(available(COFFEE) + available(MILK) + available(TEA) >= 5)
//	// Esiste uno stato in cui il latte e il tè sono terminati e ci sono ancora 9 caffè.
	CTLSPEC ef(available(MILK) + available(TEA) = 0 and available(COFFEE) = 9)
	// In qualsiasi stato si trovi la macchina, esiste sempre uno stato futuro in cui il latte è ancora disponibile
	CTLSPEC ag(ef(available(MILK)>0))

	main rule r_Main =
		if (coins < 25) then
			if (insertedCoin = HALF) then
				if (available(MILK) > 0) then
					r_serveProduct[MILK]
				endif
			else
				choose $p in {COFFEE, TEA} with available($p) > 0 do
					r_serveProduct[$p]
			endif
		endif


default init s0:
	function coins = 0
	function available($p in Product) = 10