Snoopy Tool Evaluation

Snoopy is a tool which is used for designing and animating hierarchical graphs along with others Petri nets. Snoopy also provides the facility to construct Petri nets and allows animation and simulation of the resulting token flow. This tool is used to verify technical systems specifically software-based systems and natural systems e.g. signal transduction, biochemical networks as metabolic and gene regulatory networks. Snoopy is in use for consideration of the qualitative network structure of a model under specific kinetic aspects of the specified Petri net class and investigation of Petri net models in several complementary conducts. Simultaneous usage of different Petri net classes in Snoopy is one of its outstanding features. Other features are:

It is extensible as its generic design aids the implementation of new Petri net classes.
It is adaptive as numerous models can be used simultaneously.
It is platform independent as it is executable on all common operating systems e.g. linux, mac, windows.

Two particular types of nodes i.e. logical nodes and macro nodes are meant for supporting the systematic construction, neat arrangement and design of large Petri nets. Logical nodes act as connector or multiple used places or transitions sharing the same factor or function. Macro nodes allow hierarchically designing of a Petri net. Snoopy allows edition and coloring of all elements in each Petri net class and manual or automatic change of network layout too. Prevention of syntactical errors in the network structure of a Petri net is facilitated by the implementation of the graphical editor.

Editor Mode:

Start Snoopy and go to File New or press the new button in the tool bar. It results in opening of a template dialogue that allows selection of the document template.

File: New/Open/Close Window/Save/Save as, Print, Export/Import, Preferences (change the default visualization) and Exit.

Edit: Undo/Redo, Select All/Copy/Copy in new net/Paste/Cut, Clear/Clear all, Hide/Unhide, Edit selected elements/Transform Shapes, Layout (automatic layout function), Sort Nodes (by ID or name), Check Net (duplicate nodes, syntax, consistency) and Convert to.

View : Zoom 100%/Zoom In/Zoom Out, Net Information (number of each element used in the model), Toogle Graphelements/Hierachy browser/Filebar/Log window, Show Attributes (choose for each elements which attributes to be shown in the model), Start Anim-Mode/SimulationMode/Steering-Mode.

Elements (list of all available elements): Select/ Place/Transition/ Coarse Place/Coarse Transition/ Immediate Transition/Deterministic Transition/Scheduled Transition/Parameter/Coarse Parameter/LookupTable, Edge/Read Edge/Inhibitor Edge/Reset Edge/Equal Edge/Modifier Edge and Comment.

Hierarchy (edit and browse hierarchy): Coarse (chosen elements are encapsulate in a macro node)/Flatten and Go Up in Hierarchy/Go To First Child in Hierarchy/Go To Next Sibling in Hierarchy/o To Previous Sibling in Hierarchy.

Search : Search nodes (by ID or name).

Extra : Load node sets (visualize, e.g., T-, P-invariants, siphons and traps), Interaction and General Information (title, author, description, literature).

Window (arrange all opened windows): Cascade/Tile Horizontally/Tile vertically, Arrange Icons/Next/Previous and Open Files.

Help: Help, About (current version), check update.

The tool bar holds four shortcuts that facilitate:

Open a new document.

Load a document.

Save a document.

Select an element.

All elements accessible in the current net class are displayed in panel for the graph elements. Left-click on one of the elements enables user to use one of these elements. Right click on the respective element allows user to edit or select all elements of the same class. All levels are displayed in hierarchy browser and any hierarchical level can be opened in a new window by a left-click. The editor pane can be considered as the canvas which allows user to draw the network. A left-click on the Editor pane activates chosen element and places the selected element on the canvas. Click left onto one node, hold the left-click, drag the line to the other node and drop the left-click, to draw an arc between two nodes. To add edges to an arc push the CRTL key and click left on the arc which facilitates the user to drag the edge with another left-click. Grid in the canvas tab can also be used for a better orientation. User can also pick edge styles i.e. line or spline in the preference dialogue in the elements tab.

Elements:

Nodes:

Elements

Graphics

Standard transition

Standard transition

Coarse place

Coarse transition

Immediate transition

Deterministic transition

Scheduled transition

Immediate Transition: Immediate transitions fire as soon as they are enabled. The waiting time is equal to zero.

Standard Transition (Timed Transition): A waiting time is computed as soon as the transition is enabled. The transition fires if the timer elapsed zero and the transitions is still enabled.

Deterministic Transition: Deterministic transitions fire as soon as the fixed time interval elapses during the entire simulation run time. The respective deterministic transitions must be enabled at the end of each repeated interval.

Scheduled Transition: Scheduled transitions fire as soon as the fixed time interval elapsed during the given time points. The respective deterministic transitions must be enabled at the end of each repeated interval.

Edges:

Elements

Graphics

Description

Standard edge

The transition is enabled and may fire if both pre-places and are sufficiently marked by tokens. After firing of the transition, tokens are removed from the pre-places and new tokens are produced on post place.

Read edge

The transition is enabled and may fire if both pre-places A and B are sufficiently marked by tokens. After firing of the transition, tokens are removed from the pre-place B but not from pre-place A, new tokens are produced on post place. The firing of the transition does not change the amount of tokens on pre-place A.

Inhibitor edge

The transition is enabled and may fire if pre-place B is sufficiently marked by tokens. The amount of tokens on pre-place A must be smaller than the given arc weight. After firing of the transition, tokens are removed from the pre-place B but not from pre-place A; new tokens are produced on place C. The firing of the transition does not change the amount of tokens on pre-place A.

Reset edge

The transition is enabled and may fire if pre-place B is sufficiently marked by tokens. The amount of tokens on pre-place A has no effect on the ability to enable the transition and affects only the kinetics. After firing of the transition, tokens are removed from the pre-place B according the arc weight and all tokens on pre-places A are deleted; new tokens are produced on place C.

Equal edge

The transition is enabled and may fire if number of tokens on pre-place A is equal to the corresponding arc weight and place B is sufficiently marked. After firing of the transition, tokens are removed from the pre-place B but not from preplace A; new tokens are produced on place C. The firing of the transition does not change the amount of tokens on pre-place A.

Modifier edge

The transition is enabled and may fire if pre-place B is sufficiently marked with tokens. The amount of tokens on pre-place A has no effect on the ability to enable the transition and affects only the kinetics. After firing of the transition, tokens are removed from the pre-place B but not from pre-place A; new tokens are produced on place C. The firing of the transition does not change the amount of tokens on pre-place A.

Functions:

Name

Meaning of function

BioMassAction(.)

Stochastic law of mass action. Tokens are interpretated as single

molecules.

BioLevelInterpretation(.)

Stochastic law of mass action. Tokens are interpretated as concentration.

ImmediateFiring(.)

Refers to immediate transitions.

TimedFiring(.)

Refers to deterministic transitions.

FixedTimedFiring Single(.)

Refers to deterministic transitions that only res once after a given timepoint

FixedTimedFiring(., ., .)

Refers to scheduled transitions.

abs(.)

Absolute value

acos(.)

Arc cosine function

asin(.)

Arc sine function

atan(.)

Arc tangent function

ceil(.)

Rounding up

cos(.)

Cosine function

exp(.)

exponential function

sin(.)

Sine function

sqrt(.)

Square root

tan(.)

Tangent function

floor(.)

Round off

log(.)

Natural logarithm with constant e as base

log10(.)

Common logarithm with constant 10 as base

pow(.)

Exponent

Parameters:

Parameters are used for defining individual parameters and rate or weight functions but are not able to define the number of tokens on a particular place. Third group of macro elements are coarse parameters which facilitate encapsulating parameters. High numbers of parameters are not visible on the top-level or can also be categorized by the use of coarse parameters.

Animation mode:

Snoopy allows user to observe the token flow in animation mode which starts by pressing F5 or going to View and then start AnimationMode. It will result in opening a new window which allow user to steer the animation. This part of snoopy is very beneficial to catch a first expression of the causality of a model and its workings as it provides information about the transitions too. In order to understand modeled mechanism, playing with the token flow prove to be worthwhile. The token flow can be animated manually by a single click on the transition. A message box is displayed revealing a message “This transition is not enabled” when user tries to fire a transition that is not enabled. Clicking-left and clicking-right on a place aids addition of tokens and extraction of tokens respectively. Animation of the token flow can also be controlled by using the radio buttons present on the animation steering panel. Usage of radio buttons involves step-wise forward and backward or sequentially as long as one transition can be enabled, otherwise a notification “Dead State: There are no more enabled transitions” is displayed on screen.

Simulation Mode

Pressing F6, going to view/Start Simulation or using the stochastic simulation button on the animation control panel, are three ways to perform stochastic simulations with the current model in the active window. Facilities of this mode include simulation of the time-dependent dynamic behavior of the model indicated by the token flow or the firing frequency of the transitions. The fluctuating concentration levels or the discrete number of the components over time is indicated by the token flow. This provides an impression of the time-dependent changes in model under consideration which is helpful in understanding the wet-lab system. More than a few simulation studies can be performed with considered model by manipulating the structure and perturbing the initial state and kinetics. All results can be manually and automatically exported in the standard *.csv-format and can be analyzed in other mathematical programs.

Simulation Control:

The simulation control allows selection of main settings and individualities for the simulation. It splits further into four panels:

Configuration Sets: Modification of configuration sets is carried out by edition of single entries or addition of new sets and picking the configuration sets that is suitable for the simulation run.
Simulation Properties: It includes setting interval start i.e. time point where simulation starts, interval end i.e. time points where simulation ends and output step count i.e. number of time-points that should be displayed in the given interval.
Export Properties: Various automatic export settings are accessible to the *.csv-format.
Start Simulation: It will initiate simulation with the selected settings and properties. Progress of simulation is indicated by the bar and the required time is displayed below.

Viewer/Node Choice:

It facilitates user by providing choices in displaying simulation results. It is divided into two panels:

Viewer Choice: It provides user an option to select one between data tables and data plots. Provided buttons in panel allow user to edit, add and delete the data tables and data plots. Token flow (places) or the firing frequency (transitions) can be displayed in a data table or data plot.
Place Choice: User can choose those nodes which should be displayed in the data table or data plot.

Display:

This panel allows displaying the simulation results as data table or data plot. If data table is selected, the token flow for the selected places is presented in a table. Some options which are used for model checking are present at the bottom of the window. If data plot is chosen, the x-axis displays the time-interval and the y-axis indicates the average number of tokens. View of the plot can be altered via the buttons located below i.e. compress/stretch x-axis, compress/stretch y-axis, zoom in/out and centre view. A csv export button allows user to export the simulation results of the selected places manually. Image of the current plot can be saved by using print button.

Model Checking Mode:

Snoopy is enabled to perform model checking of linear-time properties based on the stochastic simulation. A subset of probabilistic linear-time temporal logic (PLTL) is employed to formulate and authenticate properties. Various features of snoopy also include checking several features at the same time. In order to perform model checking in Snoopy, user needs to open the simulation window and select the table view. To perform model checking on all simulation traces, user have to enter or load a property that is checked by simulating the time-dependent dynamic behavior. Simulation window allows following options:

Enter State Property: User can specify a property in the dialogue box and no model checking is performed if it is empty.
Load state property: User can load a property which is defined in a text file.
Check state property: It refers to model checking which is performed on the basis of average behavior of the previous simulation.

Simulation run count is of assistance to state a number of simulation traces to which model checking can be applied. It splits into two types:

Default value 1 run: User is only able to get the information if the defined property holds true or is not false.
Arbitrary number of runs: The number of simulation runs supports defining probability of the defined properties as high accuracy calls for high number of simulation runs.

User can set the time interval where model checking should be applied with the help of interval start and interval end.

A log window displays model checking results that includes following elements:

Formula displays the formula checked during simulation.

Runs indicate the number of simulation runs performed.

Runtime shows the number of threads used for simulation.

Threads display the number of threads used for simulation.

Prop indicate the computed probability for the formula.

S ^2 displays the variance of the probability.

Confidence Interval indicates the size of the confidence interval.

[a,b] reveals the interval of the probability that is calculated from the confidence interval