rain1，冲突状态前有三个状态，step设置为4，或者优先上一状态，无效才说明是extended

同时smoke和runin到期，确实要smoke放runin前

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

fix1 通过改not_raining自然属性，所以不行，或者说是正常执行情况,rain属于影响不了的，温度属于能影响的，smoke也可以固定，包括在冲突状态 找close的原因，或open rain不同时出现的原因

flag反映了单谓词到多谓词

  -> State: 1.1 <-window.switch = closeweather.rain = rainingweather.rainState = not_rainingrain_count = 1smoke = clearsmokeState = clearsmoke_count = 1runinwindow.timer = 0delaywindow = 0step = 1flag1 = TRUEflag2 = FALSEflag3 = FALSEflag4 = TRUEflag5 = FALSE-> State: 1.2 <-weather.rainState = rainingrain_count = 0smoke_count = 0step = 2flag3 = TRUEflag4 = FALSEflag5 = TRUE-> State: 1.3 <-weather.rain = not_rainingrain_count = 1smoke = detectedsmoke_count = 1step = 3-- Loop starts here-> State: 1.4 <-weather.rainState = not_rainingrain_count = 0smokeState = detectedsmoke_count = 0step = 0-> State: 1.5 <-

fix2 冲突状态仍存在，不处理而是共享后面正常结束的close，也是正常执行路径 改LTL为X、U不行，说明当前配置不行，应该!=原配置

  -> State: 1.1 <-window.switch = closeweather.rain = rainingweather.rainState = not_rainingrain_count = 1smoke = clearsmokeState = clearsmoke_count = 1runinwindow.timer = 0delaywindow = 0step = 1flag1 = TRUEflag2 = FALSEflag3 = FALSEflag4 = TRUEflag5 = FALSE-> State: 1.2 <-weather.rainState = rainingrain_count = 0smoke_count = 0step = 2flag3 = TRUEflag4 = FALSEflag5 = TRUE-> State: 1.3 <-smoke = detectedsmoke_count = 1step = 3-> State: 1.4 <-window.switch = opensmokeState = detectedsmoke_count = 0delaywindow = 5step = 4-> State: 1.5 <-weather.rain = not_rainingrain_count = 1runinwindow.timer = 5step = 0-> State: 1.6 <-weather.rainState = not_rainingrain_count = 0runinwindow.timer = 4-> State: 1.7 <-runinwindow.timer = 3-> State: 1.8 <-runinwindow.timer = 2-> State: 1.9 <-runinwindow.timer = 1-- Loop starts here-> State: 1.10 <-window.switch = closeruninwindow.timer = 0delaywindow = 0-- Loop starts here-> State: 1.11 <--> State: 1.12 <-

fix3 同上

INVAR
!(flag1 = TRUE & flag2 = FALSE)

fix4 搜索有没有冲突状态，发现没有

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

  -> State: 1.1 <-window.switch = closeweather.rain = rainingweather.rainState = not_rainingrain_count = 1smoke = clearsmokeState = clearsmoke_count = 1runinwindow.timer = 0delaywindow = 0step = 1flag1 = FALSEflag2 = TRUEflag3 = FALSEflag4 = TRUEflag5 = FALSE-> State: 1.2 <-weather.rainState = rainingrain_count = 0smoke_count = 0step = 2flag3 = TRUE-> State: 1.3 <-smoke = detectedsmoke_count = 1step = 3-> State: 1.4 <-smokeState = detectedsmoke_count = 0step = 4-> State: 1.5 <-weather.rain = not_rainingrain_count = 1step = 0-- Loop starts here-> State: 1.6 <-weather.rainState = not_rainingrain_count = 0-> State: 1.7 <-

rain1_1 冲突状态前有4个状态，step设置为5。一直open

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

rain1_1_fix1 1.5的自然状态不同，而且满足LTL的形式很有意思

  -> State: 1.1 <-window.switch = closeweather.rain = rainingweather.rainState = not_rainingrain_count = 1smoke = clearsmokeState = clearsmoke_count = 1runinwindow.timer = 0delaywindow = 0step = 1flag1 = TRUEflag2 = FALSEflag3 = TRUEflag4 = TRUEflag5 = FALSEflag6 = FALSE-> State: 1.2 <-weather.rainState = rainingrain_count = 0smoke_count = 0step = 2-> State: 1.3 <-weather.rain = not_rainingrain_count = 1smoke = detectedsmoke_count = 1step = 3-> State: 1.4 <-window.switch = openweather.rainState = not_rainingrain_count = 0smokeState = detectedsmoke_count = 0delaywindow = 5step = 4-> State: 1.5 <-runinwindow.timer = 5step = 5-> State: 1.6 <-runinwindow.timer = 4step = 0-> State: 1.7 <-runinwindow.timer = 3-> State: 1.8 <-runinwindow.timer = 2-> State: 1.9 <-smoke = clearsmoke_count = 1runinwindow.timer = 1flag1 = FALSEflag3 = FALSEflag4 = FALSEflag5 = TRUEflag6 = TRUE-- Loop starts here-> State: 1.10 <-smokeState = clearsmoke_count = 0runinwindow.timer = 0delaywindow = 0flag1 = TRUEflag3 = TRUEflag4 = TRUEflag5 = FALSEflag6 = FALSE-> State: 1.11 <-

rain1_1_fix2 冲突状态仍存在，是在下一状态变（因为先action），并没有像之前的消掉（因为后action） action要变

关键是找到没有close的raining而不是冲突状态，并不是说冲突状态导致LTL冲突，而是有rain一直没找到close

  -> State: 1.1 <-window.switch = closeweather.rain = rainingweather.rainState = not_rainingrain_count = 1smoke = clearsmokeState = clearsmoke_count = 1runinwindow.timer = 0delaywindow = 0step = 1flag1 = TRUEflag2 = FALSEflag3 = TRUEflag4 = TRUEflag5 = FALSEflag6 = FALSE-> State: 1.2 <-weather.rainState = rainingrain_count = 0smoke_count = 0step = 2-> State: 1.3 <-weather.rain = not_rainingrain_count = 1smoke = detectedsmoke_count = 1step = 3-> State: 1.4 <-window.switch = openweather.rainState = not_rainingrain_count = 0smokeState = detectedsmoke_count = 0delaywindow = 5step = 4-> State: 1.5 <-weather.rain = rainingrain_count = 1runinwindow.timer = 5step = 5-> State: 1.6 <-weather.rainState = rainingrain_count = 0runinwindow.timer = 4step = 0-> State: 1.7 <-weather.rain = not_rainingrain_count = 1runinwindow.timer = 3-> State: 1.8 <-weather.rainState = not_rainingrain_count = 0runinwindow.timer = 2-> State: 1.9 <-smoke = clearsmoke_count = 1runinwindow.timer = 1flag1 = FALSEflag3 = FALSEflag4 = FALSEflag5 = TRUEflag6 = TRUE-- Loop starts here-> State: 1.10 <-smokeState = clearsmoke_count = 0runinwindow.timer = 0delaywindow = 0flag1 = TRUEflag3 = TRUEflag4 = TRUEflag5 = FALSEflag6 = FALSE-> State: 1.11 <-

  -> State: 1.1 <-window.switch = closeweather.rain = rainingweather.rainState = not_rainingrain_count = 1smoke = clearsmokeState = clearsmoke_count = 1runinwindow.timer = 0delaywindow = 0step = 1flag1 = TRUEflag2 = FALSEflag3 = TRUEflag4 = TRUEflag5 = FALSEflag6 = FALSE-> State: 1.2 <-weather.rainState = rainingrain_count = 0smoke_count = 0step = 2-> State: 1.3 <-weather.rain = not_rainingrain_count = 1smoke = detectedsmoke_count = 1step = 3-> State: 1.4 <-window.switch = openweather.rainState = not_rainingrain_count = 0smokeState = detectedsmoke_count = 0delaywindow = 5step = 4-> State: 1.5 <-weather.rain = rainingrain_count = 1runinwindow.timer = 5step = 5-> State: 1.6 <-window.switch = closeweather.rainState = rainingrain_count = 0runinwindow.timer = 4step = 0-> State: 1.7 <-weather.rain = not_rainingrain_count = 1runinwindow.timer = 3-> State: 1.8 <-weather.rainState = not_rainingrain_count = 0runinwindow.timer = 2-> State: 1.9 <-runinwindow.timer = 1-- Loop starts here-> State: 1.10 <-runinwindow.timer = 0delaywindow = 0-> State: 1.11 <-

rain1_2 任务：找没有close匹配的raining

所以是1.10而不是1.1，step=10

  -> State: 1.1 <-window.switch = openweather.rain = rainingweather.rainState = not_rainingrain_count = 1smoke = clearsmokeState = clearsmoke_count = 1runinwindow.timer = 0delaywindow = 0-> State: 1.2 <-weather.rainState = rainingrain_count = 0smoke_count = 0-> State: 1.3 <-weather.rain = not_rainingrain_count = 1smoke = detectedsmoke_count = 1-> State: 1.4 <-weather.rainState = not_rainingrain_count = 0smokeState = detectedsmoke_count = 0-> State: 1.5 <-weather.rain = rainingrain_count = 1-> State: 1.6 <-window.switch = closeweather.rainState = rainingrain_count = 0smoke = clearsmoke_count = 1-> State: 1.7 <-weather.rain = not_rainingrain_count = 1smokeState = clearsmoke_count = 0-> State: 1.8 <-weather.rainState = not_rainingrain_count = 0smoke = detectedsmoke_count = 1-> State: 1.9 <-window.switch = opensmokeState = detectedsmoke_count = 0delaywindow = 5-> State: 1.10 <-weather.rain = rainingrain_count = 1smoke = clearsmoke_count = 1runinwindow.timer = 5-> State: 1.11 <-weather.rainState = rainingrain_count = 0smokeState = clearsmoke_count = 0runinwindow.timer = 4-> State: 1.12 <-weather.rain = not_rainingrain_count = 1runinwindow.timer = 3-> State: 1.13 <-weather.rainState = not_rainingrain_count = 0runinwindow.timer = 2-> State: 1.14 <-smoke = detectedsmoke_count = 1runinwindow.timer = 1-- Loop starts here-> State: 1.15 <-smokeState = detectedsmoke_count = 0runinwindow.timer = 0delaywindow = 0-> State: 1.16 <-

rain1_2_fix1

flag1 = TRUE
flag2 = FALSE
flag3 = TRUE
flag4 = FALSE
flag5 = TRUE
flag6 = FALSE

rain1_1_fix3 冲突状态

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

  -> State: 1.1 <-window.switch = closeweather.rain = rainingweather.rainState = not_rainingrain_count = 1smoke = clearsmokeState = clearsmoke_count = 1runinwindow.timer = 0delaywindow = 0step = 1flag1 = TRUEflag2 = FALSEflag3 = TRUEflag4 = FALSEflag5 = FALSEflag6 = FALSE-> State: 1.2 <-weather.rainState = rainingrain_count = 0smoke_count = 0step = 2-> State: 1.3 <-weather.rain = not_rainingrain_count = 1smoke = detectedsmoke_count = 1step = 3-> State: 1.4 <-window.switch = openweather.rainState = not_rainingrain_count = 0smokeState = detectedsmoke_count = 0delaywindow = 5step = 4-> State: 1.5 <-weather.rain = rainingrain_count = 1runinwindow.timer = 5step = 5-> State: 1.6 <-weather.rainState = rainingrain_count = 0runinwindow.timer = 4step = 0-> State: 1.7 <-weather.rain = not_rainingrain_count = 1runinwindow.timer = 3-> State: 1.8 <-weather.rainState = not_rainingrain_count = 0runinwindow.timer = 2-> State: 1.9 <-weather.rain = rainingrain_count = 1runinwindow.timer = 1-- Loop starts here-> State: 1.10 <-weather.rainState = rainingrain_count = 0runinwindow.timer = 0delaywindow = 0-> State: 1.11 <-

rain1_1_fix4 冲突状态

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

  -> State: 1.1 <-window.switch = closeweather.rain = rainingweather.rainState = not_rainingrain_count = 1smoke = clearsmokeState = clearsmoke_count = 1runinwindow.timer = 0delaywindow = 0step = 1flag1 = TRUEflag2 = FALSEflag3 = TRUEflag4 = FALSEflag5 = TRUEflag6 = FALSE-> State: 1.2 <-weather.rainState = rainingrain_count = 0smoke_count = 0step = 2-> State: 1.3 <-weather.rain = not_rainingrain_count = 1smoke = detectedsmoke_count = 1step = 3-> State: 1.4 <-window.switch = openweather.rainState = not_rainingrain_count = 0smokeState = detectedsmoke_count = 0delaywindow = 5step = 4-> State: 1.5 <-weather.rain = rainingrain_count = 1runinwindow.timer = 5step = 5-> State: 1.6 <-weather.rainState = rainingrain_count = 0runinwindow.timer = 4step = 0-> State: 1.7 <-weather.rain = not_rainingrain_count = 1runinwindow.timer = 3-> State: 1.8 <-weather.rainState = not_rainingrain_count = 0runinwindow.timer = 2-> State: 1.9 <-weather.rain = rainingrain_count = 1smoke = clearsmoke_count = 1runinwindow.timer = 1-- Loop starts here-> State: 1.10 <-weather.rainState = rainingrain_count = 0smokeState = clearsmoke_count = 0runinwindow.timer = 0delaywindow = 0-> State: 1.11 <-

rain1_1_fix5

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

rain1_1_fix6

NuSMV > check_ltlspec -p "G((weather.rain=raining)->F(window.switch=close))"
-- specification  G (weather.rain = raining ->  F window.switch = close)  is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample-> State: 1.1 <-window.switch = closewindowSwitchState = closeweather.rain = rainingrain_count = 0smoke = clearsmoke_count = 0alarm.alarmCap.alarm = bothalarmState = offruninalarm.timer = 0delayalarm = 0runinwindow.timer = 0delaywindow = 0-> State: 1.2 <-smoke = detectedsmoke_count = 1alarmState = both-> State: 1.3 <-window.switch = opensmoke_count = 0alarm.alarmCap.alarm = sirendelayalarm = 3delaywindow = 5-> State: 1.4 <-windowSwitchState = openweather.rain = not_rainingrain_count = 1alarmState = sirenruninalarm.timer = 3runinwindow.timer = 5-> State: 1.5 <-rain_count = 0runinalarm.timer = 2runinwindow.timer = 4-> State: 1.6 <-runinalarm.timer = 1runinwindow.timer = 3-> State: 1.7 <-runinalarm.timer = 0delayalarm = 0runinwindow.timer = 2-> State: 1.8 <-runinwindow.timer = 1-- Loop starts here-> State: 1.9 <-runinwindow.timer = 0delaywindow = 0-> State: 1.10 <NuSMV > check_ltlspec -p "G((weather.rain=raining)->!F(window.switch=close))"
-- specification  G (weather.rain = raining -> !( F window.switch = close))  is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample-> State: 1.1 <-window.switch = closewindowSwitchState = closeweather.rain = rainingrain_count = 0smoke = clearsmoke_count = 0alarm.alarmCap.alarm = bothalarmState = offruninalarm.timer = 0delayalarm = 0runinwindow.timer = 0delaywindow = 0flag1 = TRUEflag2 = FALSEflag3 = TRUEflag4 = FALSEflag5 = TRUEflag6 = FALSEflag7 = FALSEflag8 = FALSEflag9 = TRUEflag10 = FALSE-> State: 1.2 <-weather.rain = not_rainingrain_count = 1smoke = detectedsmoke_count = 1alarmState = both-> State: 1.3 <-window.switch = openrain_count = 0smoke_count = 0alarm.alarmCap.alarm = sirendelayalarm = 3delaywindow = 5-> State: 1.4 <-windowSwitchState = openalarmState = sirenruninalarm.timer = 3runinwindow.timer = 5-> State: 1.5 <-runinalarm.timer = 2runinwindow.timer = 4-> State: 1.6 <-runinalarm.timer = 1runinwindow.timer = 3-> State: 1.7 <-runinalarm.timer = 0delayalarm = 0runinwindow.timer = 2-> State: 1.8 <-runinwindow.timer = 1-- Loop starts here-> State: 1.9 <-runinwindow.timer = 0delaywindow = 0-> State: 1.10 <-
NuSMV >-- specification  G (weather.rain = raining ->  F window.switch = close)  is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample-> State: 1.1 <-window.switch = closewindowSwitchState = closeweather.rain = rainingrain_count = 1smoke = clearsmoke_count = 1alarm.alarmCap.alarm = bothalarmState = offruninalarm.timer = 0delayalarm = 0runinwindow.timer = 0delaywindow = 0step = 1flag1 = TRUEflag2 = FALSEflag3 = TRUEflag4 = FALSEflag5 = TRUEflag6 = FALSEflag7 = FALSEflag8 = FALSEflag9 = TRUEflag10 = FALSE-> State: 1.2 <-rain_count = 0smoke_count = 0alarmState = bothstep = 2flag3 = FALSEflag4 = TRUEflag9 = FALSEflag10 = TRUE-> State: 1.3 <-window.switch = opensmoke = detectedsmoke_count = 1alarm.alarmCap.alarm = offdelaywindow = 5step = 3flag3 = TRUEflag4 = FALSEflag9 = TRUEflag10 = FALSE-> State: 1.4 <-windowSwitchState = openweather.rain = not_rainingrain_count = 1smoke_count = 0alarm.alarmCap.alarm = sirenalarmState = offdelayalarm = 3runinwindow.timer = 5-> State: 1.5 <-rain_count = 0alarmState = sirenruninalarm.timer = 3runinwindow.timer = 4-> State: 1.6 <-runinalarm.timer = 2runinwindow.timer = 3-> State: 1.7 <-runinalarm.timer = 1runinwindow.timer = 2-> State: 1.8 <-runinalarm.timer = 0delayalarm = 0runinwindow.timer = 1-- Loop starts here-> State: 1.9 <-runinwindow.timer = 0delaywindow = 0-> State: 1.10 <-
NuSMV >BUG LOCATION 继续弄

考虑如下智能家居场景，用户家中有以下智能设备：温湿度传感器、人体传感器、烟雾传感器、智能灯、智能窗户、智能报警器、智能风扇。为了实现智能家居自动化，设置如下X条TAP规则：1）IF 烟雾传感器检测到烟雾，THEN 智能报警器报警；2）IF 烟雾传感器检测到烟雾，THEN 打开智能窗户10min后关闭；3）IF 烟雾传感器检测到烟雾，THEN 打开智能风扇10min后关闭；4）IF 室内环境潮湿，THEN 打开智能风扇10min后关闭；