I have an asynchronous symmetric ring-shaped protocol with 5 processes that satisfies a given property. I want to prove (or get counterexample) that the property is true for protocols with 6 number of processes and more; that is
∀n.φ(n)
I decided to use assume-guarantee and I’m using nuSMV for model-checking.
I know that former versions of SMV like Cadence could support this feature but is there any way to implement assume-guarantee in nuSMV?
If there is not, could I use other model checkers like SPIN instead?
Thank you.
