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
This is not a bug report but a support request.