DocName Project Version FullName ShortDescription
EnvRoad RailwayCrossing V2
ModelName Number Type
ModelName Description Strategy StrategyType RealizedRequirement
EnvRoadTask1 generating cars periodically If curMode is period, generate every perDur a new car. Increment noOfCars accordingly f
EnvRoadTask2 generating cars on event After receiving genCars, create the given number of cars. Increment noOfCars accordingly. Set curMode to event.  f
EnvRoadTask3 setting period to create cars By receiving setPeriod, set curMode to period and set perDur to the given value.  f
EnvRoadTask4 signaling number of cars If noOfCars is greater than maxNoOfCars, send newCarSens to the environment. f
EnvRoadTask5 set the maxNoOfCars By receiving setMaxNoOfCars, set maxNoOfCars to the given value.  f
EnvRoadTask6 decrementing cars After receiving gateOpen, start decrementing noOfCars, until noOfCars = 0 or signbal gateClosed is received. f
ModelName FullName Type Value Tasks Usage Description
curMode Enum (period, event) period EnvRoadTask1, EnvRoadTask2, EnvRoadTask3
perDur Duration 10 EnvRoadTask1, EnvRoadTask3
noOfCars Integer 0 EnvRoadTask1, EnvRoadTask2, EnvRoadTask4, EnvRoadTask6
maxNoOfCars Integer 5 EnvRoadTask4, EnvRoadTask5
ModelName FullName Parameters Tasks Usage Description SignalPaths
genCars Integer EnvRoadTask2 c
setPeriod Duration EnvRoadTask3 c
newCarSens EnvRoadTask4 p
setMaxNoOfCars Integer EnvRoadTask5 c
gateOpen EnvRoadTask6 c
gateClosed EnvRoadTask6