On the picture below you can see the screenshot of the MGE applet.
To get the model graph of this program just push the Run button. The model graph of the program will be displayed in the lower panel of the applet.
The model graph is placed using the circle layout. You can use however the Options button to open the options dialog box and to change the circle layout by the grid layout. Also, you can use mouse drag and drop actions to place the nodes of the graph manually.
The buttons with the labels <== and ==> can be used to navigate through the text area buffers, e.g. to look for log messages.

/* The sequential circuit example, Anatol Ursu, 2010 Given the sequential circuit: x1 . ..  .'.  `1  .. r0  .. r1  MUX  R1 ' R2  y0 x0 0  `' `' `' This circuit contains a MUX and two registers, R1 and R2. The PTTF program of this circuit is presented at the end of this file. The satisfiability analysis of this program by MGE tool will produce a model graph that accepts all sequences of states satisfying the program. To run this program and to view the model graph push the buttons:  "Run" or  "Compile" and "Place" Note: Use mouse drag and drop to place the nodes of the graph manually. Use "==>" and "<==" buttons to look for log messages. */ //The PTTF program starts below this line /*====================================================*/ Module SeqCircuit(x0, x1, y0) Input x0, x1; Output y0; Begin //The initial state of the registers !r0 ^ !r1; //The two formulas describe the register r0 [](((!x1 ^ x0)  (x1 ^ r0)) => @(r0)); [](!(((!x1 ^ x0)  (x1 ^ r0))) => @(!r0)); //These two formulas describe the register r1 [](r0 => @(r1)); [](!r0 => @(!r1)); //This formula is a way to say that r1 and y0 are interconnected, i.e. they are equivalent []equiv(r1, y0); End 
% Graphplace representation of the PTTF model graph. % This is an automatically generated file by MGE tool, v. 0.2. () () 5 node % !r0 !r1 !x1 x0 !y0 % % (0/5) () 5 1 edge (0/5) () 5 9 edge () () 9 node % r0 !r1 !x1 !x0 !y0 % % (0/9) () 9 7 edge (0/9) () 9 17 edge (@i) () () 3 node % !r0 !r1 !x1 !x0 !y0 % !r0 !r1 x1 !y0 % % (0/3) () 3 0 edge (0/3) () 3 5 edge () () 13 node % r0 r1 !x1 x0 y0 % r0 r1 x1 y0 % % (0/13) () 13 11 edge (0/13) () 13 13 edge () () 1 node % r0 !r1 !x1 x0 !y0 % r0 !r1 x1 !y0 % % (0/1) () 1 11 edge (0/1) () 1 13 edge () () 17 node % !r0 r1 !x1 !x0 y0 % !r0 r1 x1 y0 % % (0/17) () 17 0 edge (0/17) () 17 5 edge () () 11 node % r0 r1 !x1 !x0 y0 % % (0/11) () 11 7 edge (0/11) () 11 17 edge (@i) () () 15 node % !r0 !r1 !x1 x0 !y0 % % (0/15) () 15 1 edge (0/15) () 15 9 edge () () 0 node % !r0 !r1 !x1 !x0 !y0 % !r0 !r1 x1 !y0 % % (0/0) () 0 0 edge (0/0) () 0 5 edge () () 7 node % !r0 r1 !x1 x0 y0 % % (0/7) () 7 1 edge (0/7) () 7 9 edge % End. 
If you do not like the graph layout you can push the Options button and to choose the grid layout. After having chosen a new layout you have to place the model graph again. To place it again you have to use <== and ==> buttons to navigate to the graphplace expressions buffer of the model graph and to push the Place button, or to reload the PTTF program again and to push Run (or Compile ans Place) buttons.
This graph must be read as follows. The nodes 1 and 15 are the initial nodes. They are distinguished by the solid line rectangles around them. All other nodes are accepting nodes. A node represents a set of possible circuit states at a given instant. Let us take, for example, the node 0. Here is its graphplace records taken from the compilation log file presented at step 2. You can see that this node is described by 2 cubes: (!r0 !r1 !x1 !x0 !y0) and (!r0 !r1 x1 !y0).
() () 0 node % !r0 !r1 !x1 !x0 !y0 % !r0 !r1 x1 !y0 
The labels on model graph edges have no special meaning for the circuit. They are used to decorate the graph.
Every infinite sequences of states starting in an initial state and looping over the accepting states is an accepting run of the model graph. An accepting run of the model graph is a run of the circuit.
/* Equivalence checking example, Anatol Ursu, 2013 This example deals with the equivalence of two sequential circuits: x1 . ..  .'.  `1  .. r0  .. r1  MUX  R0 ' R1  y0 x0 0  `' `' `' .. q0 x1  Q0 . `' ..  .'.  `1  .. q2  .. q1  MUX  Q2 ' y1 x0  Q1 0  `' `' `' The equivalence checking of these circuits can be done by checking that the circuits produce the same values on the outputs "y0" and "y1" when the inputs with the same names are feed with the same values. In fact, we can check the signals "r1" and "q2" instead of "y0" and "y1" because "y0" == "r1" and "y1" == "q2". We represent the circuits as one circuit with two outputs (see the circuit below) and then we check whether the signals "r1" and "q2" are equivalent or not. x1..  ..   .'.   `1  .. r0  .. r1   MUX  R0 ' R1  x0.0  `' `'   `'     .. q0 ` Q0 .  `' ..   .'.   `1  .. q2   .. q1  MUX  Q2 ' ` Q1 0  `' `' `' The PTTF code of this circuit and the property to verify are presented at the end of this file. The property is given in the negative form. MGE tool uses the negative form of properties because the complementation of Buchi automata is difficult in general case. The verification of the PTTF code by MGE tool will produce a verification Buchi automaton that accepts all sequences of states that violate the circuits equivalence. If the circuits are equivalent, this Buchi automaton is empty  it accepts an empty set of sequences that violate the equivalence. Indeed, for the initial state (!r0,!r1,!q0,!q1,!q2) the Buchi automaton is empty (it has no accepting state) and, thus, the circuits are equivalent. To obtain a case when the circuits are not equivalent, consider the initial state (r0,!r1,!q0,!q1,!q2). For this initial state the Buchi automaton is not empty and, thus, the circuits are not equivalent. To run this program and to view the Buchi automaton of the verification push the buttons:  "Run" or  "Compile" and "Place" Note: Use mouse drag and drop to place the nodes of the graph manually. Use "==>" and "<==" buttons to look for log messages. */ //The PTTF code starts below this line /*====================================================*/ Module EquivCheck(x0, x1) Input x0, x1; /* We do not declare the output variables, we use register variables r1 and q2 to check the equivalence of circuits.*/ Begin //The initial state !r0 ^ !r1 ^ !q0 ^ !q1 ^ !q2; //The register r0 [](((!x1 ^ x0)  (x1 ^ r0)) => @(r0)); [](!(((!x1 ^ x0)  (x1 ^ r0))) => @(!r0)); //The register r1 [](r0 => @(r1)); [](!r0 => @(!r1)); //The register q0 [](x0 => @(q0)); [](!x0 => @(!q0)); //The register q1 [](x1 => @(q1)); [](!x1 => @(!q1)); //The register q2 [](((!q1 ^ q0)  (q1 ^ q2)) => @(q2)); [](!(((!q1 ^ q0)  (q1 ^ q2))) => @(!q2)); /* The next formula is the negation of the property stating that the circuits are equivalent. The circuits are equivalent if the registers r1 and q2 are equivalent. Thus, in the negative form, the formula tells us that there are some states such that the outputs of the registers r1 and q2 are different. */ NPROPERTY <>!equiv(r1, q2); /* The MGE tool will prove that this formula is always FALSE. Indeed, the Buchi automaton of this program and of the negated property has no accepting run, because it has no accepting state. Thus, the circuits are equivalent. */ End 
% Graphplace representation of the PTTF verification graph % This is an automatically generated file by MGE tool, v. 0.2. () () 51 node % !r0 !r1 x1 !x0 !q0 q1 !q2 % % (0/51) () 51 15 edge (0/51) () 51 23 edge (0/51) () 51 41 edge (0/51) () 51 51 edge () () 3 node % !r0 r1 x1 x0 !q0 !q1 q2 % % (0/3) () 3 25 edge (0/3) () 3 47 edge (0/3) () 3 55 edge (0/3) () 3 61 edge () () 63 node % !r0 r1 !x1 !x0 !q0 !q1 q2 % % (0/63) () 63 17 edge (0/63) () 63 21 edge (0/63) () 63 57 edge (0/63) () 63 59 edge () () 67 node % r0 r1 x1 x0 !q0 q1 q2 % % (0/67) () 67 7 edge (0/67) () 67 35 edge (0/67) () 67 45 edge (0/67) () 67 49 edge () () 61 node % !r0 !r1 !x1 !x0 q0 q1 !q2 % % (0/61) () 61 17 edge (0/61) () 61 21 edge (0/61) () 61 57 edge (0/61) () 61 59 edge () () 19 node % r0 !r1 !x1 !x0 q0 !q1 !q2 % % (0/19) () 19 3 edge (0/19) () 19 9 edge (0/19) () 19 13 edge (0/19) () 19 63 edge () () 39 node % r0 r1 x1 x0 q0 !q1 q2 % % (0/39) () 39 7 edge (0/39) () 39 35 edge (0/39) () 39 45 edge (0/39) () 39 49 edge () () 13 node % !r0 r1 !x1 x0 !q0 !q1 q2 % % (0/13) () 13 11 edge (0/13) () 13 19 edge (0/13) () 13 31 edge (0/13) () 13 65 edge () () 1 node % r0 r1 !x1 !x0 q0 !q1 q2 % % (0/1) () 1 3 edge (0/1) () 1 9 edge (0/1) () 1 13 edge (0/1) () 1 63 edge () () 35 node % r0 r1 !x1 !x0 q0 q1 q2 % % (0/35) () 35 3 edge (0/35) () 35 9 edge (0/35) () 35 13 edge (0/35) () 35 63 edge (@i) () () 69 node % !r0 !r1 x1 !x0 !q0 !q1 !q2 % % (0/69) () 69 15 edge (0/69) () 69 23 edge (0/69) () 69 41 edge (0/69) () 69 51 edge () () 11 node % r0 !r1 x1 !x0 q0 !q1 !q2 % % (0/11) () 11 27 edge (0/11) () 11 43 edge (0/11) () 11 53 edge (0/11) () 11 67 edge () () 9 node % !r0 r1 x1 !x0 !q0 !q1 q2 % % (0/9) () 9 15 edge (0/9) () 9 23 edge (0/9) () 9 41 edge (0/9) () 9 51 edge () () 17 node % !r0 !r1 !x1 !x0 !q0 !q1 !q2 % % (0/17) () 17 17 edge (0/17) () 17 21 edge (0/17) () 17 57 edge (0/17) () 17 59 edge () () 47 node % !r0 !r1 x1 !x0 q0 q1 !q2 % % (0/47) () 47 15 edge (0/47) () 47 23 edge (0/47) () 47 41 edge (0/47) () 47 51 edge (@i) () () 29 node % !r0 !r1 x1 x0 !q0 !q1 !q2 % % (0/29) () 29 25 edge (0/29) () 29 47 edge (0/29) () 29 55 edge (0/29) () 29 61 edge (@i) () () 0 node % !r0 !r1 !x1 !x0 !q0 !q1 !q2 % % (0/0) () 0 17 edge (0/0) () 0 21 edge (0/0) () 0 57 edge (0/0) () 0 59 edge () () 7 node % r0 r1 !x1 x0 q0 q1 q2 % % (0/7) () 7 1 edge (0/7) () 7 5 edge (0/7) () 7 33 edge (0/7) () 7 39 edge () () 65 node % r0 !r1 x1 x0 q0 !q1 !q2 % % (0/65) () 65 7 edge (0/65) () 65 35 edge (0/65) () 65 45 edge (0/65) () 65 49 edge () () 59 node % !r0 !r1 x1 x0 !q0 !q1 !q2 % % (0/59) () 59 25 edge (0/59) () 59 47 edge (0/59) () 59 55 edge (0/59) () 59 61 edge (@i) () () 37 node % !r0 !r1 !x1 x0 !q0 !q1 !q2 % % (0/37) () 37 11 edge (0/37) () 37 19 edge (0/37) () 37 31 edge (0/37) () 37 65 edge () () 15 node % !r0 !r1 !x1 x0 !q0 q1 !q2 % % (0/15) () 15 11 edge (0/15) () 15 19 edge (0/15) () 15 31 edge (0/15) () 15 65 edge () () 43 node % r0 r1 !x1 !x0 !q0 q1 q2 % % (0/43) () 43 3 edge (0/43) () 43 9 edge (0/43) () 43 13 edge (0/43) () 43 63 edge () () 45 node % r0 r1 x1 x0 q0 q1 q2 % % (0/45) () 45 7 edge (0/45) () 45 35 edge (0/45) () 45 45 edge (0/45) () 45 49 edge () () 53 node % r0 r1 x1 !x0 !q0 q1 q2 % % (0/53) () 53 27 edge (0/53) () 53 43 edge (0/53) () 53 53 edge (0/53) () 53 67 edge () () 21 node % !r0 !r1 x1 !x0 !q0 !q1 !q2 % % (0/21) () 21 15 edge (0/21) () 21 23 edge (0/21) () 21 41 edge (0/21) () 21 51 edge () () 49 node % r0 r1 x1 !x0 q0 q1 q2 % % (0/49) () 49 27 edge (0/49) () 49 43 edge (0/49) () 49 53 edge (0/49) () 49 67 edge () () 31 node % r0 !r1 !x1 x0 q0 !q1 !q2 % % (0/31) () 31 1 edge (0/31) () 31 5 edge (0/31) () 31 33 edge (0/31) () 31 39 edge () () 55 node % !r0 !r1 x1 x0 q0 q1 !q2 % % (0/55) () 55 25 edge (0/55) () 55 47 edge (0/55) () 55 55 edge (0/55) () 55 61 edge () () 5 node % r0 r1 !x1 x0 q0 !q1 q2 % % (0/5) () 5 1 edge (0/5) () 5 5 edge (0/5) () 5 33 edge (0/5) () 5 39 edge () () 33 node % r0 r1 x1 !x0 q0 !q1 q2 % % (0/33) () 33 27 edge (0/33) () 33 43 edge (0/33) () 33 53 edge (0/33) () 33 67 edge () () 41 node % !r0 !r1 !x1 !x0 !q0 q1 !q2 % % (0/41) () 41 17 edge (0/41) () 41 21 edge (0/41) () 41 57 edge (0/41) () 41 59 edge () () 57 node % !r0 !r1 !x1 x0 !q0 !q1 !q2 % % (0/57) () 57 11 edge (0/57) () 57 19 edge (0/57) () 57 31 edge (0/57) () 57 65 edge () () 23 node % !r0 !r1 x1 x0 !q0 q1 !q2 % % (0/23) () 23 25 edge (0/23) () 23 47 edge (0/23) () 23 55 edge (0/23) () 23 61 edge () () 25 node % !r0 !r1 !x1 x0 q0 q1 !q2 % % (0/25) () 25 11 edge (0/25) () 25 19 edge (0/25) () 25 31 edge (0/25) () 25 65 edge () () 27 node % r0 r1 !x1 x0 !q0 q1 q2 % % (0/27) () 27 1 edge (0/27) () 27 5 edge (0/27) () 27 33 edge (0/27) () 27 39 edge % End. 
If you do not like the graph layout you can push the Options button and to choose the grid layout. After having chosen a new layout you have to place the model graph again. To place it again you have to use <== and ==> buttons to navigate to the graphplace expressions buffer of the model graph and to push the Place button. Alternativelly, you can reload the PTTF program again and to push Run (or Compile ans Place) buttons.
Below, the model graph is displayed using the grid layout.
NPROPERTY <>!equiv(r1, q2); 
This formula is the negation of the property stating that the circuits are equivalent. The circuits are equivalent if the registers r1 and q2 are equivalent. Thus, in the negative form, the formula tells us that there are some states such that the outputs of the registers r1 and q2 are different.
The MGE tool proved that this formula is always FALSE. Indeed, the model graph of the PTTF program and of the negated property has no accepting run, because it has no accepting state. Thus, the circuits are equivalent.
/* Traffic light controller example, Anatol Ursu, 2013 This example deals with the traffic light controller circuit. It uses the onehot encoded design: .. .\ \__Red  ./ /   ''  . ..   '\ \__Yellow   ./ /    ''   .Green .....            .o.  .o.  .o.  .o.               . r0 ' r1 ' r2 ' r3 '.   .>  .>  .>  .>                     `o'  `o'  `o'  `o'     1                  Clk ''''   Rst ''''  '' This circuit contains four registers, r0, r1, r2 and r3. The PTTF program of this circuit and the properties to verify are presented at the end of this file. 1) The first property to verify states that the circuit is onehot encoded. 2) The second property to verify states that the the signals "Red" and "Green" are never ON together. The properties are given in the negative form. MGE tool uses the negative form of the properties because the complementation of Buchi automata is difficult in general case. The verification of the PTTF code by MGE tool will produce a verification Buchi automaton that accepts all sequences of states that violate the specified properties. If the properties are verified (proved correct), this Buchi automaton is empty  it accepts an empty set of sequences that violate the properties. Indeed, for the initial state (r0,!r1,!r2,!r3) the Buchi automaton is empty (it has no accepting state) and, thus, the verified properties are proved correct for this circuit. To obtain a case when the properties are not proved correct, consider the initial state (r0,r1,!r2,!r3). For this initial state the Buchi automaton is not empty and, thus, the circuit is not correct for these properties. To run this program and to view the Buchi automaton of the verification push the buttons:  "Run" or  "Compile" and "Place" Note: Use mouse drag and drop to place the nodes of the graph manually. Use "==>" and "<==" buttons to look for log messages. */ //The PTTF program starts below this line /*====================================================*/ Module TrafficLight(Clk, Rst, Red, Yellow, Green) Input Clk, Rst; Output Red, Yellow, Green; Begin //The initial state of the registers r0 ^ !r1 ^ !r2 ^ !r3; //The next two formulas describe the register r0 [](r3 => @(r0)); [](!r3 => @(!r0)); //The register r1 [](r0 => @(r1)); [](!r0 => @(!r1)); //The register r2 [](r1 => @(r2)); [](!r1 => @(!r2)); //The register r3 [](r2 => @(r3)); [](!r2 => @(!r3)); /* This formulas describe the output signals of the circuit, the signals "Red", "Yellow" and "Green". */ []equiv(r0 \/ r1, Red); []equiv(r1 \/ r3, Yellow); []equiv(r2, Green); /* The next formula is the negation of the property stating that the circuit is onehot encoded. Thus, in the negative form, the formula tells us that there are some states that are not onehot encoded. */ NPROPERTY <>!one_hot(r0, r1, r2, r3); /* The next formula is the negation of the property stating that the the signals "Red" and "Green" are never ON together. Thus, in the negative form, the formula tells us that there are some states that the signals are ON together. */ NPROPERTY <>(Red ^ Green); /* The MGE tool will prove that these formulas are always FALSE. Indeed, the model graph of this program and of the negated properties has no accepting run, because it has no accepting state. Thus, the circuit is onehot encoded and the signals "Red" and "Green" are never ON together. */ End 
% Graphplace representation of the PTTF verification graph % This is an automatically generated file by MGE tool, v. 0.2. () () 11 node % !r0 !r1 !r2 r3 !Red Yellow !Green % % (0/11) () 11 3 edge () () 5 node % r0 !r1 !r2 !r3 Red !Yellow !Green % % (0/5) () 5 1 edge () () 3 node % r0 !r1 !r2 !r3 Red !Yellow !Green % % (0/3) () 3 0 edge () () 0 node % !r0 r1 !r2 !r3 Red Yellow !Green % % (0/0) () 0 15 edge (@i) () () 7 node % r0 !r1 !r2 !r3 Red !Yellow !Green % % (0/7) () 7 0 edge () () 17 node % !r0 !r1 r2 !r3 !Red !Yellow Green % % (0/17) () 17 13 edge () () 1 node % !r0 r1 !r2 !r3 Red Yellow !Green % % (0/1) () 1 17 edge () () 15 node % !r0 !r1 r2 !r3 !Red !Yellow Green % % (0/15) () 15 11 edge () () 13 node % !r0 !r1 !r2 r3 !Red Yellow !Green % % (0/13) () 13 5 edge (@i) () () 9 node % r0 !r1 !r2 !r3 Red !Yellow !Green % % (0/9) () 9 1 edge % End. 
If you do not like the graph layout you can push the Options button and to choose the grid layout. After having chosen a new layout you have to place the model graph again. To place it again you have to use <== and ==> buttons to navigate to the graphplace expressions buffer of the model graph and to push the Place button. Alternativelly, you can reload the PTTF program again and to push Run (or Compile ans Place) buttons.
NPROPERTY <>!one_hot(r0, r1, r2, r3); NPROPERTY <>(Red ^ Green); 
The first property states that the circuit is onehot encoded. In the negative form this property tells us that there some states that are not onehot encoded.
The second property states that the signals "Red" and "Green" are never ON together. In the negative form this property tells us that there are some states in the circuit such that "Red" and "Green" are on together.
This formula is the negation of the property stating that the circuits are equivalent. The circuits are equivalent if the registers r1 and q2 are equivalent. Thus, in the negative form, the formula tells us that there are some states such that the outputs of the registers r1 and q2 are different.
The MGE tool proved that these properties is always FALSE. Indeed, the model graph of the PTTF program and of the negated properties has no accepting run, because it has no accepting state. Thus, the circuit is correct for these properties.
1. x0 & x1 2. (!x0  !x1) 
/* The Tautology Checking example, Anatol Ursu, 2011 This example checks the equivalence of two boolean formulas: 1. x0 & x1 2. (!x0  !x1) The PTTF program to check this equivalence is presented at the end of this file. To run this program and to view the model graph push the buttons:  "Run" or  "Compile" and "Place" Note: Use mouse drag and drop to place the nodes of the graph manually. Use "==>" and "<==" buttons to look for log messages. The tool will produce one node model graph and the following log output.  (@i) () () 0 node %TRUE % (0/0) (0) 0 0 edge % End.  The model graph accepts an infinite sequence of TRUE states. It means the formulas (1) and (2) are equivalent. */ //The PTTF code starts below this line /*====================================================*/ Module TautologyCheck(x0, x1) Input x0, x1; Begin //The invariant saying the the formulas (1) and (2) are equivalent []equiv(x0 & x1, !(!x0  !x1)); End 
As you can see the body of PTTF program consists of one statement:
//The invariant saying the the formulas (1) and (2) are equivalent []equiv(x0 & x1, !(!x0  !x1)); 
This statemens specifies the fact that the formulas x0 & x1 and !(!x0  !x1) are equivalent.
% Graphplace representation of the PTTF model graph. % This is an automatically generated file by MGE tool, v. 0.2. (@i) () () 0 node %TRUE % (0/0) () 0 0 edge % End. 