Help

Welcome to CMCV, CTL Model Checking Visualizer!

Model checking is an automatic model-based property-verification approach to verification of computer systems by using transition systems and temporal logic. The system to verify has to be translated in a formal model called transition system. An example of a temporal logic is Computation Tree Logic, or CTL for short. The algorithm used to do CTL model checking here is the labeling algorithm. If you want to read more about CTL model checking, please consider the book Logic in Computer Science written by Michael Huth and Mark Ryan.

Throughout this page, the following syntax notation is used:

• | separates alternatives
• "" surround literals
• () specifies grouping
• [a-z] means one character in the interval from a to z (any lower case letter)
• [abc] means one character of those between the brackets
• ? means 0 times or 1 time
• * means 0 or more times
• \ escapes special characters in literals

CMCV visualizes the steps involved for CTL model checking for better understanding. It is divided into three panels:

Transition System

Here the current transition system is displayed as a directed graph. The nodes correspond to states and the links correspond to transitions. You have several options:

• Choose Example
  Use this combo box to load some predefined example.
• Filename
  If you want to save your transition system, you can enter a filename for it.
• Load
  You can open a file containing a JSON description of a transition system. Such a file can either be produced by CMCV, or written manually by the user. If your browser does not support file uploads, you can use the Edit button and paste in some JSON string.
• Save
  Save the current transition system into a JSON file on your file system. Note that your current transition system is stored automatically in your browser, but if you want share one transition system on many browsers or devices, or you want to manage many transition systems in one browser, this option might be useful. If for any reason you cannot save files to your file system, you can use the Edit button and copy the displayed text to your clipboard.
• Edit
  Directly edit the JSON representation of the current transition system. This can be useful for browsers which do not support one of the two previous options.
• Notes
  This is the right spot to place any explanatory notes for your transition system. If you save your transition system, these notes will be saved with it. Also, after choosing an example, read these notes to understand the intention of that transition system.
• Layout Graph automatically
  Select this option to apply a force layout to the graph. A gravitational center will attract the nodes towards it. The nodes repulse each other, and the links try to have a certain fixed distance. This layout is rather CPU expensive. Also, if dealing with a large number of states and transitions, it will not give the best results.
• Automatic Zoom
  CMCV always tries to keep the whole graph visible by changing its size.
• Nodes
  The upper text label in a node is the id or name of the state, while the lower one is called the labels of this state, i.e. the atoms it is labeled with. With nodes you can do the following things.
  • Create a node by clicking on free space while nothing is selected.
  • Select a node by clicking on it. Once you have selected a node, you have more options.
  • Move around a node by dragging it. Note that it depends on whether you use Layout Graph Automatically and/or Automatic Zoom what happens after releasing the node.
  • Change the id of a selected node by clicking on it.
  • Change the labels of a selected node by clicking on them. They are separated by comma and/or whitespaces.
  • Make a self-loop at a selected node by clicking on the yellow button.
  • Make a link from a selected node to another by clicking on the orange button first and on the target node afterwards.
  • Remove a selected node by clicking on the red button.
• Links
  Links cannot be dragged but selected. To learn how they can be made, see Nodes. Selected links offer an orange button for bending and a red button for removing them. Loops also provide a third, yellow button for changing the loops position, where N, E, S, W mean north, east, south and west, respectively, and A means automatically, which is to point away from the center.

The JSON representation of transition systems must be in the following format:

    system:
        "{" sysCore ("," sysNotes)? "}"
    sysCore:
        "\"states\"" ":" states "," "\"transitions\"" ":" transitions
    sysNotes:
    	"\"notes\"" ":" string
    states:
        "[" stateList? "]"
    stateList:
        state ("," state)*
    state:
        "{" stateCore ("," statePos)? "}"
    stateCore:
        "\"id\"" ":" string "," "\"labels\"" ":" labels
    statePos:
        "\"x\"" ":" number "," "\"y\"" ":" number
    labels:
        "[" labelList? "]"
    labelList:
        string ("," string)*
    transitions:
        "[" transitionList? "]"
    transitionList:
        transition ("," transition)*
    transition:
        "[" string "," string "]"
        | "{" transitionCore ("," bend)? ("," loopDir)? "}"
    transitionCore:
        "\"source\"" ":" string "," "\"target\"" ":" string
    bend:
        "\"bend\"" ":" (string | boolean)
    loopDir:
        "\"loopDir\"" ":" string
	

Here number and string can be any JSON number and string, respectively, except that any string must be non-empty. Additionally, tokens can be separated by arbitrary many whitespaces. If a JSON representation of a transition system specifies keys other than those above, they are ignored.

Note that the statePos rule for specifying x- and y-coordinates is optional. If not all states specify a position, the option "Layout Graph Automatically" is activated in order to determine positions for all nodes.

An edge representing a transition s → t without bend is bent to the left if t → s also exists, and goes straight otherwise. If bend is "r"" or "right" (case insensitive), the edge is bent to the right, while for any other truthy value the edge is bent to the left. Moreover, the loopDir option can be used for specifying the orientation of loops with the (case insensitive) values "n" or "north", "e" or "east", "s" or "south" and "w" or "west". If no loopDir is specified, the loop points away from the center.

The sysNotes rule is also optional. If you omit this rule, the notes are considered to be empty.

Formula

Here you can type in a CTL formula. The expected syntax is as follows:

    formula:
        disjunctive ("->" formula)?
	
    disjunctive:
        conjunctive ("|" disjunctive)?
	
    conjunctive:
        unary ("&" conjunctive)?
	
    unary:
        "B"                               
        | "T"                             
        | [a-z][a-z0-9_]*     
        | "!" unary
        | "EX" unary
        | "AX" unary
        | "EF" unary
        | "AF" unary
        | "EG" unary
        | "AG" unary
        | "E[" formula "U" formula "]"
        | "A[" formula "U" formula "]"
        | "(" formula ")"
	

So the binding is -> < | < & < unary. All symbols can be separated by arbitrary many spaces.
The three first alternatives of unary, respectively, represent ⊥, ⊤ and an atom. The latter contains lower case letters, digits or underscores and begins with a lower case letter.

Furthermore, you can check "use adequate set of connectives" to automatically translate your input formula in an equivalent formula using only the connectives ⊥, ¬, ∧, EX, AF and EU.

Press enter or click run algorithm to start the labeling algorithm with the current transition system and the formula you specified.

Labeling Algorithm

This panel is visible only if you started the algorithm in the Formula Panel. A table will be displayed, where columns correspond to subformulas of your input and rows correspond to states in the transition system. This is where the labeling algorithm operates. You can navigate through its steps using the buttons clear, prev, next and solve, or by clicking on a table cell to see the first step considering whether to label this cell or not.
Below you find the definition of how labeling states with the current subformula is done, which is what CMCV tries to explain. Hover the abstract symbols to highlight the corresponding elements in the table and the graph.

To explain the current step, the following highlighting is used in the table:

current	The cell we think about whether to label or not.
good	Votes for labeling the current cell, but loses in the end.
bad	Votes for not labeling the current cell, but loses in the end.
good critical	Votes for labeling the current cell and wins.
bad critical	Votes for not labeling the current cell and wins.
some/or	Some cell with a green border must be labeled in order to label the current cell. In other words, green wins here.
every/and	Every cell with a red border must be labeled in order to label the current cell. In other words, red wins here.
result	After executing the very last step, the states satisfying the given formula are highlighted this way.

A cell with a black bold border is not quantified, hence always "critical". Note that there are formulas (namely EU and AU), where a single step involves quantified and not quantified cells. In such a case, the highlighting is done separately in two groups, meaning that the colors of the quantified cells has nothing to do with the not quantified cell, and vice-versa. In the end, labeling is done only if green wins in both groups.

Similarly to the table, the algorithm is explained also in the graph with the following differences:

• The node corresponding to the current state is the dashed circle.
• If the current formula is an atom, it is searched in the labels of the current node. If contained, it is displayed in green while the other atoms are red.
• Quantification over successors is indicated by the stroke color of the corresponding links and circles.
• Only successors are filled with the corresponding color for good, bad, critical etc., because everything else is better explained in the table.
• If a state is definitely not considered anymore by the current subformula, its corresponding node is shown grayed.