September 10, 2013

Mikhail shared this idea

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

November 5, 2013

Michael Westergaard (Code and Support Guy, CPN Tools) responded


This is not a bug report but a support request.

Clone ConstraintArcs
BendPoints on Declare constraints not being saved in CPN 4.0.0

You must be logged in to post a comment.