Permalink
Browse files

Merge pull request #454 from cristian-mattarei/master

Fixed indexing and simple path condition in MC example
  • Loading branch information...
mikand committed Nov 3, 2017
2 parents 2d5d067 + 3207f2c commit 94983ab83eda0c1afd3f3806e52d43c4a08be719
Showing with 8 additions and 6 deletions.
  1. +8 −6 examples/model_checking.py
View
@@ -10,7 +10,7 @@
#
from six.moves import xrange
from pysmt.shortcuts import Symbol, Not, Equals, And, Times, Int, Plus, LE
from pysmt.shortcuts import Symbol, Not, Equals, And, Times, Int, Plus, LE, Or, EqualsOrIff
from pysmt.shortcuts import is_sat, is_unsat
from pysmt.typing import INT
@@ -51,7 +51,7 @@ def get_unrolling(system, k):
E.g. T(0,1) & T(1,2) & ... & T(k-1,k)
"""
res = []
for i in xrange(k):
for i in xrange(k+1):
subs_i = get_subs(system, i)
res.append(system.trans.substitute(subs_i))
return And(res)
@@ -62,19 +62,21 @@ def get_simple_path(system, k):
each time encodes a different state
"""
res = []
for i in xrange(k):
for i in xrange(k+1):
subs_i = get_subs(system, i)
for j in xrange(i+1, k):
for j in xrange(i+1, k+1):
state = []
subs_j = get_subs(system, j)
for v in system.variables:
v_i = v.substitute(subs_i)
v_j = v.substitute(subs_j)
res.append(Not(Equals(v_i, v_j)))
state.append(Not(EqualsOrIff(v_i, v_j)))
res.append(Or(state))
return And(res)
def get_k_hypothesis(system, prop, k):
"""Hypothesis for k-induction: each state up to k fulfills the property"""
"""Hypothesis for k-induction: each state up to k-1 fulfills the property"""
res = []
for i in xrange(k):
subs_i = get_subs(system, i)

0 comments on commit 94983ab

Please sign in to comment.