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".
  • Calculating the state space << CPN Tools Homepage
    the options for the Calculate state space tool If calculation was successful a green status bubble will appear in the index Position the mouse cursor on top of the status bubble to see generation statistics If some of the stop or branching criteria are fulfilled then a yellow status bubble will appear in the index If calculation failed a red status bubble will appear in the index Position the mouse

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


  • Attributes and options in state space tool << CPN Tools Homepage
    string representation options below Setting string representation options The string representation options allow the user to specify how the st functions which are fully described in the state space tool manual will work The st functions are used for the standard reports generated by the Save state space report tool Hence changing these options also influences the state space report To set a string representation option create an auxiliary text containing the appropriate string representation functions described in the manual and evaluate the function using the Evaluate ML tool Next we show an example of how to change the string representation of place instances in the state space tool Evaluating the top auxiliary text shows the default string representation for the place Think on the first 1 instance of the page named Page in the example CPN for the Dining philosophers example Evaluating the middle auxiliary text will change the string representation function for place instances Evaluating the bottom auxiliary text shows the new string representation for the place Think Setting stop and branching options The stop options allow you to determine when the calculation of a state space stops This happens when all nodes have been processed or when

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

  • Draw state spaces with CPN Tools << CPN Tools Homepage
    hidden again using techniques similar to hiding a node descriptor If the cursor hovers over a node descriptor or an arc descriptor the element which the descriptor belongs to will be highlighted Displaying nodes and arcs from lists The Display partial state space tool is used to draw arbitrary groups of nodes or arcs The tool must be applied to an auxiliary text that contains a CPN ML expression that will evaluate to either a list of node numbers or a list of arc numbers The CPN ML expression can be very simple or more complex Here are a couple of examples of CPN ML expressions that will return lists of nodes for the example net for the Dining philosophers example Applying the tool to the expression 1 2 3 will result in nodes 1 2 and 3 being drawn if they are not already on the page If the tool is applied to the other CPN ML expression in the figure the expression will first be evaluated and it will return a list of nodes corresponding to markings in which the marking of the place Eat contains the multiset 1 ph 1 All of the nodes in the list will then be drawn If the tool is applied to a CPN ML expression that contains syntax errors or that does not return a list of nodes or arcs then an error message will be shown next to a status bubble Here is the error message after the tool was applied to the expression 1 2 3 which is missing the right bracket Active and inactive state space elements State space nodes and arcs can only be drawn after you Enter the state space tool and Calculating the state space State space elements that are drawn after entering the state

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

  • Draw State Spaces with Graphviz << CPN Tools Homepage
    nodelist Node list Exports the nodes in the list OGtoGraphviz ExportNodePath filename nodelist Checks whether the nodes form a path i e whether there is an arc between each node and its immediate successor in the list If this is the case the nodes and arcs are exported If there are multiple arcs between two neighbouring nodes they are all exported OGtoGraphviz ExportArcs filename arclist Arc list Exports the arcs and their source and destination nodes OGtoGraphviz ExportArcPath filename arclist Checks whether the arcs form a path i e whether the destination node of an arc is the same as the source node of its immediate successor in the list If this is the case the arcs and their source and destination nodes are exported OGtoGraphviz ExportSuccessors filename nodelist Exports the nodes in the list their immediate successor arcs and their immediate successor nodes The function only exports nodes and arcs which have already been calculated OGtoGraphviz ExportPredecessors filename nodelist Analogous to OGtoGraphviz ExportSuccessors OGtoGraphviz ExportStateSpace filename Exports the nodes and arcs in the state space that has been calculated The calculated state space may only be a partial state space OGtoGraphviz ExportSccGraph filename Exports the nodes and arcs in the Scc graph Nodes and Arcs are defined in Chapter 3 of the manual for the state space tool Using the Export Functions Evaluating the functions above will export the desired graph structure to a file The Create Auxiliary Text and Evaluate ML tools can be used to evaluate the functions The file that is created adheres to the DOT language that is the input file format for the Graphviz tools Using Graphviz The following is a very brief introduction to how to use Graphviz For more information about using Graphviz see the web site for Graphviz Download and Install

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

  • Enter the state space tool << CPN Tools Homepage
    All places transitions and pages in the net must have non empty names Places transitions and pages must have unique ML names see Naming policy Syntactical errors and non unique ML names will be identified during Syntax checking To enter the state space tool apply the Enter state space tool to one of the sheets containing a page from the net Entering the state space tool will take some time

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

  • Make state space queries << CPN Tools Homepage
    liveness and fairness properties using standard queries and non standard queries can be created by writing CPN ML functions Queries are made by creating auxiliary text containing the query function and then using the Evaluate ML tool to evaluate the text The query functions that are available are described in the state space tool manual Exceptions The ExcAvlLookup exception will be raised if you attempt to access a node that

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

  • Nondeterministic nets << CPN Tools Homepage
    can be made If the ran function is used to choose a random element from a small color set then there are only a few values in the color set to choose from If a random number is to be chosen from a relatively short interval using the Discrete function then there are only few integers to choose from It is not however obvious to the state space tool that there are only a limited number of possible outcomes nor is there any way to ensure that the state space tool considers every possibility The best that the state space tool can do when calculating the successors of a given marking is evaluate Transition inscriptions for a given binding of the transition s variables and see what is returned Since the result of evaluating a transition s inscriptions may not be uniquely determined by the given binding it is not possible to deterministically calculate the state space Making nondeterministic nets deterministic In some cases it is possible to make a nondeterministic net deterministic in order to make it better suited for state space analysis Some examples are shown below Removing random elements from a list Suppose that a function is used to randomly determine which element should be removed from a list on a place For example in the following example the Discrete function is used to determine the index number of the element to be removed This is an example of a nondeterministic net If you know that there is a relatively small upper limit on the length of the lists that can be found on the place then it is possible to make the above nondeterministic net deterministic as follows Rather than using a function to randomly pick an the index of the element from a list a

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

  • Saving a standard state space report << CPN Tools Homepage
    determined by the options for the Save state space report tool The textual format of place and transition names in a report can be changed by setting the string representation options To set these options you must Attributes and options in state space tool Example The full state space report for the Dining philosophers example example CPN looks like this Statistics Occurrence Graph Nodes 11 Arcs 30 Secs 0 Status Full Scc Graph Nodes 1 Arcs 0 Secs 0 Boundedness Properties Best Integers Bounds Upper Lower Page Eat 1 2 0 Page Think 1 5 3 Page Unused 1 5 1 Best Upper Multi set Bounds Page Eat 1 1 ph 1 1 ph 2 1 ph 3 1 ph 4 1 ph 5 Page Think 1 1 ph 1 1 ph 2 1 ph 3 1 ph 4 1 ph 5 Page Unused 1 1 cs 1 1 cs 2 1 cs 3 1 cs 4 1 cs 5 Best Lower Multi set Bounds Page Eat 1 empty Page Think 1 empty Page Unused 1 empty Home Properties Home Markings All Liveness Properties Dead Markings None Dead Transitions Instances None Live Transitions Instances All Fairness Properties Page Put 1

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



  •