Introduction

PNSDD is a CTL model checker using the Hierarchy Set Decision Diagram technology. For more detail about the SDD, refer you to this page below:

• LIBSDD (developped by A. Hamez)
• LIBDDD (developped by Y. Thierry-Mieg)
• LIBITS (developped by Y. Thierry-Mieg)
• IDDMC and ZBDDMC (developped by Technische Universität Cottbus)

The use of different libraries justifies the several menus entries (one for each type of used library). PNSDD works on P/T nets and can also process Colored nets (but with a preliminary unfolding).

The menus

When the Colored Petri net you have designed is syntactically correct, you can reach yhe following services that allows you to access one of the available version of PNSDD.

When the service is selected, a windows ask you the ammount of memory you want to affect to PNSDD (only on the Linux version). The selected percentage is computed from the total available RAM on the machine running CPN-AMI. PNSDD is automatically stoped when the selected memory bound is reached.

If you cancel this dialog box, by default, memory bound is set to 90 % of the RAM.

After having selected the memory bound, you must enter the CTL Formula to be checked in the dedicated window. If you only want to calculate the state space click on cancel.

Let us consider this small Coloured Petri net displayed below. It is a quite small model including composed tokens and successor/predecessor functions. It is thus quite difficult to analyse and could worth an unfolding. The syntax for formulas is presented at the bottom of this page.

When you click on OK, the formula is computed and resultas are displayed as shown below.

Description of the syntax

The syntax is described as follows:

• semi-colon separator is ";" (at the end of each formula)
• Atomic formula : variable = xx (where xx is a correct value)
• variable must be the name of a place into the model
• Basic Operator :
  • F AND G = F * G (Intersection)
  • F OR G = F + G (Union)
  • NOT(F) = !(F) (Negation)
  • F -> G = F -> G (Then)
• EX(F) Exist a next of F
• EF(F) Exist a futur of F
• E(F U G) Exst F until G
• EG(F) Exist Globally F
• AX(F) For All paths there is a next of F
• AF(F) For All paths there is a future of F
• A(F U G) For All paths there is F until G
• AG(F) For All paths there is Globally F

Here are some examples of formulas:

• EF(init_ID0 = 1 * init_ID1 = 2);
• E(init_ID0 = 1 U init_ID1 = 2);
• AF(EG(init_ID0 = 0) -> EF(end_ID0 = 1));

where INIT_ID0, INIT_ID1 and end_ID0 refer to places. Be careful, for colored nets, you must consider that a colored place will be unfolded (its name is then postifex by the value of the color corresponding to the non colored place).