from crestdsl.model import *
# Resources require a unit and domain
watt = Resource(unit="Watt",domain=REAL)
celsius = Resource("Celsius", INTEGER)
onoffSwitch = Resource("Switch", ["on","off"])
colour = Resource("Colour",["red","green"])
time = Resource("Time", REAL)
class AirCon(Entity):
temperature = Input(celsius, 24)
switch = Input(onoffSwitch, "off")
coolingpower = Output(watt, 0)
statuslight = Output(colour, "red")
on = State()
off = current = State()
my_new_ac = AirCon()
my_other_ac = AirCon()
class DynamicAirCon(AirCon):
# add the ontime port
ontime = Local(time, 0)
# A transition created by a transition object
off_to_on = Transition(source="off", target="on", guard=(lambda self: self.temperature.value > 22 and self.switch.value == "on" and self.ontime.value <= 0))
# Another transition, this time using the decorator
@transition(source="on", target="off")
def on_to_off(self):
return self.temperature.value <= 22 or self.switch.value == "off" or self.ontime.value >= 30
# update ontime
ontime_when_on = Update(state="on", target=ontime, function=(lambda self, dt: self.ontime.value + dt))
# An update via decorator
@update(state="off", target="ontime")
def ontime_when_off(self, dt):
new_time = self.ontime.value - 5 * dt
return max(0, new_time)
# Adding an update as object
cooling_when_off = Update(state="off", target="coolingpower", function=(lambda self, dt: 0))
# An update via decorator
@update(state="on", target="coolingpower")
def cooling_when_on(self, dt):
return (self.temperature.value - 22) * 50
@influence(source="switch", target="statuslight")
def light_influence(value):
if value == "on":
return "green"
else:
return "red"
dyn_ac = DynamicAirCon()
from crestdsl.ui import plot
plot(DynamicAirCon())
from crestdsl.simulation import Simulator
system = DynamicAirCon() # create system
sim = Simulator(system) # init simulator
sim.stabilise() # fsm state is off
print(system.current, system.ontime.value)
system.switch.value = "on" # modify input
sim.stabilise() # state: on
print(system.current, system.ontime.value, system.switch.value)
sim.advance(10) # ontime: 10
print(system.current, system.ontime.value)
sim.advance(20) # ontime: 30, state: off
print(system.current, system.ontime.value)
ERROR:crestdsl.simulation.interactivesimulator:There is an error in the 'colored' package. They use 'fileno'. I guess we have to wait for a fix.
DynamicAirCon.off 0 DynamicAirCon.on 0 on DynamicAirCon.on 10 DynamicAirCon.off 30
from crestdsl.verification import check, is_possible, always, before
system = DynamicAirCon()
system.switch.value = "on" # turn on the AC
chk = check(system.ontime) == 25
# model checking
print(is_possible(chk).check()) # True
print(always(chk).check()) # False
WARNING:crestdsl.verification.verifier:Caution: No end time set for formula. This means statespace will be explored until exhausted (possibly forever !!) WARNING:crestdsl.verification.verifier:Caution: No end time set for formula. This means statespace will be explored until exhausted (possibly forever !!)
True False
from crestdsl.verification import tctl, check, StateSpace, ModelChecker
# define a system and check
system = DynamicAirCon()
system.switch.value = "on" # turn on the AC
chk = check(system) == system.on
reach_within_30 = tctl.EF(chk, tctl.Interval(end=30))
# explore state space and model checking
statespace = StateSpace(system)
statespace.explore()
mc = ModelChecker(statespace)
mc.check(reach_within_30)
True