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:

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: 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: