coffee_HICmd.himaude

load hi-maude.maude .
load coffee.himaude .
---
---Place your commands below

--- Simulate cs1 until the room and coffee are equal temperatures (~0.1c)
(hfind earliest cs1 =>* {C:Configuration 
	< coffeeObj : Coffee | effort : EFF:Float >
	< roomObj : Room | effort : EFF2:Float >}
   such that (abs(EFF:Float - EFF2:Float) < 0.1) 
   using euler stepsize 0.1 discreteswitch nonaccurate .)

--- Simulate and compare cs2 and cs3, small vs. large cup
(hrew cs2 in time <= 100 using euler stepsize 1.0 discreteswitch nonaccurate .)
(hrew cs3 in time <= 100 using euler stepsize 1.0 discreteswitch nonaccurate .)
 
--- Simulate multiple cups in the room, cs4
(hrew cs4 in time <= 100 using euler stepsize 0.1 discreteswitch nonaccurate .)
 
--- Search for states where room and coffee and equal temperatures
---(  ~0.1c for the first 100 ticks
(hsearch [1] cs1 =>* {C:Configuration 
	< coffeeObj : Coffee | effort : EFF:Float >
	< roomObj : Room | effort : EFF2:Float >}
	such that (abs(EFF:Float - EFF2:Float) < 0.1)
	in time <= 100 using euler stepsize 0.1 discreteswitch nonaccurate .)
)---

--- Timed LTL model checking
---  Show that 'temp-ok' is always saisfied for the first 5 ticks
---(  temp-ok == temperature of coffee is between 65 and 95 degrees
(hmc cs1 |=t [](temp-ok) in time <= 5 using euler stepsize 1.0 discreteswitch nonaccurate .)
)---

---Place your commands above
---
q .