Changes between Version 9 and Version 10 of MoMoC

Timestamp:

Jan 12, 2020, 10:07:03 PM (5 years ago)

Author:

5willrod

Comment:

--

MoMoC

@@ -8 +8 @@
 This makes it easy to test out new algorithms or data-structures, as only the corresponding module needs to be replaced. 
 
-The foundation of MoMoC is the [/wiki/ReferenceNetsReachabilityGraph RNRG] plugin, whose key functionality (creating a reachability graph) can be accessed through the MoMoC Plugin.
+The foundation of MoMoC is the [/wiki/ReferenceNetsReachabilityGraph RNRG] plugin, whose key functionality (creating a reachability graph) can also be accessed through the MoMoC Plugin.
+For more detailed instructions on how to read MoMoC's reachability graphs, refer to [/wiki/ReferenceNetsReachabilityGraph RNRG].
+
+The rest of this page is split into a user guide and a developer guide.
+As the names suggest, the user guide explains usage and features of the MoMoC plugin, whereas the developer guide is addressed to anyone who wants to extend the plugin.
 
 == User Guide
@@ -14 +18 @@
 A detailed user guide will follow shortly.
 
+=== User Interface
+
+=== Syntax
+
+MoMoC follows the general syntax of CTL.
+The table below lists possible ways to write the boolean and temporal operators, as well as atomic propositions.
+The latter are further described below the table.
+
 p and q are state formulas, f is a path formula.
 
 ||= Category =||= Name =||= Allowed Variations =||= Syntax =||
-||= Boolean =|| True || TRUE, True || ||
+||= Boolean =|| True || TRUE, True || ||
 || || False || FALSE, False || ||
 || || Not || NOT, Not, ~, ¬ || (Not p) ||
@@ -37 +49 @@
 || || Number || ![0-9]+ || ||
 
+==== Examples
+
+AG (NOT DEADLOCK)
+
+(FIREABLE(T1) OR EX FIREABLE(T1))
+
+AG !(Net1, m(p1) <= 5)
+
+=== Atomic Propositions
+
+**Deadlock**: True, iff no transition is activated in a marking.
+
+**Fireable(T)**: True, iff T is activated in a marking. For root net transitions, it is sufficient to use the transition name as the parameter. For any other net instance, the syntax is !NetName.!TransitionName
+
+**!NetInstanceForall**: True, iff the instance predicate is true in all instances of the given type. 
+
+**!NetInstanceExists**: True, iff the instance predicate is true in at least one instance of the given type.
+
+**!InstancePredicate**: True if the total number of tokens in a place fulfills the given expression. Does not distinguish between token types.
+
+=== Results
+
 == Developer Guide