FSM转NuSMV模型LTL属性验证存疑：返回True但有手动反例

Hey there, I've implemented a finite state machine (FSM) and written the corresponding NuSMV code to verify an LTL property. The target LTL property is:
G!(r1 & r2) -> (G(!g1 | !g2) & G(r1 -> F(g1)) & G(r2 -> F(g2)))

My NuSMV Code #

MODULE main
VAR
state : 0 .. 2;
r1 : boolean;
r2 : boolean;
g1 : boolean;
g2 : boolean;
ASSIGN
init (state) := 0;
init(r1) := FALSE;
init(r2) := FALSE;
init(g1) := FALSE;
init(g2) := FALSE;
next(state) := case
(state = 0) & (g1) & (r1) & (!r2) & (!g2) : 1;
(state = 1) & (g1) & (!r1) & (r2) & (g2) : 0;
(state = 0) & (!g1) & (!r1) & (!r2) & (!g2) : 0;
(state = 0) & (!g1) & (!r1) & (r2) & (g2) : 0;
(state = 0) & (g1) & (r1) & (r2) & (!g2) : 0;
(state = 1) & (g1) & (!r1) & (!r2) & (g2) : 1;
(state = 1) & (g1) & (r1) & (r2) & (!g2) : 1;
(state = 1) & (!g1) & (r1) & (!r2) & (!g2) : 1;
TRUE : state;
esac;
next(g1) := case
(state = 1) & (!r1) & (r2) & (g2) : TRUE;
(state = 0) & (!r1) & (!r2) & (!g2) : FALSE;
(state = 0) & (r1) & (!r2) & (!g2) : TRUE;
(state = 1) & (!r1) & (!r2) & (g2) : TRUE;
(state = 1) & (r1) & (!r2) & (!g2) : FALSE;
(state = 0) & (r1) & (r2) & (!g2) : TRUE;
(state = 1) & (r1) & (r2) & (!g2) : TRUE;
(state = 0) & (!r1) & (r2) & (g2) : FALSE;
TRUE : g1;
esac;
next(r1) := case
(state = 0) & (g1) & (!r2) & (!g2) : TRUE;
(state = 0) & (!g1) & (r2) & (g2) : FALSE;
(state = 1) & (!g1) & (!r2) & (!g2) : TRUE;
(state = 0) & (g1) & (r2) & (!g2) : TRUE;
(state = 1) & (g1) & (!r2) & (g2) : FALSE;
(state = 0) & (!g1) & (!r2) & (!g2) : FALSE;
(state = 1) & (g1) & (r2) & (!g2) : TRUE;
(state = 1) & (g1) & (r2) & (g2) : FALSE;
TRUE : r1;
esac;
next(r2) := case
(state = 0) & (g1) & (r1) & (!g2) : {TRUE, FALSE};
(state = 1) & (!g1) & (r1) & (!g2) : FALSE;
(state = 0) & (!g1) & (!r1) & (g2) : TRUE;
(state = 1) & (g1) & (!r1) & (g2) : {TRUE, FALSE};
(state = 1) & (g1) & (r1) & (!g2) : TRUE;
(state = 0) & (!g1) & (!r1) & (!g2) : FALSE;
TRUE : r2;
esac;
next(g2) := case
(state = 1) & (g1) & (r1) & (r2) : FALSE;
(state = 0) & (!g1) & (!r1) & (!r2) : FALSE;
(state = 1) & (g1) & (!r1) & (!r2) : TRUE;
(state = 0) & (g1) & (r1) & (!r2) : FALSE;
(state = 1) & (g1) & (!r1) & (r2) : TRUE;
(state = 1) & (!g1) & (r1) & (!r2) : FALSE;
(state = 0) & (!g1) & (!r1) & (r2) : TRUE;
(state = 0) & (g1) & (r1) & (r2) : FALSE;
TRUE : g2;
esac;

Verification Command & Result #

I ran the following model verification command in NuSMV's interactive mode:

NuSMV -int read_model -i test2.smv flatten_hierarchy encode_variables build_model pick_state -i check_ltlspec -p "G!(r1 & r2) -> (G(!g1 | !g2) & G(r1 -> F(g1)) & G(r2 -> F(g2)))"

NuSMV returned:

-- specification ( G !(r1 & r2) -> (( G (!g1 | !g2) & G (r1 -> F g1)) & G (r2 -> F g2))) is true

The Problem #

However, I've manually identified a counterexample to this property. I've gone through the NuSMV 2.6 user manual but still can't figure out where my code went wrong. Could someone help me troubleshoot this issue?

内容的提问来源于stack exchange，提问作者Ali Kianinejad