Users Manual (en) for 1.x

Japanese Version→Users Manual (jp) for 1.x

How to Write the model

Configuration of the main screen

• Main screen of HiPS is composed of four panes.

①Structure of the Petri net that is currently being edited

②Attribute of an selected element(place, arc ,transition, sub page)

• You can edit the label of the element etc.

③Petri net editing screen

• Page of Petri nets is displayed in the tab.
• When the element of Petri Nets is selected, the edge becomes blue and selected elements(place, arc ,transition etc) are displayed in the second pane.
• It is referred to as the canvas in this document.

④Firing history etc.

Tool bar

Names of various buttons on the toolbar and functions (From left to right).

(1)Select button

• While selecting the Select button, you can select an element on the canvas. In addition, you also can select multiple elements by dragging.

(2)Place button

• While selecting the Place button, you can add a new place in its place by clicking on the canvas

. (3)Transition button

• While selecting the Transition button, you can add a new transition in its place by clicking on the canvas.

. (4)Arc button

• While selecting the Arc button, you can link a transition and a place by an arc on the canvas.
• You can add an arc by clicking on a transition from a place you want to connect in order.

(5)Scaling button

• You can scale Petori nets on the canvas.

(6)Hand tool button

• You can move the position of the entire canvas by clicking on the canvas.

(7)Stepping simulation button

• When Stepping simulation button is selected, the canvas becomes a simulation mode, and you can run the random firing simulation of Petri nets in the design.

(8)Stopping simulation

• You can return to design mode from simulation mode.

Menu bar

Menu list of HiPS

1. File
   • New Net : Create new net
   • open  : Read Petri net HiPS files that are saved in xml format
   • close  :
   • Save  : Save to overwrite
   • Save As :
   • Exit  : Exit the HiPs
2. Edit
   • New Page  : Create new page
   • Undo(Ctrl+Z)  :
   • Redo(Ctrl+Y)  :
   • Cut(Ctrl+X)  :
   • Copy(Ctrl+C)  :
   • Paste(Ctrl+V)  :
   • Delete(Del)  :
   • SelectAll(Ctrl+A) :
3. Tool
   • Cancel
   • SnapShot  : Create a screenshot of the Petri net on the canvas you are currently viewing
   • IncidenceMatrix  : Display incidence matrix of Petri net in tabular format or text format
   • Structural Property : Static analysis
   • T-invariant  : Analyze the T-invariant of Petri nets on the canvas you are currently viewing
   • Behavioral Property : Dynamic analysis
   • Reachability Graph with Delay : Reachability analysis(Bounded)
   • Reachability Graph with Delay for Unbounded : Coverablity analysis(Unbounded)
   • Deadlock  : Deadlock analysis
   • Bounded  : Bounded analysis
   • Reversibility  : Reversibility analysis
   • FC/AC Liveness/Safeness Check : FC/AC Active safety checker
4. Help
   • Manual  : Display manual
   • HiPS Web Page : Display HiPs project page on sourceforge
   • Version  : Display version information

Model design

1. Create new Petrinet xml file or new page

   File->New Net

   Edit->New Page

2. Add place and transition

   Select the Place button(Transition button)

   While selecting the button, you can add a new place(transition) in its place by clicking on the canvas

3. Add arc

   While selecting the Arc button, when you click the Place(Transition) order and Transition(Place), they are bridged by an arc between the elements.

   In addition, place and place or transition and transition can't connect by arc

4. Installation of token

   While selecting the Select button, click on the place you want to set the token to selected state on the canvas. (When a element is selected, the edge becomes blue.)

   Enter the number of token to "InitialMarking" in the place property settings screen (second pane of the main screen).

   

5. Set weight of arc

   While selecting the Select button, click on the arc you want to set the weight to selected state on the canvas. (When a element is selected, the edge becomes blue.)

   Enter the number of weights to "weight" in the second pane of the main screen.

   

6. Set label of element

   For each element of Petri net such as place and transition, you can set the label different from id of the element. (But you can't set arc.)

   While selecting the Select button, click on the place or transition you want to set the label to selected state on the canvas. (When a element is selected, the edge becomes blue.)

   Enter the label to "Name" in the second pane of the main screen.

   

Make sub page

Describes a method for manufacturing a hierarchical Petri net(sub-page).

1. Introduction of Sub-pages

   On main Petri net screen design, select File→New→NewPage, make new page. At that time, Petri net design canvas will be in the form tab, and Petri nets were designed on the page by selecting the tab will appear.

   

2. Sub-page design

   In each sub-page, it is necessary to specify the port to the element.　This port is that the input and output port to connect with the main Petri net.

   You can be set place or transition　to the port.　So, it is possible to set input and output ports of the plurality to one of sub-page.

3. Port Settings

   Select an element on the canvas of the sub-page,　and edits the "PortDir" of property (second pane of the main screen). Set "None" if you do not have anything set, set "In" if you want to set as an input port, set "Out" if you want to set as an output port.

   

   
   

   

4. Insert Sub-page

   Configure at least one for each sub-page input and output ports,　open the canvas you want to install a sub-page.

   In the ① pane of the main screen,　the structure of the Petri net that is being edited are marked. Drag and drop to the ③ pane from ① pane, which was designed as a sub-net. Then, the sub-page will be added to the canvas.　It is not possible to insert　page the port is not set as a sub-page.

   

How to use the simulation capabilities

1. Simulation of Petri net

   Designed Petri nets can be simulated on HiPS. In this simulation, transition to fire as the operation of the transition firing is red, and marked token in place transitions.

   

   
   

   

2. Stepping simulation button

   Designed Petri nets can be simulated by Stepping simulation button that is also button(7) on the toolbar.

   When you press Stepping simulation button, canvas switch to simulation mode. Simulation where the token moves actual start. But, if it becomes impossible to fire in the middle, you will not be able to simulate more.

3. Log in simulation

   During simulation,　ｆiring sequence of transitions that fire so far is retained.　In the fourth pane of the main screen, transitions fired is output each time you press Stepping simulation button.

4. Sub-page during simulation

   It is also possible simulation of hierarchical Petri nets. When token enters the hierarchical portion, simulation is performed automatically in the sub-page, and token output. Simulation is performed in random firing even in the sub-page, If there is a firing sequence of several, it is impossible to know what will be output in any firing sequence. In addition, confirmation of the firing sequence is possible, because it is output to the log.

   
   

   

How to use the analysis functions

The description of the function of various analysis on HiPS. All analysis functions are available from the Tool→Behavioral Property or Tool→Structual Property in the menu bar.

Dynamic analyzer

Reachability Graph analysis(Bounded)

When the firing sequence to convert the markingM₀ to markingM_n is exist,　markingM_n has reachable from markingM₀. In net(N,M₀), the set of all markings that reachability from M₀　noted　R(N,M₀). Reachability problem of Petri nets is a problem　that demand whether it is M_n∈R(N,M₀) for markingM_n in in net(N,M₀). Reachability analysis on HiPS enumerates all marking reachability from the initial marking the transition relation between markings. But, it is impossible to apply for an unbounded net.

1. des(0,7,8) respectively corresponds the initial state, the number of state transition relation, the number of marking.
2. Next seven lines represent the relationship between the state transition.
3. Under number->Marking represents the markings corresponding to the state number.

Coverability Graph analysis (Unbounded ω-trans.)

If markingM₁ satisfies the condition to be M₁(p)≧M(p) in R(N,M₀) exists for all place p in the net, markingM in a Petri net(N,M₀) is coverable. Coverage analyzer represent the transition of marking as a finite graph structure by introducing ω to marking capable of covering for unbounded net. Reachability marking from the initial marking, the transition between marking is listed.

1. des(0,7,8) respectively corresponds the initial state, the number of state transition relation, the number of marking.
2. Next seven lines represent the relationship between the state transition.
3. Under number->Marking represents the markings corresponding to the state number. Because it is unbounded, marking that token would increase infinitely represented using ω.

Extended Coverability Graph analysis (Unbounded N*-trans.)

TBA

Deadlock analysis

When there is no transition can fire, the marking is deadlock. The deadlock analyzer　analyze whether the reachability to the depth specified in the form,　and find the markings that are deadlocked. When Marking that is deadlocked is found, display the firing sequence leading up to it with its marking.

1. You can specify the depth to deadlock analyze in the field of Depth.
2. If firing sequence that leads to a deadlock exists more than one, display the firing sequence and marking one of them.

k-bounded analysis

When the number of tokens in each place does not exceed a finite number k, Petri net is called bounded or　k-bounded　simply　in any marking reachability from M₀, Bounded analysis analyzes the boundedness to the depth specified in the form.

1. You can specify the depth of the analysis of boundedness in the field Depth.
2. Display the marking obtained results were analyzed boundedness under the k-bounded.

Reversibility analysis

If reachability is M₀ from M for all marking of R(N,M₀), Petri net (N,M₀) is called reversible. It is always possible to go back to the initial marking, if the net is reversible.

1. Reversibility analysis stat button
2. It is possible to choose which was the sum of permutation invariant, or which was alone permutation invariant. Need to be checked either.
3. Check box for parallel processing
4. Cancel button of the analysis
5. Progress bar
6. Play and pause button
7. Display remaining time
8. Now, display whether pause or during the analysis
9. Refresh the text box of the log
10. Refresh the the color of the table, the color of the net figure
11. Visibility of the progress bar
12. Visibility of the log
13. Ignite sequentially firing sequence of the row that was pressed (Ignition scenario)
14. Colors of all transitions included in the press line is changed
15. A line is a Firing sequence of one．
16. There is one transition at one cell．Color of transitions of selected net is changed.
17. Log space of ignition scenario．Display marking and fired transitions．By default, initial marking and the order of the place and is displayed.

Synchronic Distance and Fairness analysis

Using the synchronic distance, it is possible to quantify the degree of interdependence of events between the two in Condition / Event systems. Display in a grid format for the presence of fairness of two types and the following values ​​of the synchronization distance in the "synchronization distance and fairness analyzer".

• B-fair net

Two transitions are said to be in a B-fair relation if the other is not firing is bounded. A Petrin net(N,M₀) is said to be a B-fair net if every pair of transitions in the net are in a B-fair relation.

• Unconditionally fair net

A firing sequence σ is said to be unconditionally fair if it is finite or every transition in the net appears infinitely often in σ. A Petrin net(N,M₀) is said to be an unconditionally fair net if every firing sequence σ from M in R(M₀) is unconditionally fair.



When you Synchronic Distance and Fairness analysis, the above screen is displayed. Analysis result of the synchronic distance is displayed in the cell. Analysis results of fairness is displayed in the text field.

1. View synchronic distance in the rows and columns of the transition in the net. "-" Means that the synchronic distance analysis of the same transition between is not performed. If synchronic distance is finite, cell color become blue. If synchronic distance is 0, cell color become red.
2. The view to the cell value of the synchronic distance of all in the "All" button click.
3. The delete to the cell value of the synchronic distance of all in the "Clear" button click.
4. Show ID and name of transition, structurally bounded and fairness.

The figure above is the case you click a cell "t4" part of the line. Only synchronic distance of the clicked line is displayed.
It appears in the text field as shown in the figure on "Bounded Fair Net" case net of the analysis target is a B-fair net, and "Unconditional Fair Net" the case of unconditional equity net.

By clicking on the value of the synchronic distance, change the color of the transition of Petri nets. Synchronic distance value is changed to yellow-green in the case of finite, it is changed to purple otherwise.

Structure analyzer

T-invariant

When let A be incidence matrices of Petri net, and let x be firing count vector, integer solution x of A^Tx = 0 is called T-invariant.



When you run a T-invariant analysis, the above screen will appear. Users can choose the output format button on the "Text" and, "Table".



If you select "table", the above figure is output. Each invariant is expressed on a per-row basis. By pressing the button of "view" in the column　of "ColorView", the invariant of the row that was pressed will be reflected in the net.





If you select "text", the above figure is output.



If you analyze T-invariant in Petri net T invariant does not exist, the above screen will appear.

S-invariant

When let A be incidence matrices of Petri net, and let y be firing count vector, integer solution y of Ay = 0 is called S-invariant.
We can analyze S-invariant with the same procedures as T-invariant analysis.

Structurally Analayzer

Structurally Analyzer analyze the structural properties of the Petri net.
Structural Property depends on the topological structure of the Petri net.They are independent of the initial marking in the sense that these properties hold for any initial marking or are concerned with the existence of certain firing sequences from some initial marking.
It is possible to analyze 7 properties from incidence matrix and its associated homogeneous equations or inequalities. So, Petri net of interest must be pure.

• Structurally Bounded

The Petri Net is said to be structurally bounded if it is bounded for any finite initial marking.

• (Partially) Conservative

The Petri net is said to be (partially) conservative if there exists a positive integer for every(some) place p such that the weighted sum of tokens.

• (Partially) Repetitive

The Petri net is said to be (partially) repetitive if there exists a marking and a fire sequence from a initial marking such that every(some) transition occurs infinitely often in a firing sequence.

• (Partially) Consistent

The Petri net is said to be (partially) consitent if there exists a marking and a fire sequence from a initial marking back to a initial marking such that every(some) transition occurs at least once in a firing sequence.



The above screen appears when you run a structurally analyzer.　The table has columns about Structurally bounded, conservative, partially conservative, repetitive, partially repetitive, consistent, partially consistent from left. And the table has cell where you want to display the analysis result of the property of each.



When you press the Start button, and then press the button of each property, analysis of properties that are turned ON begins. The results are displayed in the cell as shown on the above screen at the end of the analysis. if the Petri net has property， '+' is displayed, and if the Petri net does not have property, '-' is displayed.

Structurally Analyzer has counter example feedback function. To analyze in a state which the items of "Analyze counter example" are checked, It can analyze counter example of structurally bounded, conservative and consistent.
By clicking on the cell that result is '-' from above screen, places and transitions and sub-pages of the cause is colored.

• Structurally Unbounded

Transitions of cause are colored purple. If the transitions continue to fire, the Petri net will be unbounded.

• Unconservative

The Petri net does not have conservative means that the weighted sum of tokens is increased or decreased.
By transitions that are colored red firing, the weighted sum of tokens is increased. By transitions that are colored blue firing, the weighted sum of tokens is decreased.

• Unconsistent

The Petri net does not have consistent means that, there dose not exist a marking and a fire sequence from a initial marking back to a initial marking such that every(some) transition occurs at least once in a firing sequence.
When every transitions is fired, it color places that the number of tokens is increased or decreased compared to the marking. Places the number of tokens increases are colored red, and places the number of tokens decreases are colored blue.

Liveness and Safeness in Free-Choice(FC) net

TBA

Exhausted Process Trace Generation

TBA

LTL Model Checker

TBA