Each monitor is associated with a subnet of a CPN, i.e. a set of places and transitions from the CPN. During a simulation a monitor can examine and extract information from the subnet.
A subnet consists of:
- Zero or more place instances and
- Zero or more transition instances
Three data types are defined for each monitor when a monitor is created, and these data types are dependent on the subnet that is associated with the monitor. The three data types are
BindElemmarkingssubnet
The data type BindElem determines the binding elements that the monitor can examine. A binding element is a transition instance together with a binding of the variables for the transition.
The data type markings is a representation of the markings of the place instances that are associated with the monitor. The markings data type determines the information from the net that a monitor can examine in the initialization and stop monitoring functions.
The data type subnet determines the information from the net that a monitor can examine after simulation steps in the predicate and observation monitoring functions.
Data type definitions for subnets
The data types that are defined for a monitor are dependent on the places and transitions that are associated with the monitor. This section shows how the data types for monitored subnets are defined depending on the number of places and transitions that are associated with a monitor.
When two or more places are associated with a monitor, they are ordered. They are sorted in ascending order by name, where the name is a string with this format <pagename>'<placename>_<instance number>_mark.
No places, no transitions
datatype BindElem = unit
type markings = unit
type subnet = unit
When no nodes are associated with a monitor, then each of the three data types will be of type unit which consists of the single value () which is pronounced ‘unity’.
Some places, no transitions
datatype BindElem = unit
type markings = <cs (t)ms>_1 * <cs (t)ms>_2 * … * <cs (t)ms>_n
type subnet = markings
Where <cs (t)ms>_i depends on the color set inscription for the i’th place (where places are ordered as described above). If the color set of the i’th place is one of the timed color sets, then <cs (t)ms>_i is the set of timed multi-sets over the values from the color set of the place. If the color set of the i’th place is not a timed color set, then <cs (t)ms>_i is the set of multi-sets over the values from the color set of the place.
Concrete examples of how markings data types are defined can be found below.
No places, some transitions
datatype BindElem =
<pgname_1’transname_1> of int * {var_1_1: type_1_1,
…,
var_n_1: type_n_1}
| …
| <pgname_m’transname_m> of int * {var_m_1: type_m_1,
…,
var_m_j: type_m_j}type markings = unit
type subnet = BindElem
For each transition associated with a monitor, a constructor is declared in the declaration of the type BindElem. Each constructor is a function that takes an integer and a record as arguments and that return something of type BindElem. The integer specifies an instance of the transition, and the record specifies a binding of the variables of the transition. Examples of constructors for binding elements are shown below.
Some places, some transitions
datatype BindElem =
<pgname_1’transname_1> of int * {var_1_1: type_1_1,
…,
var_n_1: type_n_1}
| …
| <pgname_m’transname_m> of int * {var_m_1: type_m_1,
…,
var_m_j: type_m_j}type markings = <cs (t)ms>_1 * <cs (t)ms>_2 * … * <cs (t)ms>_n
type subnet = BindElem * <cs (t)ms>_1 * <cs (t)ms>_2 * … * <cs (t)ms>_n
Data type examples
No places, no transitions
datatype BindElem = unit
type markings = unit
type subnet = unit
Some places, no transitions
datatype BindElem = unit
type markings = Server tms * Jobs ms
type subnet = markings
The data type BindElem is the trivial type unit, which means that the monitor is not associated with any transitions. The data type markings is a product of two types which indicates that the monitor is associated with two place instances. Therefore, a monitor with these data types is associated with two place instances and no transitions.
The color set of the first place (the ordering of places is described above) is Server. The tms indicates that Server is a timed color set. The markings of the first place are timed multi-sets of Server values.
The color set of the second place is Jobs. The ms indicates that Jobs is not a timed color set. The markings of the second place are multi-sets of Jobs values.
No places, some transitions
datatype BindElem =
Arrivals’Arrive of int * {job: Job,
jobs: Jobs}
| Server’Start of int * {job: Job,
jobs: Jobs,
proctime: int}type markings = unit
type subnet = BindElem
The data type BindElem has two constructors, which means that the monitor is associated with two transitions. The data type markings is the trivial type unit which indicates that the monitor is not associated with any place instances. Therefore, a monitor with these data types is associated with and no places and two transitions.
One of the transitions is named Arrive, and it is on page Arrivals. There are two variables, job and jobs, on the arcs that are connected to the transition. The variable job is of type Job, and the variable jobs is of type Jobs.
The other transition is named Start, and it is on page Server. There are three variables, job, jobs, and proctime, on the arcs that are connected to the transition. The types of variable job and jobs are as described above. The variable proctime is of type int.
Some places, some transitions
datatype BindElem =
Arrivals’Arrive of int * {job: Job,
jobs: Jobs}
| Server’Start of int * {job: Job,
jobs: Jobs,
proctime: int}type markings = Server tms * Jobs ms
type subnet = BindElem * Server tms * Jobs ms
The data type BindElem has two constructors, which means that the monitor is associated with two transitions. The data type markings is a product of two types which indicates that the monitor is associated with two place instances. Therefore, a monitor with these data types is associated with and two places and two transitions.
The transitions and places that are associated with this monitor are similar to the places and transitions described above.
Related pages
You must be logged in to post a comment.