smoke step设置为4

X出不来是因为有smoke一直在detected不变的情况，也不是，只要smoke

NuSMV > check_ltlspec -p "G((smoke=detected)->X(window.switch=open))"
-- specification  G (smoke = detected ->  X window.switch = open)  is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample-> State: 1.1 <-window.switch = closeweather.rain = not_rainingweather.rainState = not_rainingrain_count = 1smoke = detectedsmokeState = clearsmoke_count = 1runinwindow.timer = 0delaywindow = 0-> State: 1.2 <-window.switch = openrain_count = 0smokeState = detectedsmoke_count = 0delaywindow = 5-> State: 1.3 <-weather.rain = rainingrain_count = 1runinwindow.timer = 5-> State: 1.4 <-window.switch = closeweather.rainState = rainingrain_count = 0smoke = clearsmoke_count = 1runinwindow.timer = 4-- Loop starts here-> State: 1.5 <-weather.rain = not_rainingrain_count = 1smokeState = clearsmoke_count = 0runinwindow.timer = 3-> State: 1.6 <-weather.rainState = not_rainingrain_count = 0runinwindow.timer = 2-> State: 1.7 <-smoke = detectedsmoke_count = 1runinwindow.timer = 1-> State: 1.8 <-window.switch = opensmokeState = detectedsmoke_count = 0runinwindow.timer = 0-> State: 1.9 <-weather.rain = rainingrain_count = 1smoke = clearsmoke_count = 1runinwindow.timer = 5-> State: 1.10 <-window.switch = closeweather.rainState = rainingrain_count = 0smokeState = clearsmoke_count = 0runinwindow.timer = 4-> State: 1.11 <-weather.rain = not_rainingrain_count = 1runinwindow.timer = 3

NuSMV > check_ltlspec -p "G((smoke=detected)->F(window.switch=open))"
-- specification  G (smoke = detected ->  F window.switch = open)  is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample-> State: 2.1 <-window.switch = openweather.rain = rainingweather.rainState = not_rainingrain_count = 1smoke = clearsmokeState = clearsmoke_count = 1runinwindow.timer = 0delaywindow = 0-> State: 2.2 <-window.switch = closeweather.rainState = rainingrain_count = 0smoke_count = 0-> State: 2.3 <-weather.rain = not_rainingrain_count = 1smoke = detectedsmoke_count = 1-> State: 2.4 <-window.switch = openweather.rainState = not_rainingrain_count = 0smokeState = detectedsmoke_count = 0delaywindow = 5-> State: 2.5 <-weather.rain = rainingrain_count = 1runinwindow.timer = 5-> State: 2.6 <-window.switch = closeweather.rainState = rainingrain_count = 0runinwindow.timer = 4-> State: 2.7 <-weather.rain = not_rainingrain_count = 1smoke = clearsmoke_count = 1runinwindow.timer = 3-> State: 2.8 <-weather.rainState = not_rainingrain_count = 0smokeState = clearsmoke_count = 0runinwindow.timer = 2-> State: 2.9 <-runinwindow.timer = 1-- Loop starts here-> State: 2.10 <-runinwindow.timer = 0delaywindow = 0-> State: 2.11 <-

smoke_fix1，直接跳过一步固定自然属性

冲突状态仍存在

NuSMV > check_ltlspec -p "G((smoke=detected)->!X(window.switch=open))"
-- specification  G (smoke = detected -> !( X window.switch = open))  is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample-> State: 1.1 <-window.switch = closeweather.rain = not_rainingweather.rainState = not_rainingrain_count = 1smoke = detectedsmokeState = clearsmoke_count = 1runinwindow.timer = 0delaywindow = 0flag1 = TRUEflag2 = FALSEstep = 1-> State: 1.2 <-window.switch = openrain_count = 0smokeState = detectedsmoke_count = 0delaywindow = 5step = 2-> State: 1.3 <-weather.rain = rainingrain_count = 1runinwindow.timer = 5step = 3-> State: 1.4 <-window.switch = closeweather.rainState = rainingrain_count = 0runinwindow.timer = 4step = 4-> State: 1.5 <-weather.rain = not_rainingrain_count = 1runinwindow.timer = 3step = 0-> State: 1.6 <-weather.rainState = not_rainingrain_count = 0runinwindow.timer = 2-> State: 1.7 <-runinwindow.timer = 1-- Loop starts here-> State: 1.8 <-runinwindow.timer = 0delaywindow = 0-> State: 1.9 <-

smoke_fix2

INVAR
!(flag1 = TRUE & flag2 = FALSE) 也不行

NuSMV > check_ltlspec -p "G((smoke=detected)->!X(window.switch=open))"
-- specification  G (smoke = detected -> !( X window.switch = open))  is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample-> State: 1.1 <-window.switch = closeweather.rain = not_rainingweather.rainState = not_rainingrain_count = 1smoke = detectedsmokeState = clearsmoke_count = 1runinwindow.timer = 0delaywindow = 0flag1 = FALSEflag2 = FALSEstep = 1-> State: 1.2 <-window.switch = openrain_count = 0smokeState = detectedsmoke_count = 0delaywindow = 5step = 2-> State: 1.3 <-weather.rain = rainingrain_count = 1runinwindow.timer = 5step = 3-> State: 1.4 <-window.switch = closeweather.rainState = rainingrain_count = 0runinwindow.timer = 4step = 4-> State: 1.5 <-weather.rain = not_rainingrain_count = 1runinwindow.timer = 3step = 0-> State: 1.6 <-weather.rainState = not_rainingrain_count = 0runinwindow.timer = 2-> State: 1.7 <-runinwindow.timer = 1-- Loop starts here-> State: 1.8 <-runinwindow.timer = 0delaywindow = 0-> State: 1.9 <-

smoke_fix3(未实行) 改action

smoke_fix3

INVAR
!(flag1 = TRUE & flag2 = FALSE)
INVAR
!(flag1 = FALSE & flag2 = FALSE)

  -> State: 1.1 <-window.switch = closeweather.rain = not_rainingweather.rainState = not_rainingrain_count = 1smoke = detectedsmokeState = clearsmoke_count = 1runinwindow.timer = 0delaywindow = 0flag1 = FALSEflag2 = TRUEstep = 1-> State: 1.2 <-window.switch = openrain_count = 0smokeState = detectedsmoke_count = 0delaywindow = 5step = 2-> State: 1.3 <-weather.rain = rainingrain_count = 1runinwindow.timer = 5step = 3-> State: 1.4 <-weather.rainState = rainingrain_count = 0runinwindow.timer = 4step = 4-> State: 1.5 <-weather.rain = not_rainingrain_count = 1smoke = clearsmoke_count = 1runinwindow.timer = 3step = 0-> State: 1.6 <-weather.rainState = not_rainingrain_count = 0smokeState = clearsmoke_count = 0runinwindow.timer = 2-> State: 1.7 <-runinwindow.timer = 1-- Loop starts here-> State: 1.8 <-window.switch = closeruninwindow.timer = 0delaywindow = 0-> State: 1.9 <-

smoke_2 step为6

close 不设置延迟，open可以设置延迟，先不设置延迟，相当于延迟的值为无限，只是打开窗户，如果无限时间都满足，那么短暂时间也满足。如果不满足就考虑延迟

-- specification  G (smoke = detected ->  X window.switch = open)  is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample-> State: 1.1 <-window.switch = closeweather.rain = not_rainingweather.rainState = not_rainingrain_count = 1smoke = detectedsmokeState = clearsmoke_count = 1runinwindow.timer = 0delaywindow = 0-> State: 1.2 <-window.switch = openrain_count = 0smokeState = detectedsmoke_count = 0delaywindow = 5-> State: 1.3 <-weather.rain = rainingrain_count = 1smoke = clearsmoke_count = 1runinwindow.timer = 5-> State: 1.4 <-window.switch = closeweather.rainState = rainingrain_count = 0smokeState = clearsmoke_count = 0runinwindow.timer = 4-> State: 1.5 <-smoke = detectedsmoke_count = 1runinwindow.timer = 3-> State: 1.6 <-weather.rain = not_rainingrain_count = 1smokeState = detectedsmoke_count = 0runinwindow.timer = 2-> State: 1.7 <-weather.rainState = not_rainingrain_count = 0smoke = clearsmoke_count = 1runinwindow.timer = 1-- Loop starts here-> State: 1.8 <-smokeState = clearsmoke_count = 0runinwindow.timer = 0delaywindow = 0-> State: 1.9 <-

smoke_2_fix1

(weather.rainState != weather.rain)) &(weather.rain = raining) & (smoke = detected): open;

NuSMV > check_ltlspec -p "G((smoke=detected)->!X(window.switch=open))"
-- specification  G (smoke = detected -> !( X window.switch = open))  is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample-> State: 1.1 <-window.switch = closeweather.rain = not_rainingweather.rainState = not_rainingrain_count = 1smoke = detectedsmokeState = clearsmoke_count = 1runinwindow.timer = 0delaywindow = 0flag1 = TRUEflag2 = FALSEflag3 = TRUEflag4 = TRUEflag5 = FALSEflag6 = FALSEstep = 1step_uperlimit = 6-> State: 1.2 <-window.switch = openrain_count = 0smokeState = detectedsmoke_count = 0delaywindow = 5step = 2-> State: 1.3 <-weather.rain = rainingrain_count = 1smoke = clearsmoke_count = 1runinwindow.timer = 5step = 3-> State: 1.4 <-window.switch = closeweather.rainState = rainingrain_count = 0smokeState = clearsmoke_count = 0runinwindow.timer = 4step = 4-> State: 1.5 <-smoke = detectedsmoke_count = 1runinwindow.timer = 3step = 5-> State: 1.6 <-weather.rain = not_rainingrain_count = 1smokeState = detectedsmoke_count = 0runinwindow.timer = 2step = 6-> State: 1.7 <-weather.rainState = not_rainingrain_count = 0runinwindow.timer = 1step = 0-- Loop starts here-> State: 1.8 <-runinwindow.timer = 0delaywindow = 0-> State: 1.9 <-

smoke_2_fix2 冲突状态仍存在

!(flag1 = TRUE & flag2 = FALSE & flag3 = TRUE & flag4 = TRUE & flag5 = FALSE & flag6 = FALSE)

smoke_2_fix3 同上

!( flag1 = TRUE & flag2 = FALSE & flag3 = TRUE & flag4 = FALSE & flag5 = FALSE & flag6 = FALSE)

smoke_2_fix4

INVAR
!( flag1 = TRUE & flag2 = FALSE & flag3 = TRUE & flag4 = FALSE & flag5 = TRUE & flag6 = FALSE)

分析反例后
(weather.rain = raining)&(smokeState != smoke)&(smoke = detected) : open;
与 smokeState != smoke & smoke = detected & (weather.rain = not_raining): open;合并

因为无限都能满足，那么出于人性化可以设置为延时，这里无限满足不了

NuSMV > check_ltlspec -p "G((smoke=detected)->!X(window.switch=open))"
-- specification  G (smoke = detected -> !( X window.switch = open))  is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample-> State: 1.1 <-window.switch = closeweather.rain = not_rainingweather.rainState = not_rainingrain_count = 1smoke = detectedsmokeState = clearsmoke_count = 1runinwindow.timer = 0delaywindow = 0flag1 = TRUEflag2 = FALSEflag3 = FALSEflag4 = TRUEflag5 = FALSEflag6 = TRUEstep = 1step_uperlimit = 6-> State: 1.2 <-window.switch = openrain_count = 0smokeState = detectedsmoke_count = 0delaywindow = 5step = 2-> State: 1.3 <-weather.rain = rainingrain_count = 1smoke = clearsmoke_count = 1runinwindow.timer = 5step = 3-> State: 1.4 <-window.switch = closeweather.rainState = rainingrain_count = 0smokeState = clearsmoke_count = 0runinwindow.timer = 4step = 4-> State: 1.5 <-smoke = detectedsmoke_count = 1runinwindow.timer = 3step = 5-> State: 1.6 <-window.switch = openweather.rain = not_rainingrain_count = 1smokeState = detectedsmoke_count = 0runinwindow.timer = 2step = 6-> State: 1.7 <-weather.rainState = not_rainingrain_count = 0runinwindow.timer = 1step = 0-- Loop starts here-> State: 1.8 <-window.switch = closeruninwindow.timer = 0delaywindow = 0-> State: 1.9 <-

smoke_3 delay也要跟着改，这里新增规则和原延时重合，不需要新增延时

step为8
特点runin=1在冲突的前一状态
7、8：不好好设置延时会导致规则执行完仍未消除smoke，smoke->规则执行结束的close。一直smoke

  -> State: 1.1 <-window.switch = closeweather.rain = rainingweather.rainState = not_rainingrain_count = 1smoke = detectedsmokeState = clearsmoke_count = 1runinwindow.timer = 0delaywindow = 0-> State: 1.2 <-window.switch = openweather.rainState = rainingrain_count = 0smokeState = detectedsmoke_count = 0delaywindow = 5-> State: 1.3 <-weather.rain = not_rainingrain_count = 1runinwindow.timer = 5-> State: 1.4 <-weather.rainState = not_rainingrain_count = 0runinwindow.timer = 4-> State: 1.5 <-runinwindow.timer = 3-> State: 1.6 <-runinwindow.timer = 2-> State: 1.7 <-runinwindow.timer = 1-> State: 1.8 <-window.switch = closesmoke = clearsmoke_count = 1runinwindow.timer = 0delaywindow = 0-- Loop starts here-> State: 1.9 <-smokeState = clearsmoke_count = 0-> State: 1.10 <-

smoke_4

属于无trigger，ruin不好弄的情况
抽象原规则，新规则，延时（无延迟0，固定时长和非固定），而且基于规则定期trigger和无法until的特性
抽象原规则不能解决就加延时，然后新规则，延时

    runinwindow.timer=1 & window.switch=open: close;smokeState != smoke & smoke = detected: {0,5};

将延时换为smokeState != smoke & smoke = clear & window.switch=open: close;

-> State: 1.1 <-
smoke = detected
smoke_last = clear
smoke_count = 1
window.switch = close
window.switch_last = close
weather.rain = not_raining
weather.rain_last = raining
weather.rain_count = 1
delay_window.switch_open_0 = 0
runin_window.switch_open_0.timer = 0
-> State: 1.2 <-
smoke_last = detected
smoke_count = 0
window.switch = open
weather.rain_last = not_raining
weather.rain_count = 0
delay_window.switch_open_0 = 5
-> State: 1.3 <-
smoke = clear
smoke_count = 1
window.switch_last = open
runin_window.switch_open_0.timer = 5
-> State: 1.4 <-
smoke_last = clear
smoke_count = 0
weather.rain = raining
weather.rain_count = 1
runin_window.switch_open_0.timer = 4
-> State: 1.5 <-
smoke = detected
smoke_count = 1
window.switch = close
weather.rain_last = raining
weather.rain_count = 0
runin_window.switch_open_0.timer = 3
-> State: 1.6 <-
smoke_last = detected
smoke_count = 0
window.switch_last = close
runin_window.switch_open_0.timer = 2
-> State: 1.7 <-
smoke = clear
smoke_count = 1
runin_window.switch_open_0.timer = 1
-> State: 1.8 <-
smoke_last = clear
smoke_count = 0
delay_window.switch_open_0 = 0
runin_window.switch_open_0.timer = 0
-> State: 1.9 <-
smoke = detected
smoke_count = 1
weather.rain = not_raining
weather.rain_count = 1