Model checking has problems when the initial value of an integer port is out-of-range
this caused the problem in the model of Zhu Peng
(from redmine: issue id 879, created on 2012-06-26, closed on 2012-07-07)
this caused the problem in the model of Zhu Peng
(from redmine: issue id 879, created on 2012-06-26, closed on 2012-07-07)