My First Model, Petri Net
ContentsPetri Net creation
The Pin databases (the tricky part)
Modeling the user interaction
Final result (with a conditional transition)
Petri Net creation
If you followed the previous step in this tutorial, you should have by now an AlPiNA project and a list of ADTs created. Once we have the data types, we must define the behaviour of our system, this will be done using Algebraic Petri Nets. If you want a quick introduction to Petri Nets, you can look here.
In AlPiNA, the graphical description of a Petri Net is done in file that have the apn_diagram extension. In our case, it's the file PinCheckAPN.apn_diagram. Once you double click on this file, the first thing to do is to give a name for your Petri Net, this is done in the window at the bottom of your Eclipse interface, on the Properties tab. Please note that no element of your Petri Net must be selected in order to be able to see this window.
Our Petri Net will use the ADTs that we defined in previous steps of this tutorial. For this, we must import the correct ADTs. This can be done in the Specification imports tab. To import an ADT, clic on the '+' button and select the correct ADT. In our case, we must add all the ADTs that were defined in the previous step, that is:
Now we're ready to create our Petri Net. We will start by creating our first Place. This place will be a container where we will add all our clients at the beggining of our system execution. To create a place, simply clic on the place icon in the palette, then clic in any place of your diagram. A place is created, and automatically select (notice that when you select an element, the properties pane is modified to show the properties of that element). We must give a name to our place and specify it's sort. In this case, we will simply call our place Users and it's sort will be user. Remember that we defined this sort in our ADT Users, when we clic in the Sort button in the Properties pane, we obtain a list of the sorts that can be found in our imported ADTs.
Now we have a Place, with a name and a sort. We will also add an initial marking. As we said before, the place Users will contain the list of our system users, so we will add 3 tokens: 1 token for Albert, 1 token for Brenda and 1 token for Charles. To do this, modifiy the place properties as in the next figure.
Please note that the marking we introduced is equivalent to [1*Albert, 1*Brenda, 1*Charles].
If we check our system (see previous steps), two actions will be taken simultaneously for every user: the system will ask him for his PIN and the system will retrieve a stored PIN code from the system database. We will represent this in our Petri Net with two new places, called respectively Ask_for_pin and retrieve_pin. Both places will have the sort User, and their initial marking will be empty.
During the execution of our Petri net, we want to take one of the users in the Users place, and to add it to both other places. This can be done with a transition.
We can create a transition exactly like we created a place, using the Transition button in the palette. We will name this transition select_user. We want the transition to take one token from the place Users, and to add the same token to the other two places, we achieve this adding 3 arcs: one arc from the place Users to the transition, and one arc from the transition to each other place. To add and arc, clic on the arc button in the palette, then single clic on the source (either a place or a transition) and finally clic on the destination. You should obtain a result similar to the next image.
Our transition is still missing something: the arcs indicate that the transition must take something from a place and put something into other places. We must indicate what must be taken and what must be added. In this case, we want to take any client, and we want to add the client we just took. This can be achieved using a variable.
To create a variable, we must use the variable pane in the bottom of the interface. Once in the variables pane we simply have to clic in the '+' button, just like when we added our adts, and give a name and a sort for our variable. Our first variable will be called 'c' and its sort will be client.
Now we can use this variable in our previously defined arcs. Simply select each one of them and select the properties pane. You must select the sort of the arc (it will be user for all our arcs) and set its multiset, like in the next figure.
Please note that you can put multisets in the output arcs, but input arcs must only have one variable or one closed term (a closed term is a term where there isn't any variable, i.e. it's only made of ADTs operators and constants).
We now have a very simple Petri Net that could even be executed. But it only models a very small part of our system. The next step will be more complicated.
The Pin databases (the tricky part)
We will now model the system part where the real user pin is retrieved from the system database. A database is in fact a list of pairs <User, pin> as seen on the previous tutorial. So we first add a place to represent our database, we will simply call it PIN_database, and its sort will be ulist.
Now we must set its initial marking. At the beggining, the database contains one entry for every user. To keep it simple, we will set the following pin codes:
Albert : 1
Brenda : 0
Charles : 2
As we said when we defined the Users_list ADT, the lists have an inductive definition based on a operator called ulist, whose domain is the pair <User, List>. The last element of the list is the constant empty_ulist.
So, if we want to create a list with one element, say the pair <Charles, 2>, we must first define the pair itself as follows:
Please note that we are using ither theory notation, suc^2(zero) means suc(suc(zero)). Now we can define our list with one element:
ulist(pair_un(Charles, suc^2(zero)), empty_ulist)
The ulist operator takes two arguments, a pair <user, nat> and a sublist. Here we only want one element in the list, so the sublist is simply an empty list. With this definition, we can build a list with two elements:
ulist(pair_un(Brenda, zero), ulist(pair_un(Charles, suc^2(zero)), empty_ulist))
and then it's easy to define the complete list of users, with their associated pin codes:
ulist(pair_un(Albert, suc(zero)), ulist(pair_un(Brenda, zero), ulist(pair_un(Charles, suc^2(zero)), empty_ulist))). Thus we obtain the marking of the place PIN_database.
We would want to create a transition that takes a user from the place Retrieve_pin, and the list from the place Pin_database, and returns the pair <user, nat> corresponding to the input user. The pin database must be restored to its original place, as it musn't be modified. For this, we create a transition and three arcs as shown in the following picture:
We want this transition to take a user (any user) from the place Retrieve_pin, we will simply use the same variable that was used in the first transition, called c. Furthermore, we want to take the pin database from the place Pin_database, for this we must build a new variable with the sort ulist. We build this variable as before.
Then we set the arcs for the last transition we built with their respective variables.
Please note that an arc must always have the same sort as the place that it's attached to. All we need now is to extract the pair <user, nat> from our database, and some place to put the result into. We build a new place called Pin_retrieved, where we will put this result.
Then we add an arc from the transition we previously built to that place. The "extraction" of the right pair will simply be done with the operator get_used that was defined in the previous chapter, on the Users_list adt. We simply set the term in the latest arc to get_user($c, $ulist).
Modeling the user interaction
For now, we have modeled the task in the bottom of our system, called "Retrieve password". We want now to model the task above, called "Ask password". Our model won't have a true interaction with an external user, we can model this interaction with a place containing a list of possible answers given by the user. This place is shown in the following image:
Please note that the term containing the list of pins is different from the above one: Charles is introducing a wrong pin! His true pin is the number 2, and he entered the number 3. Albert and Brenda, on the other side, entered the correct pins. Thus we expect our system to give two positive and one negative answer in the end.
Now, we can see that the two tasks Ask password and Retrieve password can be modeled in exactly the same way: we have a place containing the name of a user, another place containing a list of users associated to their pin codes, we select the correct pair and we add it to a third place. Thus we simply have to repeat exactly the steps above, until we get the following result:
Final result (with a conditional transition)
Now all we have to do is to compare both results, and return a final answer. This answer will be contained in a place called Answers, where we will store couples <user, bool> (so the sort of our place must be pair_ub). The boolean value associated with a user will indicate if the login process was successful. Note that we expect two true values (for Albert and Brenda) and one false value (for Charles).
We will now add the last component in our Petri net: a transition that will take both pairs <user, nat> from the places Pin_obtained and Pin_retrieved, will compare them and will put the correct result in the Answers place. In order to indicate that we want to take two different pairs <user, nat> (one from each place), we need to create two variables of the sort pair_un. We will simply call this varibles pun and pun2.
We can use these variables to build our transition:
For now, this transition will take any combination of pairs from both places. We would like to add a condition to this behaviour, we would only want to take pairs that have the same user. For this, we will use a condition in the transition. A condition comes as an equation "a = b", where a and b are terms of an ADT. Note that it's possible to use variables in these equations, but these variables must have been used in the preconditions of the transition. Our condition must ensure that both pairs have the same user, we can achieve this using the get_user operator taken from the pair_user_nat adt.
All we have to do now is to set the term in our last arc, i.e. to make the comparison itself. For this we will simply use the operator compare that we defined in the Pair_user_nat adt.
Voilà! Our petri net is done.
The next and final step of this tutorial, My First Model, Checks, will show how to compute the net's State Space, how to check some properties and the two main features of AlPiNA in terms of model checking large state spaces: clustering and unfolding.