Propositional Temporal Transition Formulas Model Graph Extractor

Model Graph Extractor (MGE) applet is a tool for Propositional Temporal Transition Formulas (PTTF) model graphs extraction. The model graph of a temporal logic formula is the fundamental data in formal verification and model checking.

On the picture below you can see the screenshot of the MGE applet.

How to use the applet

  1. to start the applet.
  2. In the text area of the applet you can see a PTTF program. This is a demo PTTF program of a sequential circuit. The program is loaded from the file SeqCircuit.pttf. This file was loaded into the applet during the applet initialization. It includes a long comment that explains the program. The PTTF program starts with the statement Module SeqCircuit(x0, x1, y0).

    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.

  3. Alternatively, you can push Compile and then Place buttons to get the same result. It means, you Compile the program first and then you Place the model graph. After each step you can use <== button to look for log messages.
  4. A list of demo examples is available. See the drop list containing SeqCircuit.pttf under the applet text area. You can choose an example from this list and then push the Load Spec button to load it in the applet text area.
  5. You can also type or copy your own PTTF program into the text area and push the Run (or Compile and then Place buttons).
See more information about PTTF tool input language syntax, as well as try some examples.

The Model Graph Extractor Applet


The MGE applet buttons

A short description of the MGE applet buttons:
New buff
Creates a new text area buffer. The applet text area is mapped to a buffer. A buffer is the object containing the text from the text area. Each time you push the New button, the current text area contents is saved in a buffer and a new empty text area is displayed. The buffers are chained in a list. You can navigate though these buffers using ==> and <== buttons.
Close buff
Closes current text area buffer. The object corresponding to this buffer is removed from the list. The text area is mapped to the previous buffer of the list.
Close all
Closes all buffers. The text area is mapped to a new buffer.
Run
Runs the PTTF program displayed in text area. This action calls the PTTF compiler and the model graph placer. The model graph is displayed in the lower panel of the applet.
Compile
Compiles the PTTF program from the text area. The compiler produces the model graph of the PTTF program in textual (graphplace) format. If the compilation terminates successfully the model graph text is displayed in a new text area.
Place
Places the model graph produced by the compiler. The model graph is displayed in the lower panel of the applet.
Options
This button allows us to set the MGE tool options.
Reset
Resets the applet. This button reloads the default demo example SeqCircuit.pttf in the text area. Also, it clears the lower panel of the applet and initializes the default options of the tool.
About
Shows the About info box panel.
Load Spec
Loads a demo PTTF program. You can choose a demo example from the list to the left of this button. After having loaded the demo example you can push the Run, or the Compile and Place buttons.
Load Graph
Load a demo graph. You can choose a demo example from the list to the left of this button. After having loaded the demo example you can push the Place button.


Example 1

A sequential circuit

  1. Given the following PTTF program of a sequential circuit.

    /* 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
    

  2. If you load or paste this PTTF program into the TextArea of the MGE applet and then push the Compile button you will obtain the following satisfiability analysis result in a new buffer:

    % 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.
    

  3. If you push then the Place button the following model graph will be displayed in the lower panel of the applet. The graph is displayed using a circle layout (see the picture below).

    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.

  4. The steps 2 and 3 can be carried out by a simple push on Run button. (To see the log file after having pushed the Run button push 2 times the button <==).
  5. If you still do not like the graph layout, you can improve it manually using mouse drag and drop actions. Below you can see the same graph placed manually.
  6. 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
    
    Each cube contains input, output and registers variables. A cube encodes a set of minterms. A minterm represents the values of input, output signals as well as the values of the circuit registers at a given instant.

    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.

Example 2

Equivalence checking

  1. Given the following PTTF program of a sequential 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
    

  2. If you load or paste this PTTF program into the TextArea of the MGE applet and then push the Compile button you will obtain the following result in a new buffer:

    % 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.
    

  3. If you push the Place button the model graph (Buchi automaton) will be displayed in the lower panel of the applet. The model graph is displayed using the circle layout.

    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.

  4. If you still do not like the graph layout, you can improve it manually using mouse drag and drop actions.
  5. This model graph must be read as follows. The nodes in solid rectangles, that is the nodes 11, 33, 43 and 65, are the initial nodes. All other nodes are normal nodes. As you can see there is no accepting node in this graph (an acception node is represented by double line circles). Thus, the model graph does not accept any run. This situation is normal when checking properties in negative form, like in our case. In this example we check the property,

    
       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.

Example 3

Property checking

  1. Given the following PTTF program of a sequential circuit.

    /* Traffic light controller example, Anatol Ursu, 2013
    
       This example deals with the traffic light controller circuit. It
       uses the one-hot 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 one-hot 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 one-hot encoded. Thus, in the negative form, the
       formula tells us that there are some states that are not one-hot
       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 one-hot encoded and the signals "Red"
       and "Green" are never ON together. */
    
    End
    

  2. If you load or paste this PTTF program into the TextArea of the MGE applet and then push the Compile button you will obtain the following result in a new buffer:

    % 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.
    

  3. If you push the Place button the model graph (Buchi automaton) will be displayed in the lower panel of the applet. The model graph is displayed using the circle layout.

    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.

  4. If you still do not like the graph layout, you can improve it manually using mouse drag and drop actions.
  5. This model graph must be read as follows. The nodes in solid rectangles, that is the nodes 7 and 9, are the initial nodes. All other nodes are normal nodes. As you can see there is no accepting node in this graph (an acception node is represented by double line circles). Thus, the model graph does not accept any run. This situation is normal when checking properties in negative form, like in our case. In this example we check the properties,

    
       NPROPERTY <>!one_hot(r0, r1, r2, r3);
       
       NPROPERTY <>(Red ^ Green);
    
    

    The first property states that the circuit is one-hot encoded. In the negative form this property tells us that there some states that are not one-hot 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.

Example 4

Tautology checking

  1. The MGE tool can be used as a tautology checker as well. For example, suppose one wants to check te equivalence of these formulas.

      1. x0 & x1
      2. (!x0 | !x1)
    

  2. The PTTF program used to check the equivalence of these formulas is presented below:

    /* 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.

  3. If you load or paste this PTTF program into the text area of the MGE applet and then push the Compile button you will obtain the following satisfiability analysis result in a new buffer:

    % 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.
    

  4. As we can see, the model graph consists of a node and a loopback edge. The boolean expression of the node is the value TRUE - the universal set. This means that the formulas are equivalent.
  5. If you push then the Place button the following one node model graph will be displayed in the lower panel of the applet.


Back to Top