Examples

Here are few examples included in the archive of VaChe.

Producer consumer

We can modelize a consumer producer system with a VASS.
If you open the file "example/product_comsom.pns" with VASS_editor you will get this :

Then, if you ask about the boundeness, the VASS_editor will answer that this VASS is bounded :

However, if you ask about the prefix boundeness, it will answer that the VASS is not prefix bounded :

Sliding window protocol

We can modelize the sliding window protocol with a VASS.
If you open the file "example/Sliding_window_protocol.pns" with VASS_editor you will get this :

If you ask about the prefix boundeness, the VASS_editor will answer that the VASS is prefix bounded : Sliding window protocol

Simple cryptographic protocol

We can modelize a simple cryptographic protocol with TINA and save it in the file "example/SCP.tpn" : TINA Simple cryptographic protocol

Let's check the following property : "If a ticket cannot be consumed without the client’s private key, then the server does not consume jobs submitted by the intruder ?".

./Petri_net_MSO example/SCP.tpn "(all1 x: x<-Tickets => x<-PrivateKey) => Server<-Jobs<-JobSubmission" Formula is valid

The tool indicates that this property is true.

Let's check now the following property : "If a ticket cannot be consumed without the client’s private key, then the client consumes only tickets that it has requested ?"

./Petri_net_MSO example/SCP.tpn "(all1 x: x <- Tickets => x <- PrivateKey) => JobSubmission <- Tickets <- TrustedThirdParty <- p3 <- TicketRequest" Formula is not valid

The tool will answer that this property is false and exhibit the smallest process for which the property is not satisfied : Counter Example