Mypyvy CTI Representation

README.md

example.pyv is the pyv file I intend to pass as input (ported from Ivy - https://github.com/microsoft/ivy/blob/master/doc/examples/client_server_example.ivy).

It should present a CTI as follows:

state 0:
link(client0,server0)
semaphore(server0)

state 1:
link(client0,server0)
link(client1,server0)

where there exists a transition connect(client1,server0) between state 0 and state 1.

The output.json is along the lines of the JSON I would like to receive back after verification.

example.pyv

# https://github.com/Microsoft/ivy/blob/master/doc/examples/client_server_example.md#discovering-a-safety-invariant

sort client
sort server

mutable relation link(client, server)
mutable relation semaphore(server)

init semaphore(S)
init !link(C, S)

# The atomic actions of the system are declared as "transitions", 
# which are written as two-state formulas possibly parameterized 
# by some values (such as `c` in `connect` here).
# Each transition also specifies an optional `modifies` clause, 
# whose meaning is to add "doesn't change" conjuncts for all
# elements of the state that are not modified.
transition connect(c: client, s: server)
    modifies link, semaphore

    old(semaphore(s)) &
    (link(C, S) <-> old(link(C, S)) | C = c & S = s) &
    (semaphore(S) <-> old(semaphore(S)) & S != s)
    
transition disconnect(c: client, s: server)
    modifies link, semaphore

    link(c, s) &
    (link(C, S) <-> old(link(C, S)) & C != c & S != s) & # verbose syntax for "remove `c` from the `link` relation"
    semaphore(S) <-> old(semaphore(S)) | S = s

safety [mutex] link(C1, S) & link(C2, S) -> C1 = C2

invariant !(exists c0:client, c1: client, s0:server. c0 != c1 & link(c0, s0) & link(c1, s0))
# invariant !(exists c0:client, c1: client, s0:server. c0 != c1 & link(c0, s0) & semaphore(s0))

output.json

{
    "sorts": ["client", "server"],
    // Just ["client0", "client1", "server0"] can do just as well here. Sort can be inferred easily
    "entities": [{
        "name": "client0",
        "sort": "client"
     }, {
         "name": "client1",
         "sort": "client"
      },
      {
          "name": "server0",
          "sort": "server"
      }
    ],
    // can probably be simplified to ["mutable link(client,server)", "mutable !link(C,S)"]
    "relations": [
        {
            "name": "link",
            "sorts": ["client", "server"],
            "isMutable": true
        },
        {
            "name": "semaphore",
            "sorts": ["server"],
            "isMutable": true
        }
    ],
    // Can probably be simplified to ["semaphore(S)", "!link(C,S)"]
    "init": [
        {
            "name": "semaphore",
            "quantifiers": ["S"],
            "isNegation": false
        },
        {
            "name": "link",
            "quantifiers": ["C", "S"],
            "isNegation": true
        }
    ],
    // Can probably be simplified to ["connect(client,server)", "disconnect(client,server)"]
    "transitions": [
        {
            "name": "connect",
            "sorts": ["client", "server"]
        },
        {
            "name": "disconnect",
            "sorts": ["client", "server"]
        }
    ],
    "states": [
        {
            "id": 0,
            // can probably be simplified to ["link(client0, server0)", "semaphore(server0)"]
            "relations": [
                {
                    "name": "link",
                    "values": ["client0", "server0"]
                },
                {
                    "name": "semaphore",
                    "values": ["server0"]
                }
            ]
        },
        {
            "id": 1,
            // can probably be simplified to ["link(client0, server0)", "link(client1,server0"]
            "relations": [
                {
                    "name": "link",
                    "values": ["client0", "server0"]
                },
                {
                    "name": "link",
                    "values": ["client1", "server0"]
                }
            ]
        }
    ],
    "transitionsByStates": [
        {
            "name": "connect",
            "from": 0,
            "to": 1
        }
    ],
    "unverifiedSafeties": [
        {
            "name": "mutex",
            "safety": "link(C1, S) & link(C2, S) -> C1 = C2",
            "recommendedAdditionalInvariants": [
                "!(exists c0:client, c1: client, s0:server. c0 != c1 & link(c0, s0) & semaphore(s0))"
            ]
        }
    ],
    "invariants": [
        "!(exists c0:client, c1: client, s0:server. c0 != c1 & link(c0, s0) & link(c1, s0))"
    ]
}