NuSMV - Issue with counter-based signal activation in Model

Question

I have a project for the Embedded System Design course where I need to model a fault-tolerant sensor reading mechanism. I have reduce the system to only the important parts. The system relies on error signal that indicates errors in measuring. The system tracks number of consecutive_errors, and an alarm is triggered after two consecutive errors.

Here is my current implementation in NuSMV:

MODULE main
VAR
 error : boolean;
 alarm : boolean; 
 consecutive_errors : 0..2;
ASSIGN
 init(alarm) := FALSE;
 init(consecutive_errors) := 0;
 -- Update consecutive error count
 next(consecutive_errors) := case
 !error : 0;
 error & consecutive_errors < 2 : consecutive_errors + 1;
 error & consecutive_errors = 2 : consecutive_errors;
 TRUE : 0; 
 esac;
 -- Activate alarm after two consecutive errors
 next(alarm) := case
 (consecutive_errors = 2) : TRUE;
 TRUE : alarm; 
 esac;
LTLSPEC !alarm -- LTL number 1
LTLSPEC G (alarm <-> (consecutive_errors = 2)) -- LTL number 2
LTLSPEC G (!error -> !alarm) -- LTL number 3

However, NuSMV reports that the last two LTL specifications are not satisfied. Here is the counterexample trace invalidating LTL number 2:

-- specification G (alarm <-> consecutive_errors = 2) is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
 -> State: 1.1 <-
 error = FALSE
 alarm = FALSE
 consecutive_errors = 0
 -> State: 1.2 <-
 error = TRUE
 -> State: 1.3 <-
 consecutive_errors = 1
 -> State: 1.4 <-
 error = FALSE
 consecutive_errors = 2
 -> State: 1.5 <-
 alarm = TRUE
 consecutive_errors = 0

As shown, the consecutive_errors counter reaches 2 in a step where the error is already cleared. Consequently, the alarm activates one step later, when no error is present, causing the LTL specifications to fail.

I tried modifying the alarm logic to activate immediately when consecutive_errors becomes 2, with the code:

next(alarm) := case
 (consecutive_errors = 1 & error) : TRUE; -- alarm is set after two consecutive errors
 TRUE : alarm; 
 esac;

but the same issue occurs. The model clears the error just before the alarm activates, violating the intended behavior.

The continuation of my project depends on this counter mechanism, and I need the model to behave accordingly.

Does anyone know how to fix this? Is the problem in the model or in my LTL specifications?

Thank you!