incorrect accepting states #14
Description
it seems that the initial states are computed incorrectly as being all states, when the CTL spec is true everywhere. minimal example:
primes = PyBoolNet.Repository.get_primes("raf")
update = "asynchronous"
init = "INIT !Raf"
spec = "CTLSPEC TRUE"
res, acc = PyBoolNet.ModelChecking.check_primes_with_acceptingstates(primes, update, init, spec)
print acc["INIT"], acc["INIT_SIZE"]
gives TRUE, 8 but !(Raf), 4 would be correct.
NuSMV is probably lazy (i.e. efficient) and trivial specs are caught without constructing BDDs.
suggested fix for next version: ModelChecking.check_primes_with_acceptingstates(..) will test whether the ctl spec is trivial (either TRUE or FALSE) and in that case set the keywords INIT and INIT_SIZE from the accepting states dictionary to None.