I am trying to check whether this predicate holds within a hierarchical Petri Net model, but I got an error shown in the picture.
The predicate:
fun start n = (Mark.coin'sender 1 n= [("0X00A",50)]
andalso Mark.coin'start 1 n= [("0X00C",0)]
andalso Mark.coin'minter 1 n= []
andalso Mark.coin'receiver 1 n= [("0X00B",0)]
andalso Mark.coin'caller 1 n= [("0X00D",20)]
andalso Mark.coin'coin_m 1 n= []
andalso Mark.coin'Tx 1 n= []
andalso Mark.coin'error 1 n= []);
fun goal n = (Mark.coin'sender 1 n= []
andalso Mark.coin'start 1 n= [("0X00C",0)]
andalso Mark.coin'minter 1 n= []
andalso Mark.coin'receiver 1 n= [("0X00B",0)]
andalso Mark.coin'caller 1 n= [("0X00D",20)]
andalso Mark.coin'coin_m 1 n= []
andalso Mark.coin'Tx 1 n= []
andalso Mark.coin'error 1 n= []);
val myASKCTLformula=MODAL(INV(OR(NF("start", start),EV(NF("goal", goal)))));
eval_node myASKCTLformula InitNode;
- Badges
- Science topic
- Similar topics
- Mathematical Sciences
- Graphs