Forum Jar
Forum Jar : NuSMV Forum : new syntax in nuSMV
See other topics in NuSMV Forum

NuSMV Forum
Important rules for using NuSMV Forum
• No offensive words are allowed in this forum.
• To prevent spams, you must not use the words "http" ".com" or "/"(slashes) in this forum.

Alert! Please do not buy anything or pay anyone on this forum. Scammers have been reported on our forum. Please also do not go to any links posted on here. We have been reported about links to websites that contain viruses. Thank you.

Topic: new syntax in nuSMV
I wrote a nusmv code,a small part of my program is like this:
(hn1k2 & wrap_hn1k2 & extractable_hn1k1 & !k1Enck2 & next(k1Enck2) &
--unchanged vars
sensitive_hn1k2 = next(sensitive_hn1k2) &

(hn1k2 & wrap_hn1k2 & extractable_hn1k2 & !k2Enck2 & next(k2Enck2) &
--unchanged vars
hn1k1 = next(hn1k1) & hn1k2 = next(hn1k2) & k1 = next(k1)& k2 = next(k2) &
k1Enck2 = next(k1Enck2) &
k1Enck1 = next(k1Enck1) &
k2Enck1 = next(k2Enck1) &
in each state 1 or 2 variables change and other vars don't change, when i run it in guNusmv I saw that in some steps more than 1 var change for exampe 3 vars! is it mean that my program has semantic error?pls help me it's very important for me!!!

by guest Fri Jun 14 14:31:42 UTC 2013

by eduk8 Mon Aug 28 04:43:59 UTC 2017
Post a new comment

Name (optional):

By posting a comment, you indicate that you have agreed to our terms of use.

Feel adventurous? Check out random forums on Forum Jar!
Related Forums
Symbolic model verification Forum
Model checker Forum
Trento Forum
Italy Forum
Carnegie Mellon University Forum
University of Genoa Forum
University of Trento Forum
Binary Decision Diagrams Forum
Open source Forum
Boolean satisfiability problem Forum

sponsored links: free polls | free chat rooms (weirdtown chat) | widgets for myspace | make chat room | free chat room list | review websites | snowboard or ski | chat vocab

terms of use | privacy policy
©2011 All rights reserved.