Personal tools
You are here: Home Documentation Getting started My First Model, Checks

My First Model, Checks

Previous step: My First Model, Petri Net

Contents

State Space generation and properties
Clustering and unfolding


In the previous steps, we created a complete model, using ADTs to model data types and a Petri Net to model the system behaviour. Here we will see how to compute the net's State Space (i.e. the complete set of the sytem's possible states), how to check some simple properties and how to tweak the performances. To fully understand this last step, you may find useful to learn some aspects of the underlying technology used by AlPiNA, for details you can check xxx.

State Space generation and properties

Once the Algebraic Petri Net has been completely defined, we may want to generate its state space. This is simply done by clicking on the "Compute State Space" button.
SP_button.png

After we click on it, we see a window that asks us which ADTs should be unfolded. For now we can see that no ADT is available, and we can only click on the "ok" button.
no_unfolding.png

Unfolding is a technique used by AlPiNA to get better performances. In some cases, the improvement can be dramatic. We will see later how to use this feature, for now our model is very small and we don't really need to improve the performances, as the state space is obtained very fast.
216_states.png

We can see that our system has 216 states. Indeed, our system can be in one of 6 positions for each user:
net_states.png

The cartesian product of our 3 users gives us the result of 216 states.

Now that we have generated the entire state space for our Petri Net, we would like to checks some properties on it. If you remember, we introduced an user who entered the wrong pin, it was Charles whose pin was suc^2(zero) and who entered the pin suc^3(zero). We would like to check that our system doesn't give a positive answer to Charles. Of course, this is a trivial test, but it will serve as an example.

To define a property to be checked, we need to create a new .spec file, as we did before for the ADTs. The content of this file should look like the following one:
property.png

First, we have to import all the ADTs we will be using in our property definition, just like the ADTs. Then we have to list all the petri net's places that we will be using, with their respective sort. We are aware that this is very uncomfortable, but the next version of AlPiNA should present a lot of improvements in this field.

After we created the file, we can start defining our properties. If more than one property is defined, all of them will be checked, and if one of them doesn't hold, a negative answer will be returned. In our example we are checking tree properties:
-The first two properties check that the content of the place PIN_database is never modified. We first check that we never have more than one token in that place, and then we check that the token is always the same as the initial marking.
-The last property checks that we never give Charles a positive answer.

Once we have defined the properties we want to check, we must save the file (here we used the name property.spec), and then we must import the file into our Petri Net, just like we imported our ADTs.
import_property.png

Once we have imported the property, we can launche the check itself, with the button "Check property". We can see that all the properties we have defined hold.
Properties_hold.png

Now let's see an example where our property does not hold. We could for example check that the place Users does never have more than 2 users. This is obviously false, but only for the initial state, where there are 3 tokens in that place.
false_property.png

If we try to check that property, we obtain a message telling us that one of our properties does not hold and asking us to check the console.
prop_doesnt_hold.png

If we check the console, we can see that only one of our properties didn't hold, and we obtain a counterexample. This counterexample shows the content of each place where the property was violated. Here it is the place Users, and its marking is the initial one, where the 3 users are present in the same place.
console_view.png

As you can see, there are currently two kinds of reachability checks that can be performed with AlPiNA:
-checks concerning the cardinality of a multiset
-checks concerning the contents of a multiset

Multisets can either be explicitely declared:
-as a single term, like in our examples
-as a complete multiset: {1*Albert, 2*Charles}
Or they can represent the content of a place (i.e. content(p1))

They can also manipulated with the usual multiset operators, i.e. union, difference and intersection, (i.e. content(p2) intersection {2*Brenda, 3*Albert, 1*Charles}).

Clustering and unfolding

The model we just checked was quite simple, and we got our results really fast. AlPiNA's objective, on the other hand, is to allow model checking of models with really big state spaces. For this, there are two techniques that can really improve the performances. The first one is clustering.

Clustering leverages on the fact that big system often are composed of concurrent process that have similar behaviour. This is the case of our 3 users, each one of them has more or less the same behaviour as the others, and each one has a very small behaviour (6 states). It's the combination of their behaviours that creates a big state space.

To be more specific, the cluster definition is a function P x T -> Cl, where P is the set of places and T is the set of possible tokens. For each place and token, we must identify which process is concerned. For this, we can take profit of the inductive definition we created in our ADTs.

Let's see the clustering for our example:

Clustering.png

After the imports, variables and places definitions (like in the properties files), we can find the cluster definition itself. First of all there is a declaration for all the clusters we want to create, and then the rules that will distribute the tokens to their correct cluster.

Here we declared two kinds of clusters: one for the global data (i.e. the lists of users with their respective pin codes), and one cluster for each specific user. These three clusters are defined in an inductive way, like the naturals in the nat ADT. The three parameters are the name of the first cluster, the name of the next-cluster operator and the number of clusters to be generated. This means that the "inductive (c0, ncl, 3)" declaration will produce three clusters: c0, ncl(c0) and ncl(ncl(c0)).

After the clusters declaration, we create the rules to distribute the tokens amongst the clusters. The first 3 rules indicate that all the tokens concerning Albert will go to the cluster c0. We need three different rules as there are three different kinds of tokens concerned. The following rules indicate the same for Brenda and the cluster ncl(c0) and Charles and the cluster ncl(ncl(c0)).

The last rule assigns every token in the places PIN_database and UserPins to the db cluster, as we know that these places will always have the same only token.

In our case, all the users are constants, it would maybe be better to also declare all clusters as constants:
Other_clustering.png

The inductive definition of clusters is very useful when coupled to the inductive definitions. Imagine that instead of declaring a new datatype for the users we used integers to identify them. We could then have declared the following cluster function, much more compact:
Third_clustering.png

Once the clustering definition has been finished, it must be imported into the Petri Net, just like the ADTs and the properties files:

import_clustering.png

Once we defined our clustering function, we may want to compute the state space again. If we hit the "compute state space" button, we find the unfolding panel, that was disabled before we defined our clustering function.

Unfolding.png

Now, we must present the second AlPiNA feature that will help us improve the state space generation and check's performances : unfolding.

Unfolding simply consists in computing all (or some of) the possible terms of an ADT before computing all the calculations. We won't go into technical details here, but when this is possible it can represent a significant speedup in the computing.

In our example, we can compute all the terms of the ADT boolean, as there are only 2 of them: true and false. We can do the same for the users ADT, as there are only three terms (the three users). This is called a complete unfolding. On the other hand, we cannot compute all the terms of the naturals ADT, because they are infinite. But we know that we never use any natural number above 3, so we can compute the terms of the ADT with a limit of 3. This is called a partial unfolding.

As we just unfolded the ADTs Users, nat and boolean, we can also completely unfold the ADTs that use them: Pair_user_bool and Pair_user_nat. The users_list ADT cannot be completely unfolded, just like the naturals, because it is an infinite ADT. We may be tempted to compute a partial unfolding here, but it would be a very bad idea: even with only three users and three possible pin codes, the number of possible combinations is much too big. It's much better to keep this ADT without unfolding.

This example shows that there is no precise rule to define the ADTs unfolding, it must be adapted to every case.

 We get the following result:
Unfolded_216_states.png

Please note that our example is very small, and the performances gain of clustering and unfolding may not be really visible. On the other hand, systems with much bigger state spaces will gain a lot more from these techniques.


This was the last chapter of our tutorial. If you have further questions or comments, do not hesitate to use our forum or the AlPiNA bugzilla!

Document Actions