I’m trying to make a query on a state space. The idea is “if some situation happens in one state then later another situation must happen”. Simplified case is
fun f1 n = (n=2);
fun f2 n = (n=5);
val myASKCTLformula = POS(AND(NF("f1", f1), EV(NF("f2", f2))));
eval_node myASKCTLformula 1;
I expected false because 5-th state is not reachable from the 2-nd but got an error.
CPN Tools v. 3.4.0, Windows 7 Home x64
You must be logged in to post a comment.