My First Model, Data Types
ContentsExample project reminder
The previous step of the tutorial showed a simple system that we want to model, and the creation of an AlPiNA project. We will now see how to specify the Data Types that we will use for this model, and the next step will show how to specify the system behaviour with a Petri Net.
The model we want to implement can be described with the following Business Project, created with Intalio|BPM.
You should have created an AlPiNA project, whose contents should be similar to those in the next image.
We can see:
- A file for the graphical description of a Petri Net, called PinCheckAPN.apn_diagram.
- A file that contains the structure of the Petri Net, called PinCheckAPN.apn. Most users will never need to open this file, as they should work on the graphical description instead.
- A file that will contain our ADT, i.e. the first Data type we will define, called Users.spec.
- The standard AlPiNA ADTs, namely blackToken, boolean, listOfNats and nat. This list may grow in the future.
Data types : User identifiers (an ennumerated type)
AlPiNA uses Algebraic Petri Nets as modeling formalism, this means that Data Structures are described using ADTs. The first Data Type we will define is the users identifiers. For this model, we will choose an ennumerated list of users. The ADT will be defined in the file Users.spec.
As it is based on XText, AlPiNA supports auto-completion during the edition of the .spec files. Simply hit ctrl + space (if you didn't change the default Eclipse shortcuts) and you should see a list of options, like in the next image.
You can now write your first ADT, following the model in the next image. For now, we will only create 3 users: Albert, Brenda and Charles.
An ADT definition has two sections: an Interface, where we will define constants and operations signatures, and a Body, where we will define the behaviour of our operations. The signature defines Sorts (the types of the ADT elements), Generators and Operations. The difference between the two latest will be explained in the next section, when we will see how to define a set of elements using a combination of constants and operations.
The Users ADT is very simple, it only has 3 constants and no operator. As there isn't any behaviour to define, we don't need a Body section.
Data types : the naturals (an infinite type)
We have defined users identifiers, now we will define their PIN codes. For this we will use the default ADT naturals. Open the file nat.spec if you want to see how an infinite domain can be defined with the ADTs. We will se an excerpt here:
The natural numbers are generated with two symbols: a constant called zero and an operation called suc (for successor), that are combined in order to form an inductive definition. Thus, the number 1 is represented by suc(zero), 2 is suc(suc(zero)) and so on. Note that AlPiNA supports iter theory notation, thus we can write suc^45(zero) and obtain the natural number 45. Moreover, we have defined in the image above three operations: dec (for decrement, the inverse operation for suc), plus and minus.
We have thus defined five symbols for out ADT, two generators (one constant an one operation) and three operations. These symbols can be combined in order to form terms. Constants and operations signature (i.e. domain and co-domain) must be respected when defining terms. In AlPiNA, the terms are created using Prefix notation, so the operations name is written before all the operands.
The behaviour of the operations is defined in the Body section of our ADT, where a set of axioms are defined for each operator. Axioms definition uses induction in order to attain every possible value in our domain.
As an example, we will consider both axioms for the plus operator:
- plus (zero, $x) = $x;
- plus (suc($y), $x) = suc(plus($y, $x));
For example, to compute the operation 2+3 the following steps will be performed:
- We start with the term plus(suc^2(zero), suc^3(zero)).
- Our second axiom is applied, and we obtain a new term suc(plus(suc(zero), suc^3(zero)).
- Our second axiom can be applied again, and we obtain suc^2(plus(zero, suc^3(zero))).
- Now it's the first axiom that can be applied, to obtain suc^2(suc^3(zero)), i.e. suc^5(zero).
- No more axioms can be applied, we obtained the final result for our initial operation.
The difference between Generators and simple Operators is not really important for a basic user with a small model, but if you want to build a big model and user more advanced features like Unfolding (that will be explained later in this tutorial), this difference becomes really important. All values in the domain we want to define should be created with a combination of Generators. For example, the natural numbers we just saw are built with the two generators, zero and suc. The other operations don't create new values, but they define some behaviour on our domain.
Data type: pairs (a hierarchical definition of a complex structure)
So far we have and ADT for Users, and an ADT for the PIN codes (we will simply use the natural numbers). If we check the Business Process that represents the system we want to model, we can see that we'll need a more complex structure: pairs of the type <User, Pin>. For this we will create a new ADT that will use the two previous ADTs.
We want to create a new ADT, so we have to create a new .spec file. Clic on File -> New -> Other and look for the option algspec editor file under XText DSL Wizards.
Click next, and give a name for your new file. We will use a descriptive name : Pair_user_nat.spec. The ADT defined in this file should look like the following image:
We will update this ADT later with more functionalities. For now, we only have one symbol, an operator pair_un (for pair_user_nat) that takes two arguments, a User and a natural, and builds a pair with them. We also defined two simple operators that retrieve the User and the natural number from a given pair.
That is for the pairs of the type <User, nat>. If we look at our Business Process, we see that we will also need another kind of pair for the final answer, pairs of the type <User, Boolean>. The ADT defining this pair has to be created in a new .algspec file, and it will look a lot like the previous ADT. Its definition can be seen in the image below:
In the future, AlPiNA will support genericity, so defining different pairs for different sorts will be far easier. For now, we need to define an ADT for every kind of pair.
Let's check our Business Process again. We ask the user for this PIN code, and we retrieve the real PIN code corresponding to the same user. We can represent both results with a pair of the type <User, nat>, that we just defined. These two pairs will be then compared, and a pair <User, boolean> will be created. This comparison is a complex operation that should be defined in an ADT. As we want to compare couple of the type <User, nat>, we should create an operation in the ADT Pair_un, that can be found in the file called Pair_user_nat.spec.
Let's open that file and create one operation called compare and two axioms, like in the following image:
In the interface we can see that we added a new operation called compare that takes two pairs of the sort pair_un and returns a pair of the sort pair_ub. Please be sure to put all the needed imports in your ADT.
The axioms used to define the behaviour of the operation compare are quite simple:
- get_user($pun) = get_user($pun1) & get_pin($pun) = get_pin($pun1) =>
compare($pun, $pun1) = pair_ub(get_user($pun), true);
- get_user($pun) = get_user($pun1) & get_pin($pun) != get_pin($pun1) =>
compare($pun, $pun1) = pair_ub(get_user($pun), false);
The first line contains the conditions for the axioms to be applied. We want to compare only pairs that refer to the same user, so we add a condition get_user($pun) = get_user($pun1). The second condition will define the result of the comparison: if the pin codes are the same (i.e. get_pin($pun) = get_pin($pun1)) we want to return a pair <User, true>. This behaviour was defined in the first axiom. The second axiom describes the creation of a pair <User, false> if the two PIN codes were different.
Data types: a list (a complex inductive structure)
So far we have defined:
- An enumerated data type for our users
- An inductive un-bounded type for their PIN codes (using the naturals ADT)
- Two data types for the pairs <User, natural> and <User, boolean>
We need one more data type to model our system. The Business Process indicates that the system must retrieve the user password from a database. We will represent this database with a list of pairs <User, nat>, where we will associate each User to his PIN code.
The ADT representing this structure should look like the following one:
As in the naturals, we use an inductive definition. We declare a sort called ulist (for users list), a constant to represent an empty list called empty_ulist and an operator that adds an element to a given list (ulist). In short, a list with one element is represented by a term of the type <Element, empty list>. A list with two elements will be represented by a term <Element1, <Element2, empty list>> and so on.
We will only need to define one operation for this data type, a getter, that takes two parameters: a user and a list, and returns the pair <User, Natural> corresponding to the user. The axioms defining the behaviour of this operator are quite simple. We simply check if the user of the first pair of our list is equal to the user we are looking for. If it's not the case, we continue the search in the sub list.
Please note that this list ADT is not really safe. We could make it better, for example adding axioms to ensure that all users appear only once in the list. We could also check that a user actually belongs to a list when looking for it. In the name of simplicity, we will keep this ADT as it is, without this kind of checks.
Now that we have defined all our data types, we can start building the actual Petri net. This is done in the next step of this tutorial, My First Model, Petri Net.