1

NuSMV で信号機システムの実装を作成しようとしています。現在、NS/EW 赤、黄、緑の 6 つのブール値があります。ただし、将来の状態でそれぞれが常に true であると指定すると、false が返されます。誰かが私のコードにエラーを見つけたら、助けていただければ幸いです。ありがとう。

MODULE main
VAR
    nsRed : boolean;
    nsYellow : boolean;
    nsGreen : boolean;

    time : 0..60;

    ewRed : boolean;
    ewYellow : boolean;
    ewGreen : boolean;
ASSIGN
    init(nsRed) := TRUE;
    init(nsYellow) := FALSE;
    init(nsGreen) := FALSE;
    init(ewRed) := FALSE;
    init(ewYellow) := FALSE;
    init(ewGreen) := TRUE;
    init(time) := 60;
next(nsRed) :=
    case
        (nsYellow = TRUE & (ewGreen = TRUE | ewYellow = TRUE) & time = 0) : TRUE;
        (nsRed = TRUE & time = 0) : FALSE;
        TRUE : nsRed;
    esac;
next(nsYellow) :=
    case
        (nsGreen = TRUE & ewRed = TRUE & time = 0) : TRUE;
        (nsYellow = TRUE & time = 0) : FALSE;
        TRUE : nsYellow;
    esac;
next(nsGreen) :=
    case
        (nsRed = TRUE & ewRed = TRUE & time = 0) : TRUE;
        (nsGreen = TRUE & time = 0) : FALSE;
        TRUE : nsGreen;
    esac;

next(ewRed) :=
    case
        (ewYellow = TRUE & (nsGreen = TRUE | nsYellow = TRUE) & time = 0) : TRUE;
        (ewRed = TRUE & time = 0) : FALSE;
        TRUE : ewRed;
    esac;
next(ewYellow) :=
    case
        (ewGreen = TRUE & nsRed = TRUE & time = 0) : TRUE;
        (ewYellow = TRUE & time = 0) : FALSE;
        TRUE : ewYellow;
    esac;
next(ewGreen) :=
    case
        (ewRed = TRUE & nsRed = TRUE & time = 0) : TRUE;
        (ewGreen = TRUE & time = 0) : FALSE;
        TRUE : ewGreen;
    esac;

next(time) :=
    case
        (time > 0) : time - 1;
        (time = 0 & nsRed = TRUE) : 60;
        (time = 0 & nsYellow = TRUE) : 60;
        (time = 0 & nsGreen = TRUE) : 3;
        (time = 0 & ewRed = TRUE) : 60;
        (time = 0 & ewYellow = TRUE) : 60;
        (time = 0 & ewGreen = TRUE) : 3;
        --(time = 0 & nsRed = TRUE & ewRed = TRUE) : 3
        TRUE : time;
    esac;

-- specification 
SPEC AG !(nsRed = TRUE & nsYellow = TRUE)
SPEC AG !(nsGreen = TRUE & nsRed = TRUE)
SPEC AG !(nsGreen = TRUE & ewGreen = TRUE)
SPEC AG !(nsYellow = TRUE & ewYellow = TRUE)
SPEC AG !(nsRed = TRUE & ewRed = TRUE)
SPEC AG (nsRed = TRUE | nsYellow = TRUE | nsGreen = TRUE | ewRed = TRUE | ewYellow = TRUE | ewGreen = TRUE)
--LTLSPEC F nsGreen = TRUE
LTLSPEC F ewGreen = TRUE
4

2 に答える 2

2

プロパティが false である理由は、決して true にならないF nsGreen = TRUE無限の実行が存在するためです。nsGreenこれは、NuSMV が生成する反例です (タイマーのカウント ダウンをカットしました)。変数の更新のみが出力されることに注意してください。

-- specification  F nsGreen = TRUE  is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
-> State: 1.1 <-
  nsRed = TRUE
  nsYellow = FALSE
  nsGreen = FALSE
  time = 60
  ewRed = FALSE
  ewYellow = FALSE
  ewGreen = TRUE
-> State: 1.2 <-
  time = 59
  ...
-> State: 1.61 <-
  time = 0
-> State: 1.62 <-
  nsRed = FALSE
  time = 60
  ewYellow = TRUE
  ewGreen = FALSE
-> State: 1.63 <-
  time = 59
  ...
-> State: 1.122 <-
  time = 0
-> State: 1.123 <-
  time = 60
  ewYellow = FALSE
-> State: 1.124 <-
  time = 59
  ...
-> State: 1.182 <-
  time = 1
-- Loop starts here
-> State: 1.183 <-
  time = 0
-> State: 1.184 <-

トレースはnsRed、タイマーが初めて 0 に達したときに既に false に設定されていることを示しています。また、ewYellowfalse になりますが、ewRedtrue には設定されません。

次のように、3 つのブール値ではなく、信号機に enum 変数を使用することをお勧めします。

MODULE main
VAR
    ns : {RED, YELLOW, GREEN};
    ew : {RED, YELLOW, GREEN};
于 2015-09-12T17:52:26.797 に答える