NuSMV中IVAR与VAR的反例差异解析请求

Let's break down the key differences between VAR and IVAR in NuSMV, and why their counterexamples look so drastically different using your examples.

First: Core Difference Between VAR and IVAR #

• VAR (State Variables): NuSMV has full control over these variables. When generating a counterexample, it produces a concrete sequence of states because it can directly choose values for these variables to violate the property in the shortest way possible.
• IVAR (Input Variables): These represent external inputs controlled by the environment, not NuSMV. NuSMV's job is to verify that the property holds no matter what inputs the environment chooses. When a property is violated, the counterexample shows that there exists at least one sequence of environment inputs that causes the system to break the property.

Your VAR Example: Straightforward State Sequence #

Your VAR code defines all variables as state-controlled:

MODULE main 
VAR 
  v1: 0..20; 
  v2: 0..20; 
  v3: 0..100; 
INIT v3 = 0; 
TRANS ((v2+v1 = 0) -> (next(v3) = 10)) & (!(v2+v1 = 0) -> (next(v3) = v1 + v2)) 
LTLSPEC G(v3 = 10); 

The counterexample is a clear, linear sequence of states because NuSMV picks values for v1 and v2 to show exactly how v3 can deviate from 10:

Trace Type: Counterexample 
-> State: 1.1 <- v1 = 0 v2 = 0 v3 = 0 
-- Loop starts here 
-> State: 1.2 <- v3 = 10 
-> State: 1.3 <- v1 = 7 v2 = 6 
-> State: 1.4 <- v1 = 0 v2 = 0 v3 = 13 
-> State: 1.5 <- v3 = 10 

Here, NuSMV chooses v1=7, v2=6 to make v3=13 (violating G(v3=10)), then loops back to reset v3 to 10. It's a simple, concrete path because NuSMV controls all variables.

Your IVAR Example: Nested Loops Explained #

When you switch v1 and v2 to IVAR, they become environment-controlled inputs:

MODULE main 
IVAR 
  v1: 0..20; 
  v2: 0..20; 
VAR 
  v3: 0..100; 
INIT v3 = 0; 
TRANS ((v2+v1 = 0) -> (next(v3) = 10)) & (!(v2+v1 = 0) -> (next(v3) = v1 + v2)) 
LTLSPEC G(v3 = 10); 

The counterexample looks confusing with nested loops, but here's what it means:

Trace Type: Counterexample 
-> State: 1.1 <- v3 = 0 
-> Input: 1.2 <- v1 = 7 v2 = 3 
-- Loop starts here 
-> State: 1.2 <- v3 = 10 
-> Input: 1.3 <- -- Loop starts here 
-> State: 1.3 <- 
-> Input: 1.4 <- -- Loop starts here 
-> State: 1.4 <- 
-> Input: 1.5 <- -- Loop starts here 
-> State: 1.5 <- 
-> Input: 1.6 <- -- Loop starts here 
-> State: 1.6 <- 
-> Input: 1.7 <- 
-> State: 1.7 <- 

Why the Nested Loops? #

1. Alternating State-Input Structure: IVAR counterexamples follow a State → Input → State → Input pattern. Each Input block represents a choice the environment makes, and the State block is how the system responds to that input.
2. Environment Non-Determinism: The nested loops indicate that the environment has unlimited choices at each step. For example, once the system reaches State:1.2 (v3=10), the environment can choose any input values for v1 and v2—not just the ones shown. The loops mean: "The environment can keep choosing inputs that will eventually make v3 ≠ 10, violating the property".
3. Minimal Counterexample for Non-Determinism: NuSMV doesn't need to show every possible input (there are infinitely many). Instead, it uses loops to represent that the environment can repeat a choice (or choose any value) to break the property. The empty input blocks mean "the environment can choose any valid values here—we don't need to specify exactly which ones, just that such values exist".

In short: The nested loops are NuSMV's way of showing that the environment has the power to choose inputs that violate the property, and it can do this indefinitely.

内容的提问来源于stack exchange，提问作者Montserrat Hermo