package Valve
import Timer.SimulatedTimer
-//JPF's Verify API
-import gov.nasa.jpf.vm.Verify
-
public class Valves {
int deviceNumbers
List valves
private String valve = "closed"
private String valveLatestValue = "closed"
- Valves(Closure sendEvent, int deviceNumbers) {
+ Valves(Closure sendEvent, int deviceNumbers, boolean init) {
this.sendEvent = sendEvent
this.timers = new SimulatedTimer()
this.deviceNumbers = deviceNumbers
this.valves = []
- def init = Verify.getBoolean()
if (init) {
this.valve = "closed"
this.valveLatestValue = "closed"
def find(Closure Input) {
valves.find(Input)
}
+ def sort(Closure Input) {
+ valves.sort(Input)
+ }
def collect(Closure Input) {
valves.collect(Input)
}
//By Apps
def open() {
- if (valve != "open")
+ if (valve != "open") {
+ this.valve = "open"
+ this.valveLatestValue = "open"
valves[0].open()
+ }
}
def open(LinkedHashMap metaData) {
if (valve != "open") {
def task = timers.runAfter(metaData["delay"]) {
+ this.valve = "open"
+ this.valveLatestValue = "open"
valves[0].open()
}
}
}
def close() {
- if (valve != "closed")
+ if (valve != "closed") {
+ this.valve = "closed"
+ this.valveLatestValue = "closed"
valves[0].close()
+ }
}
def close(LinkedHashMap metaData) {
if (valve != "closed") {
def task = timers.runAfter(metaData["delay"]) {
+ this.valve = "closed"
+ this.valveLatestValue = "closed"
valves[0].close()
}
}
//By Model Checker
def setValue(LinkedHashMap eventDataMap) {
if (eventDataMap["value"] != valves[0].valve) {
+ this.valve = eventDataMap["value"]
valves[0].setValue(eventDataMap["value"])
- this.valve = valves[0].valve
}
}