archive-org.com » ORG » C » CPNTOOLS.ORG

Total: 415

Choose link from "Titles, links and description words view":

Or switch to "Titles and links view".
  • State space functions << CPN Tools Homepage
    to Node n OGSet NodeDescriptorOptions nodeToStrFun Changes the contents of node descriptors NodeFilterGen Returns template code for defining contents of node descriptors Examples of use Suppose that the State space tools have been used to calculate the full state space for the example net of the Resource allocation example The Evaluate ML tool can be used to generate a string representing the marking of the net that corresponds to Node 3 in the state space If the string is fairly long and therefore difficult to read the ML print function can be used to print the string This node descriptor contains quite a lot of information the first line shows the number of the node each place instance is shown in the form Page name Place name Instance and the marking of every place is shown even if the marking is empty To make the node descriptor more compact you can start by generating and saving template code for defining the contents of node descriptors Open the file containing the template code in a text editor below left Edit the function as desired for example to remove the line with the number of the node and remove newlines after the marking of each place below right Finally string representation options can be changed for place instances below left place markings below center and node descriptors below right Printing the node descriptor for Node 3 will now result in a much more compact representation of the marking where place instances are shown by simple place names empty markings are omitted and the node number is also omitted Arc descriptors An arc descriptor is a string representation of an arc in a state space Arcs are defined in the manual By default an arc descriptor is a string representation showing the source

    Original URL path: http://cpntools.org/documentation/tasks/verification/state_space_functions (2016-04-26)
    Open archived version from archive


  • Limitations << CPN Tools Homepage
    highly recommended that you do not apply state space tools while there are any yellow highlights on places arcs transitions pages or net names If the Replace by subpage tool is applied and the corresponding subpage s contains state space nodes and or state space arcs then the state space elements on the subpage are deleted The calculation of state spaces for timed CPNs can be nondeterministic due to the

    Original URL path: http://cpntools.org/documentation/tasks/verification/statespace_limitations (2016-04-26)
    Open archived version from archive

  • Temporal logic for state spaces << CPN Tools Homepage
    logic facilities is available Note that even though the manual is written for use with another tool much of it is applicable to CPN Tools The manual describes how to install and load the facilities These descriptions do not apply to CPN Tools In version 1 2 and after of CPN Tools it is no longer necessary to install the facilities and the steps for loading the facilities are described

    Original URL path: http://cpntools.org/documentation/tasks/verification/temporal_logic_for_state (2016-04-26)
    Open archived version from archive

  • States and state space nodes << CPN Tools Homepage
    is a marking of the net i e a distribution of tokens on the places of the net Each node in a state space represents a state marking of the corresponding CPN It is possible to transfer states between the simulator and the state space tool Nodes i e states in a state space are denoted by positive integers By convention 1 denotes the initial node of the state space i e node 1 corresponds to the initial state of the corresponding CPN Transferring states from state space to simulator To transfer a node from the state space tool to the simulator apply the State space to simulator tool to a page in a net The number in the State space to simulator tool in the State space tools is the number of the node in the state space that will be transferred from the state space tool to the simulator when the tool is applied A status bubble will indicate whether or not the state was transferred successfully To change the number of the node to be transferred change the option for the State space to simulator tool Transferring states from simulator to state space To transfer a state

    Original URL path: http://cpntools.org/documentation/tasks/verification/transfer_states (2016-04-26)
    Open archived version from archive

  • Bluetooth Network << CPN Tools Homepage
    that we provide them as inspiration The model of a given Bluetooth network is composed of submodels of the master and slave devices The process of AMA reallocation is modeled as well as the data transmitting via ether Static allocation of PMA is employed The model is described in Bereznyuk M V Gupta K K Zaitsev D A Effectiveness of Bluetooth Address Space Usage In Proceedings of 20th International Conference

    Original URL path: http://cpntools.org/documentation/examples/bluetooth_network (2016-04-26)
    Open archived version from archive

  • Dining philosophers example << CPN Tools Homepage
    different queries are illustrated The CPN model describes how a number of processes philosophers share common resources chopsticks The Dining Philosophers is one of the traditional examples used by computer scientists to illustrate new concepts in the area of synchronisation and concurrency The example is taken from Sect 1 6 of Vol 2 of K Jensen Coloured Petri Nets Basic Concepts Analysis Methods and Practical Use Monographs on Theoretical Computer

    Original URL path: http://cpntools.org/documentation/examples/dining_philosophers (2016-04-26)
    Open archived version from archive

  • Monitored dining philosophers example << CPN Tools Homepage
    Communication using monitors and Comms CPN The two user defined monitors for this net are named AppletComm and Deadlock The AppletComm monitor is associated with all five transitions on page System and the Deadlock monitor is associated with two transitions and two places on the same page AppletComm monitor The AppletComm monitor is associated with all of the transitions in the net This means that the predicate function for the monitor will be invoked after every step in a simulation Initialization function The initialization function is called once before a simulation starts It checks to see if a communication connection exists between CPN Tools and the applet If there is a connection then the connection is closed and the reference variable connected is updated to indicate that the connection has been closed The ConnManagementLayer closeConnection function is one of the Comms CPN functions fun init if connected true then ConnManagementLayer closeConnection Conn 1 connected false else Predicate function The predicate function is invoked after every step in a simulation and it returns true each time one of the transitions in the net occurs fun pred bindelem let fun predBindElem System LeftFirst 1 p true predBindElem System LeftScnd 1 p true predBindElem System PutDown 1 p true predBindElem System RightFirst 1 p true predBindElem System RightScnd 1 p true predBindElem false in predBindElem bindelem end Observation function The observation function is invoked each time the predicate function returns true and it returns a pair of strings The first value in the pair is a string representation of the variable p which is of type PH and the second value is a string that indicates what event just occurred i e which transition just occurred The function PH mkstr is one of the Color set functions fun obs bindelem let fun obsBindElem System LeftFirst 1 p PH mkstr p gotleft obsBindElem System LeftScnd 1 p PH mkstr p eat obsBindElem System PutDown 1 p PH mkstr p think obsBindElem System RightFirst 1 p PH mkstr p gotright obsBindElem System RightScnd 1 p PH mkstr p eat obsBindElem in obsBindElem bindelem end Action function Whenever the predicate function returns true the value that is returned by the observation function will be passed to the action function The action function will check whether a connection to the applet has been established If there is no connection then ConnManagementLayer acceptConnection function is invoked and the simulation will be blocked until the applet opens a connection on port 9000 When a connection has been established then the connected reference variable is set to true Finally the send to applet function is invoked with the string values that were passed from the observation function The send to applet is defined in a declaration as described above fun action s1 s2 if not connected then ConnManagementLayer acceptConnection Conn 1 9000 connected true else send to applet s1 s2 Stop function The stop function is invoked when simulation stop criteria are fulfilled If there is still a connection between

    Original URL path: http://cpntools.org/documentation/examples/dining_philosophers_monit (2016-04-26)
    Open archived version from archive

  • Dining philosophers example << CPN Tools Homepage
    suited as an introduction to state spaces also called occurrence graphs The analysis of the state space is described in great detail and a large number of different queries are illustrated The CPN model describes how a number of processes philosophers share common resources chopsticks The Dining Philosophers is one of the traditional examples used by computer scientists to illustrate new concepts in the area of synchronisation and concurrency which

    Original URL path: http://cpntools.org/documentation/examples/dining_philosophers_sp (2016-04-26)
    Open archived version from archive



  •