Changes between Version 14 and Version 15 of MoMoC

Timestamp:

Jan 26, 2020, 9:51:10 PM (5 years ago)

Author:

5willrod

Comment:

--

MoMoC

@@ -46 +46 @@
 || || !NetInstanceForall || !(''Arg'', ''!InstancePredicate'') || !(NetA, m(p1) > 0) ||
 || || !NetInstanceExists || ?(''Arg'', ''!InstancePredicate'') || ?(NetB, m(p2) = 4) ||
-|| || !InstancePredicate || m(''Arg'') ''Op'' ''Number'' || m(p3) <= 1 ||
+||= Other =|| !InstancePredicate || m(''Arg'') ''Op'' ''Number'' || m(p3) <= 1 ||
 || || Op || =, >, <, >=, <= || ||
 || || Arg || [A-Za-z0-9]+ || ||
@@ -58 +58 @@
 
 AG !(NetB, m(p1) <= 5) : ''"On all paths, globally, all net instances of net template NetB have at least 5 tokens on their place p1"''
+
+ 
+
+''Why does the formula EG(m(p)=1) throw a syntax error?''
+
+m(p)=1 is not a valid atomic proposition. Because MoMoC is designed for reference nets, all predicates that refer to a place must be nested into a ''net instance quantifier'' to avoid ambiguity. 
+
 
 === Atomic Propositions: Semantics