同時にに変数の値を変える nusmv コード

MODULE main
 VAR
  var1 : boolean;
  var2 : boolean;

 ASSIGN
  init(var1) := TRUE;
  next(var1) := case
    TRUE : {TRUE, FALSE};
  esac;
  init(var2) := TRUE;
  next(var2) := case
    TRUE : {TRUE, FALSE};
  esac;

実行例

NuSMV > go
NuSMV > pick_state -r
NuSMV > print_current_state -v
Current state is 1.1
var1 = TRUE
var2 = TRUE
NuSMV > simulate -r -k 10
********  Simulation Starting From State 1.1   ********
NuSMV > show_traces -t
There is 1 trace currently available.
NuSMV > show_traces -v
<!-- ################### Trace number: 1 ################### -->
Trace Description: Simulation Trace
Trace Type: Simulation
-> State: 1.1 <-
      var1 = TRUE
      var2 = TRUE
-> State: 1.2 <-
      var1 = FALSE
      var2 = TRUE
-> State: 1.3 <-
      var1 = FALSE
      var2 = TRUE
-> State: 1.4 <-
      var1 = FALSE
      var2 = FALSE
-> State: 1.5 <-
      var1 = TRUE
      var2 = FALSE
-> State: 1.6 <-
      var1 = FALSE
      var2 = FALSE
-> State: 1.7 <-
      var1 = FALSE
      var2 = TRUE
-> State: 1.8 <-
      var1 = FALSE
      var2 = TRUE
-> State: 1.9 <-
      var1 = FALSE
      var2 = TRUE
-> State: 1.10 <-
      var1 = TRUE
      var2 = TRUE
-> State: 1.11 <-
      var1 = FALSE
      var2 = FALSE
NuSMV >