While experimenting with nuXmv and NuSMV model checkers, I observed that input variables contribute no state to the entire state-space of any given model.
The user manuals of these tools clearly mentioned syntactic differences between these kinds of variable. For example, the "IVAR" introduces the input variables paragraph; but "VAR" introduces state variables.
Is there any science behind this behavior of input variables? In particular, how do these model checkers handle input variables and state variables? Any reference on this observation will be appreciated.
Hi Yasir,
Thank you for the response. It is really appreciated.
But I have a couple of concerns. Let me assume that v3 is a state variable (i.e. declared in VAR paragraph), hence it can be initialized or have its value changed.
Did you observe that these input variables are limited compared to state variables in the sense that, they can't be initialized or manipulated within the system?
Did you try to encode v1 and v2 in VAR paragraph together with v3 and compute the state space using: NuSMV -r fileName.smv? You will have a result of the form (x out of y); where y is the total number of states.
For example, the following gives x = 41, y = 101 (i.e. 0..100)
MODULE main
IVAR
v1 : 0..20;
v2 : 0..20;
VAR
v3 : 0..100;
ASSIGN
init(v3) := 0;
next(v3) := case
v2 + v1 = 0 : 10;
TRUE : v2 + v1;
esac;
LTLSPEC !F(v3 = 0)
But by simply changing this to VAR, we have x = 18081, y = 44541
MODULE main
VAR
v1 : 0..20;
v2 : 0..20;
VAR
v3 : 0..100;
ASSIGN
init(v3) := 0;
next(v3) := case
v2 + v1 = 0 : 10;
TRUE : v2 + v1;
esac;
LTLSPEC !F(v3 = 0)
The difference reflects from the values of y. So my question is what makes IVAR behaves differently from VAR.
Thanks for you answer,
Opeyemi
Hi Yasir,
Here are my concerns:
MODULE main
-- this is an IVAR paragraph
IVAR
v1 : 0..20;
v2 : 0..20;
-- this is a VAR paragrapgh
VAR
v3 : 0..100;
ASSIGN
init(v3) := 0;
next(v3) := case
v2 + v1 = 0 : 10;
TRUE : v2 + v1;
esac;
LTLSPEC !F(v3 = 0)
But by simply changing this to VAR, we have x = 18081, y = 44541
MODULE main
-- this is a VAR paragraph
VAR
v1 : 0..20;
v2 : 0..20;
-- this is a VAR paragraph
VAR
v3 : 0..100;
ASSIGN
init(v3) := 0;
next(v3) := case
v2 + v1 = 0 : 10;
TRUE : v2 + v1;
esac;
LTLSPEC !F(v3 = 0)
The difference reflects from the values of y. So my question is what makes IVAR behaves differently from VAR.
Try to run the my code and compare the complexities. You should be able to know the difference. I would have modified you code but the restrictions on IVAR will not make it compile.
- Badges
- Science topic
- Similar topics
- Statistics
- Survey