Created
October 23, 2016 06:48
-
-
Save psychon/828d4db68db790bcda117dd17815f602 to your computer and use it in GitHub Desktop.
Help output for all modules in APT
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Usage: apt ac <net> | |
| net The Petri net that should be examined | |
| Check if a Petri net is asymmetric-choice. | |
| A Petri net is an asymmetric choice net if ?p?,p??P: p???p???? ? p???p?? ? p???p?? | |
| ----------- | |
| Usage: apt backwards_persistent <pn_or_ts> | |
| pn_or_ts The Petri net or LTS that should be examined | |
| Check if a Petri net or LTS is persistent. | |
| A LTS is persistent if for all reachable states s and enabled labels a, b (a?b), there is a state r so that both s[ab>r and s[ba>r. A Petri net is persistent if its reachability graph is persistent. | |
| ----------- | |
| Usage: apt bcf <pn> | |
| pn The Petri net that should be examined | |
| Check if a Petri net is behaviourally conflict free (BCF). | |
| A Petri net is BCF if in every reachable marking M and for any enabled pair of transitions (M[a>, M[b> and a ? b), the presets of the transitions is disjoint (?a??b=?). | |
| ----------- | |
| Usage: apt bicf <pn> | |
| pn The Petri net that should be examined | |
| Check if a Petri net is binary conflict free (BiCF). | |
| A Petri net is BiCF if in every reachable marking M and for any enabled pair of transitions (M[a>, M[b> and a ? b), enough tokens for both transitions are present (?p?P: M(p) ? F(p, a) + F(p, b)). | |
| ----------- | |
| Usage: apt bisimulation <pnOrLts1> <pnOrLts2> | |
| pnOrLts1 The first Petri net that should be examined | |
| pnOrLts2 The second Petri net that should be examined | |
| Check if the reachability graphs of two bounded labeled Petri nets or of two LTS or a combination of both are bisimilar | |
| ----------- | |
| Usage: apt bistate_philnet_generator <n> [<pn>] | |
| n The argument for the Petri net generator | |
| pn Optional file name for writing the output to | |
| Construct a Petri net for a bistate philosopher's net of a given size. | |
| ----------- | |
| Usage: apt bitnet_generator <n> [<pn>] | |
| n The argument for the Petri net generator | |
| pn Optional file name for writing the output to | |
| Construct a Petri net for a bit nets of a given size. | |
| ----------- | |
| Usage: apt bounded <pn> [<k>] | |
| pn The Petri net that should be examined | |
| k If given, k-boundedness is checked | |
| Check if a Petri net is bounded or k-bounded. A Petri net is bounded if there is an upper limit for the number of token on each place. It is k-bounded if this limit isn't bigger than k. | |
| ----------- | |
| Usage: apt cf <net> | |
| net The Petri net that should be examined | |
| This module tests if a plain Petri net is conflict-free. That is: | |
| \forall s \in S: \mid s^\bullet \mid \leq 1 \vee s^\bullet \subset ^\bullet s | |
| ----------- | |
| Usage: apt check <maxSeconds> <generator> [<attribute1>] [<attribute2>] [<attribute3>] [<attribute4>] [<attribute5>] [<attribute6>] [<attribute7>] | |
| maxSeconds Max. execution time in seconds | |
| generator Generator | |
| attribute1 Attribute 1 | |
| attribute2 Attribute 2 | |
| attribute3 Attribute 3 | |
| attribute4 Attribute 4 | |
| attribute5 Attribute 5 | |
| attribute6 Attribute 6 | |
| attribute7 Attribute 7 | |
| Supported generators: | |
| bitnet, chance, cycle, quadPhilgen, smartchance, tnetgen2, tnetgen3, triPhilgen | |
| Supported attributes: | |
| bounded, !bounded, freeChoice, !freeChoice, isolated, !isolated, k-marking, !k-marking, persistent, !persistent, plain, !plain, pure, !pure, reversible, !reversible, snet, !snet, !strongly_k-separable, stronglyLive, !stronglyLive, tnet, !tnet, !weakly_k-separable | |
| (Choose a natural number for k) | |
| Short description of each generator: | |
| bitnet : Generates a bit net with varying number of bits. | |
| chance : Generates a Petri net through random with a chance of finding a valid net by reacting to result of last generated Petri net. | |
| cycle : Generates a cycle net with varying size of the cycle. | |
| quadPhilgen : Generates a philosoph net with varying number of philosophs and four states. | |
| smartchance : Like chance but more complex reaction to analyse results of last generated Petri nets. | |
| tnetgen2 : Generates t-nets with varying number of maximum places and tokens. | |
| (maximum transitions will be set to 'maximum places * 2') | |
| tnetgen3 : Generates t-nets with varying number of maximum places, transitions and tokens. | |
| triPhilgen : Generates a philosoph net with varying number of philosophs and three states. | |
| For detailed descriptions see analysis modules and generator packet. | |
| Example calls: | |
| apt check 5 chance 'snet' '!tnet' | |
| apt check 10 chance '2-marking' | |
| ----------- | |
| Usage: apt check_all_cycle_prop <pn> | |
| pn The Petri net that should be examined | |
| Check if all smallest cycles have same Parikh vectors, if all smallest cycles have same or mutually disjoint Parikh vectors and it computes Parikh vectors of smallest cycles | |
| ----------- | |
| Usage: apt compute_pvs <graph> [<algo>] | |
| graph The Petri net or LTS that should be examined | |
| algo Select the algorithm to use. Possible options are a depth-first search algorithm ('dfs'); an adapted Floyd-Warshall algorithm ('floyd_warshall'); Johnson's algorithm ('johnson') The default value is 'johnson'. | |
| Compute parikh vectors of smallest cycles of a Petri net or LTS | |
| ----------- | |
| Usage: apt concurrent_coverability_graph <pn> [<dot>] | |
| pn The Petri net that should be examined | |
| dot Optional file name for writing the output to | |
| Calculate the concurrent coverability graph of a Petri net in the step semantics. In the step semantics, instead of individual transitions, sets of transitions called 'a step' are fired. When a step fires, first all of its transition consume token and only afterwards produce tokens. Put differently, on each place at least as many token have to be present as the sum of the arc weights of the transitions in a step require. | |
| ----------- | |
| Usage: apt connected_bitnet_generator <n> [<pn>] | |
| n The argument for the Petri net generator | |
| pn Optional file name for writing the output to | |
| Construct a Petri net for a connected bit net of a given size. | |
| ----------- | |
| Usage: apt conpres <net> | |
| net The Petri net that should be examined | |
| This module checks if a Petri net is concurrency-preserving.That is: for every transition t there are as many places in the preset as in the postset of t. | |
| ----------- | |
| Usage: apt coverability_graph <pn> [<lts>] | |
| pn The Petri net that should be examined | |
| lts Optional file name for writing the output to | |
| Compute a Petri net's coverability graph | |
| ----------- | |
| Usage: apt covered_by_invariant <net> <inv> [<algo>] | |
| net The Petri net that should be examined | |
| inv Parameter 's' for s-invariants and 't' for t-invariants. | |
| algo Parameter 'f' for farkas algorithm and 'p' for the adapted farkas algorithm of pipe. The default value is 'p'. | |
| Check if a Petri net is covered by an S-invariant or a T-invariant. | |
| An invariant is a semi-positive vector from the nullspace of the incidence matrix C. For a T-invariant x?0 this means C*x=0 and a S-invariant x?0 satisfies C?*x=0. This module checks if a positive S- or T-invariant exists, that is an invariant without an entry equal to zero. | |
| ----------- | |
| Usage: apt cycle_generator <n> [<init>] [<pn>] | |
| n The argument for the Petri net generator | |
| init The number of token in the initial marking The default value is '1'. | |
| pn Optional file name for writing the output to | |
| Construct a Petri net for a cycle of a given size with a given number of initial token. | |
| ----------- | |
| Usage: apt cycles_same_disjoint_pv <graph> [<algo>] | |
| graph The Petri net or LTS that should be examined | |
| algo Select the algorithm to use. Possible options are a depth-first search algorithm ('dfs'); an adapted Floyd-Warshall algorithm ('floyd_warshall'); Johnson's algorithm ('johnson') The default value is 'johnson'. | |
| Check if the smallest cycles of a Petri net or LTS have the same or mutually disjoint parikh vectors | |
| ----------- | |
| Usage: apt cycles_same_pv <graph> [<algo>] | |
| graph The LTS or Petri net that should be examined | |
| algo Select the algorithm to use. Possible options are a depth-first search algorithm ('dfs'); an adapted Floyd-Warshall algorithm ('floyd_warshall'); Johnson's algorithm ('johnson') The default value is 'johnson'. | |
| Check if the smallest cycles of Petri net or LTS have the same parikh vector | |
| ----------- | |
| Usage: apt deterministic <lts> | |
| lts The LTS that should be examined | |
| Check if a LTS is deterministic | |
| ----------- | |
| Usage: apt draw <pn_or_ts> [<dot>] | |
| pn_or_ts The Petri net or labeled tansition system that should be examined | |
| dot Optional file name for writing the output to | |
| Convert a Petri net or LTS to the Dot format used by Graphviz | |
| ----------- | |
| Usage: apt examine_lts <lts> | |
| lts The LTS that should be examined | |
| Perform various tests on a transition system at once | |
| ----------- | |
| Usage: apt examine_pn <pn> | |
| pn The Petri net that should be examined | |
| Perform various tests on a Petri net at once | |
| ----------- | |
| Usage: apt extend_deterministic_persistent <ts> [<rounds>] [<extended_ts>] | |
| ts The deterministic transition system that should be extended | |
| rounds Maximum allowed number of processing rounds that add new states The default value is 'unlimited'. | |
| extended_ts Optional file name for writing the output to | |
| Extend a transition system to an deterministic persistent transition system. | |
| ----------- | |
| Usage: apt extend_lts <lts> <g> <mode> <state_file> [<extended_lts>] | |
| lts The LTS that is extended | |
| g Maximum number of new nodes | |
| mode The mode (next, next_valid, next_minimal_valid) | |
| state_file The file to load/save the state from/to | |
| extended_lts Optional file name for writing the output to | |
| Generate extensions to a given LTS that are reversible, persistent. Also, all smallest cycles share the same parikh vector. This module can run in three different modes: It can generate the next possible extension to the given LTS, the next extension that satisfies the above properties or the next satisfying extension that is also minimal among satisfying extensions. | |
| ----------- | |
| Usage: apt factorize <lts> [<factor1>] [<factor2>] | |
| lts The connected LTS that should factorized | |
| factor1 Optional file name for writing the output to | |
| factor2 Optional file name for writing the output to | |
| Decompose a LTS into its factors (if possible) | |
| ----------- | |
| Usage: apt fc <net> | |
| net The Petri net that should be examined | |
| Check if a Petri net is free-choice. That is: \forall t1,t2 \in T: ^{\bullet}t1 \Cap ^{\bullet}t2 \neq \emptyset \Rightarrow ^{\bullet}t1 \eq ^{\bullet}t2. | |
| ----------- | |
| Usage: apt find_words <options> <operation> <alphabet> | |
| options options | |
| operation Choose between printing all 'minimal_unsolvable' words or all 'solvable' words | |
| alphabet Letters that should be part of the alphabet | |
| Print either minimal unsolvable or all solvable words of some class. | |
| This module only prints a subset of all words. For this, an equivalence relation on words is used were two words are equivalent if one can be created from the other by replacing letters with other letters. For example, 'abc' and 'abd' are equivalent in this sense, since c->d turns one into the other. | |
| More concretely, words are generated so that the last letter of the word is the first letter of the alphabet. Then, the next new letter from the end is the second letter of the alphabet, and so on. | |
| Example calls: | |
| apt find_words safe solvable abc: Print all words solvable by safe Petri nets over the alphabet {a,b,c} | |
| apt find_words none unsolvable ab: Print all minimally unsolvable words over the alphabet {a,b} | |
| ----------- | |
| Usage: apt fire_sequence <sequence> <pn> | |
| sequence Sequence that should be fired | |
| pn The Petri net that should be examined | |
| Try to fire a given firing sequence on a Petri net.. This module tries to fire a given sequence of transitions in a Petri net. It will report the longest enabled prefix of the sequence and print the marking that is reached at the end. | |
| Format descriptions of parameters: | |
| sequence: | |
| Words can be specified in two different forms. | |
| The first format includes explicit delimiters between events. For delimiters, either commas, semicolons or spaces are allowed. An example of this format would be 'a, b, c'. Note that leading and trailing spaces are skipped. | |
| The second format expects events to be individual letters. The special prefix : is used to indicate this format. An example would be ':abc'. | |
| ----------- | |
| Usage: apt gdiam <lts> <T'> | |
| lts The LTS to check | |
| T' Set of labels to check | |
| Check if for the given LTS = (S, ->, T, s0) for each pair of labels a in T', b in T\T' the general diamond property holds. | |
| Format descriptions of parameters: | |
| T': | |
| Words can be specified in two different forms. | |
| The first format includes explicit delimiters between events. For delimiters, either commas, semicolons or spaces are allowed. An example of this format would be 'a, b, c'. Note that leading and trailing spaces are skipped. | |
| The second format expects events to be individual letters. The special prefix : is used to indicate this format. An example would be ':abc'. | |
| ----------- | |
| Usage: apt generate_reverse_arc <lts> <event> <reverseEvent> [<lts>] | |
| lts The LTS that should be examined | |
| event The event to look for | |
| reverseEvent The event for the reverse arcs | |
| lts Optional file name for writing the output to | |
| Generate reverse arcs for all arcs with a given label. For all arcs labelled with the given event, an arc in the opposite direction labelled with the given reverseEvent is added. | |
| ----------- | |
| Usage: apt help [<module_name>] | |
| module_name Module name for which you want help The default value is 'help'. | |
| Get information about a module | |
| ----------- | |
| Usage: apt homogeneous <net> | |
| net The Petri net that should be examined | |
| Check if a Petri net is homogeneous. | |
| A Petri net is an homogeneous net if ?p?P:?t?,t??p?: F(p,t?)=F(p,t?) | |
| ----------- | |
| Usage: apt invariants <pn> <inv> [<algo>] | |
| pn The Petri net that should be examined | |
| inv Parameter 's' for s-invariants and 't' for t-invariants. | |
| algo Parameter 'f' for Farkas algorithm and 'p' for the adapted Farkas algorithm of PIPE. The default value is 'p'. | |
| Compute a generator set of S- or T-invariants. | |
| An invariant is a semi-positive vector from the nullspace of the incidence matrix C. For a T-invariant x?0 this means C*x=0 and a S-invariant x?0 satisfies C?*x=0. This module finds the set of generators for all S- or T-invariants. | |
| ----------- | |
| Usage: apt inverse_generator <pn> [<pn>] | |
| pn The argument for the inverse generator | |
| pn Optional file name for writing the output to | |
| Construct the inverse of a Petri net | |
| ----------- | |
| Usage: apt isolated <pn> | |
| pn The Petri net that should be examined | |
| Check if a Petri net contains isolated elements. A Petri net contains isolated elements when at least one element's pre- and postset is empty. | |
| ----------- | |
| Usage: apt isolated_elements <graph> | |
| graph The graph that should be examined | |
| Find isolated elements in a graph | |
| ----------- | |
| Usage: apt isomorphism <pn_or_ts1> <pn_or_ts2> [<dontCheckLabels>] | |
| pn_or_ts1 The first Petri net or transition system that should be examined | |
| pn_or_ts2 The second Petri net or transition system that should be examined | |
| dontCheckLabels do not check arc labels (default is to check labels) | |
| Check if two Petri nets have isomorphic reachability graphs | |
| ----------- | |
| Usage: apt k_bounded <pn> | |
| pn The Petri net that should be examined | |
| Find the smallest k for which a Petri net is k-bounded. A Petri net is bounded if there is an upper limit for the number of token on each place. It is k-bounded if this limit isn't bigger than k. | |
| ----------- | |
| Usage: apt k_marking <pn> | |
| pn The petri net that should be examined | |
| Compute the largest k for which M0 is a k-marking. | |
| e.g.: Output: Largest k for which M0 is a k-marking: 1 | |
| ----------- | |
| Usage: apt label_separation <lts> <T'> | |
| lts The LTS to check | |
| T' Set of labels to check | |
| Check if for all states s != s' it is impossible to go from s to s' using only labels from T' (disregarding arc direction) as well as only labels outside T' (disregarding arc direction) | |
| Format descriptions of parameters: | |
| T': | |
| Words can be specified in two different forms. | |
| The first format includes explicit delimiters between events. For delimiters, either commas, semicolons or spaces are allowed. An example of this format would be 'a, b, c'. Note that leading and trailing spaces are skipped. | |
| The second format expects events to be individual letters. The special prefix : is used to indicate this format. An example would be ':abc'. | |
| ----------- | |
| Usage: apt language_equivalence <pn_or_ts1> <pn_or_ts2> | |
| pn_or_ts1 The first Petri net or transition system that should be examined | |
| pn_or_ts2 The second Petri net or transition system that should be examined | |
| Check if two Petri nets generate the same language | |
| ----------- | |
| Usage: apt limited_unfolding <lts> [<lts>] | |
| lts The LTS that should be unfolded | |
| lts Optional file name for writing the output to | |
| Calculate the limited unfolding of a lts. The limited unfolding, as defined in 'Petri Net Synthesis' (E. Badouel, L. Bernardinello and P. Darondeau) eliminates paths that reach the same state (where possible) without changing the language of the LTS. | |
| ----------- | |
| Usage: apt lts_convert <input_format> <output_format> <input> [<output>] | |
| input_format The format of input. | |
| output_format The format of output. | |
| input The input string that should be converted. | |
| output Optional file name for writing the output to | |
| Convert between transition system file formats | |
| Supported file formats: | |
| - apt | |
| - dot (only as output format) | |
| - petrify | |
| - synet | |
| - tikz (only as output format) | |
| ----------- | |
| Usage: apt matrices <pn> [<format>] [<output>] | |
| pn The Petri net that should be examined | |
| format The file format of the printed matrices | |
| output Optional file name for writing the output to | |
| Calculate forward, backward, and incidence matrices. The matrices can also be printed in the R and MATLAB format. | |
| ----------- | |
| Usage: apt nonpure <pn> | |
| pn The Petri net that should be examined | |
| Check if a Petri net is nonpure but only simple sideconditions. A Petri net is nonpure when there exists atleast one self-loop. A sidecondition is simple, when both arcsof the self-loop have a weight of 1. | |
| ----------- | |
| Usage: apt on <net> | |
| net The Petri net that should be examined | |
| This module checks if a Petri net is output-nonbranching. That is: | |
| \forall s \in S: \mid s^\bullet \mid \leq 1 | |
| ----------- | |
| Usage: apt overapproximate_synthesize <options> <lts> [<pn>] | |
| options Comma separated list of options | |
| lts The LTS that should be synthesized to a Petri Net | |
| pn Optional file name for writing the output to | |
| Synthesize the minimal Petri Net overapproximation from a transition system. | |
| Supported options are: none, [k]-bounded, safe, [k]-marking, pure, plain, tnet, generalized-marked-graph (gmg), marked-graph (mg), generalized-output-nonbranching (gon) output-nonbranching (on), conflict-free (cf), homogeneous, behaviourally-conflict-free (bcf), binary-conflict-free (bicf), upto-language-equivalence (language, le), minimize (minimal), verbose and quick-fail. | |
| The meaning of these options is as follows: | |
| - none: No further requirements are made. | |
| - [k]-bounded: In every reachable marking, every place contains at most [k] tokens. | |
| - safe: Equivalent to 1-bounded. | |
| - [k]-marking: The initial marking of each place is a multiple of k. | |
| - pure: Every transition either consumes or produces tokens on a place, but not both (=no side-conditions). | |
| - plain: Every flow has a weight of at most one. | |
| - tnet: Every place's preset and postset contains at most one entry. | |
| - generalized-marked-graph: Every place's preset and postset contains exactly one entry. | |
| - marked-graph: generalized-marked-graph + plain. | |
| - generalized-output-nonbranching: Every place's postset contains at most one entry. | |
| - output-nonbranching: generalized-output-nonbranching + plain. | |
| - conflict-free: The Petri net is plain and every place either has at most one entry in its postset or its preset is contained in its postset. | |
| - homogeneous: All outgoing flows from a place have the same weight. | |
| - behaviourally-conflict-free: In every reachable marking, the preset of activated transitions is disjoint. | |
| - binary-conflict-free: For every reachable marking and pair of activated transitions, enough tokens for both transitions are present. | |
| - minimize: The Petri net has as few places as possible. | |
| The following options only affect the output, but not the produced Petri net: | |
| - verbose: Print details about each calculated region/place. | |
| - quick-fail: Stop the algorithm when the result 'success: No' is clear. | |
| Example calls: | |
| apt overapproximate_synthesize none lts.apt | |
| apt overapproximate_synthesize 3-bounded lts.apt | |
| apt overapproximate_synthesize pure,safe lts.apt | |
| ----------- | |
| Usage: apt persistent <pn_or_ts> | |
| pn_or_ts The Petri net or LTS that should be examined | |
| Check if a Petri net or LTS is persistent. | |
| A LTS is persistent if for all reachable states s and enabled labels a, b (a?b), there is a state r so that both s[ab>r and s[ba>r. A Petri net is persistent if its reachability graph is persistent. | |
| ----------- | |
| Usage: apt plain <pn> | |
| pn The Petri net that should be examined | |
| Check if a Petri net is plain. A Petri net is plain if all arc weights are at most 1. | |
| ----------- | |
| Usage: apt pn_analysis <pn> <g> [<k>] [<randomly>] [<T-system>] | |
| pn The Petri net that should be examined | |
| g maximum size of places of the checked T-systems | |
| k maximum number of token of the checked T-systems | |
| randomly Parameter, which say, that a randomly selected T-system is checked with g as maximum size of places. The default value is ''. | |
| T-system Optional file name for writing the output to | |
| Output a T-system of size g, which has a reachability graph, which is isomorph to the reachability graph of the input Petri net | |
| ----------- | |
| Usage: apt pn_convert <input_format> <output_format> <input> [<output>] | |
| input_format The format of input. | |
| output_format The format of output. | |
| input The input string that should be converted. | |
| output Optional file name for writing the output to | |
| Convert between Petri net file formats | |
| Supported file formats: | |
| - apt | |
| - baggins (only as output format) | |
| - dot (only as output format) | |
| - genet | |
| - lola | |
| - petrify | |
| - pnml | |
| - synet | |
| - tikz (only as output format) | |
| ----------- | |
| Usage: apt pn_extend_and_synthesize <options> <lts> <pn> [<pn>] | |
| options Comma separated list of options | |
| lts The LTS that should be synthesized to a Petri Net | |
| pn The Petri net whose places should be re-used | |
| pn Optional file name for writing the output to | |
| Synthesize a Petri Net from a transition system, reusing places of a PetriNet. This module gets a PetriNet as input and tries to re-use the places of the given PetriNet in the synthesized result. | |
| ----------- | |
| Usage: apt ppspresynthesis <lts> | |
| lts Input LTS | |
| Checks if it is infeasible to synthesize a plain, pure and safe Petri net from the given transition system. The following properties are checked: | |
| (B) If M'[a>M and M''[b>M then [b>M' <=> [a>M'' | |
| (D) If M[a> and M[b> then for any K: (K[ab> <=> K[ba>) | |
| (F) If M[wv> and M[vw> and M[wc> and M[vc> then M[wvc>M' and M[vwc>M' and M[c> | |
| with transitions a, b, c and sequences v, w. | |
| ----------- | |
| Usage: apt product_async <lts1> <lts2> [<product>] | |
| lts1 The first LTS of the product | |
| lts2 The second LTS of the product | |
| product Optional file name for writing the output to | |
| Compute the asynchronous product of two LTS | |
| ----------- | |
| Usage: apt product_sync <lts1> <lts2> [<product>] | |
| lts1 The first LTS of the product | |
| lts2 The second LTS of the product | |
| product Optional file name for writing the output to | |
| Compute the synchronous product of two LTS | |
| ----------- | |
| Usage: apt pure <pn> | |
| pn The Petri net that should be examined | |
| Check if a Petri net is pure. A Petri net is pure if there are no side conditions. A side condition is a loop between a place p and a transition t (F(p,t)> 0 and F(t,p)>0). | |
| ----------- | |
| Usage: apt quadstate_philnet_generator <n> [<pn>] | |
| n The argument for the Petri net generator | |
| pn Optional file name for writing the output to | |
| Construct a Petri net for a quadstate philosopher's net of a given size. | |
| ----------- | |
| Usage: apt random_t_net_generator <g> [<k>] [<t-net>] | |
| g maximum count of places of the returned t-net. | |
| k maximum number of token of a place in the t-net. | |
| t-net Optional file name for writing the output to | |
| Construct a T-net or T-system (if k given) of size g. | |
| ----------- | |
| Usage: apt reachability_graph <pn> [<lts>] | |
| pn The Petri net that should be examined | |
| lts Optional file name for writing the output to | |
| Compute a Petri net's reachability graph | |
| ----------- | |
| Usage: apt regular_language_to_lts <lang> [<lts>] | |
| lang The regular language to transform | |
| lts Optional file name for writing the output to | |
| Represent a regular language as a transition system | |
| Format descriptions of parameters: | |
| lang: | |
| Let's start with an example: (abc?)* | |
| This regular expression describes the language where every word consists of a sequence of 'a', then 'b', then an optional 'c'. This sequence can be repeated infinitely often or never at all. | |
| As this example demonstrates, single letter events are just entered as is. White space is not significant and gets ignored. Concatenation is expressed by writing some sub-expressions next to each other. If you need an event consisting of more than just a single letter, enclose it in angle brackets like this: <event> | |
| Supported operations are: | |
| - !a is the negation of 'a', this means any word except a single 'a' is allowed (if the regex contains other symbols, like 'b' or 'c', then they may also occur in this words) | |
| - @a is the prefix closure of 'a', this means that all prefixes of words in the language are also allowed) | |
| - a* is the Kleene closure of 'a', including the empty word. This means any sequence of 'a' is allowed. | |
| - a+ is the Kleene plus of 'a' (without explicitly including the empty word). | |
| - a{x} means repeating 'a' x times (with an integer x). | |
| - a{x,} means repeating 'a' at least x times (with an integer x). | |
| - a{x,y} means repeating 'a' between x and y times (with integers x and y). | |
| - a? matches either 'a' or nothing, meaning that 'a' is made optional. | |
| - a|b matches either 'a' or 'b'. | |
| - a&b means the intersection which matches if both subexpresssion (a and b) match (this example never matches). | |
| - ~ describes the empty language | |
| - $ is the language containing only the empty word | |
| The precedence of the operators is: | |
| ! binds strongest, then * + and ? and repetition with {}, then concatenation, then intersection and at last the union operator. Parentheses can be used to influence the precedence, for example in (a(bc?)+)*. | |
| Finally, comments of the form | |
| /* comment */ | |
| and | |
| // comment | |
| are supported. | |
| ----------- | |
| Usage: apt reversible <pn_or_ts> | |
| pn_or_ts The Petri net or LTS that should be examined | |
| Check if a Petri net or LTS is reversible. A LTS is reversible if every reachable state can reach the initial state again. A Petri net is reversible if its reachability graph is reversible. | |
| ----------- | |
| Usage: apt rfc <net> | |
| net The Petri net that should be examined | |
| Check if a Petri net is restricted-free-choice. That is: | |
| \forall t_1,t_s\in T\colon{}^\bullet t_1\cap{}^\bullet t_2\neq\es | |
| \impl|{}^\bullet t_1|=|{}^\bullet t_2|=1 | |
| ----------- | |
| Usage: apt safe <pn> | |
| pn The Petri net that should be examined | |
| Check if a Petri net is safe. A Petri net is safe if no marking is reachable were a place has more than one token. | |
| ----------- | |
| Usage: apt sideconditions <pn> | |
| pn The Petri net that should be examined | |
| Compute the sideconditions of a Petri net. A side condition is a self-loop, consisting of the place, the transition and the arcs. | |
| ----------- | |
| Usage: apt simply_live <pn> [<transition>] | |
| pn The Petri net that should be examined | |
| transition A transition that should be checked for liveness | |
| Check if a Petri net or a transition (if given) is simply live. A transition is simply live when it can fire at least once. A Petri net is simply live when all of its transitions are simply live. For a simply live transition, this module finds a firing sequence that fires the transition. | |
| ----------- | |
| Usage: apt siphons <pn> | |
| pn The Petri net that should be examined | |
| Compute all minimal siphons in a Petri net. A siphon is a set of places so that every transition consuming tokens from one of these places also produces tokens on at least one place in the set. | |
| ----------- | |
| Usage: apt snet <pn> | |
| pn The Petri net that should be examined | |
| Check if a plain Petri net is an S-net. In a S-net, the preset and postset of any transition has at most one entry (plus the net is plain). | |
| ----------- | |
| Usage: apt strong_components <graph> | |
| graph The graph that should be examined | |
| Find the strongly connected components of a Petri net or LTS | |
| ----------- | |
| Usage: apt strong_separation <pn> <sequence> [<k>] [<verbose>] | |
| pn The Petri net that should be examined | |
| sequence Firing sequence which should be checked | |
| k Value of k The default value is '0'. | |
| verbose Optional more output The default value is ''. | |
| Check if a given sequence is strongly k-separable. | |
| Example calls: | |
| To check a given firing sequence: | |
| apt strong_separation petri_net.apt "a1;a2;a3" | |
| To check a given firing sequence and set k to 2: | |
| apt strong_separation petri_net.apt "a1;a2;a3" 2 | |
| To check a given firing sequence and set k to 2 with more output: | |
| apt strong_separation petri_net.apt "a1;a2;a3" 2 verbose | |
| Format descriptions of parameters: | |
| sequence: | |
| Words can be specified in two different forms. | |
| The first format includes explicit delimiters between events. For delimiters, either commas, semicolons or spaces are allowed. An example of this format would be 'a, b, c'. Note that leading and trailing spaces are skipped. | |
| The second format expects events to be individual letters. The special prefix : is used to indicate this format. An example would be ':abc'. | |
| ----------- | |
| Usage: apt strong_separation_length <pn> <length> [<k>] [<verbose>] | |
| pn The Petri net that should be examined | |
| length Maximum length of firing sequences | |
| k Value of k The default value is '0'. | |
| verbose Optional more output The default value is ''. | |
| Check if all sequences up to a length are strongly k-separable. | |
| Example calls: | |
| To check all firing sequences to up a length of 3: | |
| apt strong_separation_length petri_net.apt 3 | |
| To check all firing sequences to up a length of 3 and set k to 2: | |
| apt strong_separation_length petri_net.apt 3 2 | |
| To check all firing sequences to up a length of 3 and set k to 2 with more output: | |
| apt strong_separation_length petri_net.apt 3 2 verbose | |
| ----------- | |
| Usage: apt strongly_connected <graph> | |
| graph The graph that should be examined | |
| Check if a Petri net or LTS is strongly connected | |
| ----------- | |
| Usage: apt strongly_live <pn> [<transition>] | |
| pn The Petri net that should be examined | |
| transition A transition that should be checked for liveness | |
| Check if a Petri net or a transition (if given) is strongly live. A transition is strongly live when for every reachable marking there exists a firing sequence after which this transition is activated. A Petri net is strongly live when all of its transitions are strongly live. For a transition which is not strongly live, this module finds a firing sequence after which the transition cannot fire anymore. | |
| ----------- | |
| Usage: apt sum_async <pn1> <pn2> [<sum>] | |
| pn1 The first PN of the sum | |
| pn2 The second PN of the sum | |
| sum Optional file name for writing the output to | |
| Compute the synchronous sum of two PN | |
| ----------- | |
| Usage: apt sum_sync <pn1> <pn2> [<sum>] | |
| pn1 The first PN of the sum | |
| pn2 The second PN of the sum | |
| sum Optional file name for writing the output to | |
| Compute the synchronous sum of two PN | |
| ----------- | |
| Usage: apt synthesize <options> <lts> [<pn>] | |
| options Comma separated list of options | |
| lts The LTS that should be synthesized to a Petri Net | |
| pn Optional file name for writing the output to | |
| Synthesize a Petri Net from a transition system. | |
| Supported options are: none, [k]-bounded, safe, [k]-marking, pure, plain, tnet, generalized-marked-graph (gmg), marked-graph (mg), generalized-output-nonbranching (gon) output-nonbranching (on), conflict-free (cf), homogeneous, behaviourally-conflict-free (bcf), binary-conflict-free (bicf), upto-language-equivalence (language, le), minimize (minimal), verbose and quick-fail. | |
| The meaning of these options is as follows: | |
| - none: No further requirements are made. | |
| - [k]-bounded: In every reachable marking, every place contains at most [k] tokens. | |
| - safe: Equivalent to 1-bounded. | |
| - [k]-marking: The initial marking of each place is a multiple of k. | |
| - pure: Every transition either consumes or produces tokens on a place, but not both (=no side-conditions). | |
| - plain: Every flow has a weight of at most one. | |
| - tnet: Every place's preset and postset contains at most one entry. | |
| - generalized-marked-graph: Every place's preset and postset contains exactly one entry. | |
| - marked-graph: generalized-marked-graph + plain. | |
| - generalized-output-nonbranching: Every place's postset contains at most one entry. | |
| - output-nonbranching: generalized-output-nonbranching + plain. | |
| - conflict-free: The Petri net is plain and every place either has at most one entry in its postset or its preset is contained in its postset. | |
| - homogeneous: All outgoing flows from a place have the same weight. | |
| - behaviourally-conflict-free: In every reachable marking, the preset of activated transitions is disjoint. | |
| - binary-conflict-free: For every reachable marking and pair of activated transitions, enough tokens for both transitions are present. | |
| - minimize: The Petri net has as few places as possible. | |
| The following options only affect the output, but not the produced Petri net: | |
| - verbose: Print details about each calculated region/place. | |
| - quick-fail: Stop the algorithm when the result 'success: No' is clear. | |
| Example calls: | |
| apt synthesize none lts.apt | |
| apt synthesize 3-bounded lts.apt | |
| apt synthesize pure,safe lts.apt | |
| apt synthesize upto-language-equivalence lts.apt | |
| ----------- | |
| Usage: apt tnet <pn> | |
| pn The Petri net that should be examined | |
| Check if a plain Petri net is a T-net. In a T-net, the preset and postset of any place has at most one entry (plus the net is plain). | |
| ----------- | |
| Usage: apt tnet_generator <np> <nt> <m> [<directory>] | |
| np The maximum number of place for the Petri nets | |
| nt The maximum number of transitions for the Petri nets | |
| m The maximum number of token for the Petri nets | |
| directory Directory for writing the results to The default value is 'output'. | |
| Construct all T-nets up to a given size. | |
| ----------- | |
| Usage: apt to_regular_expression <pn_or_ts> | |
| pn_or_ts A Petri net or transition system whose language should be used | |
| Create a language-equivalent (up to prefix creation) regular expression | |
| ----------- | |
| Usage: apt totally_reachable <lts> | |
| lts The LTS that should be examined | |
| Check if the given LTS is totally reachable | |
| ----------- | |
| Usage: apt traps <pn> | |
| pn The Petri net that should be examined | |
| Compute all minimal traps in a Petri net. A trap is a set of places so that every transition producing tokens on one of these places also consumes tokens from at least one place in the set. | |
| ----------- | |
| Usage: apt tristate_philnet_generator <n> [<pn>] | |
| n The argument for the Petri net generator | |
| pn Optional file name for writing the output to | |
| Construct a Petri net for a tristate philosopher's net of a given size. | |
| ----------- | |
| Usage: apt use_petrify <lts> [<dead>] [<pn>] | |
| lts The LTS that should be examined | |
| dead If the given LTS is dead | |
| pn Optional file name for writing the output to | |
| Check if Petrify can generate a Petri net from a LTS | |
| For this module to function properly you must ensure that the Petrify executable can be found on your system. On most systems adding the directory where the executable is located to the PATH environment variable suffices to make it available to the APT system. | |
| ----------- | |
| Usage: apt use_synet <lts> [<pn>] | |
| lts The LTS that should be examined | |
| pn Optional file name for writing the output to | |
| Check if Synet can generate a Petri net from a LTS | |
| For this module to function properly you must ensure that the Synet executable can be found on your system. On most systems adding the directory where the executable is located to the PATH environment variable suffices to make it available to the APT system. | |
| ----------- | |
| Usage: apt weak_components <graph> | |
| graph The graph that should be examined | |
| Find the weakly connected components of a Petri net or LTS | |
| ----------- | |
| Usage: apt weak_separation <pn> <sequence> [<k>] [<verbose>] | |
| pn The Petri net that should be examined | |
| sequence Firing sequence which should be checked | |
| k Value of k The default value is '0'. | |
| verbose Optional more output The default value is ''. | |
| Check if a given sequence is weakly k-separable. | |
| Example calls: | |
| To check a given firing sequence: | |
| apt weak_separation petri_net.apt "a1;a2;a3" | |
| To check a given firing sequence and set k to 2: | |
| apt weak_separation petri_net.apt "a1;a2;a3" 2 | |
| To check a given firing sequence and set k to 2 with more output: | |
| apt weak_separation petri_net.apt "a1;a2;a3" 2 verbose | |
| Format descriptions of parameters: | |
| sequence: | |
| Words can be specified in two different forms. | |
| The first format includes explicit delimiters between events. For delimiters, either commas, semicolons or spaces are allowed. An example of this format would be 'a, b, c'. Note that leading and trailing spaces are skipped. | |
| The second format expects events to be individual letters. The special prefix : is used to indicate this format. An example would be ':abc'. | |
| ----------- | |
| Usage: apt weak_separation_length <pn> <length> [<k>] [<verbose>] | |
| pn The Petri net that should be examined | |
| length Maximum length of firing sequences | |
| k Value of k The default value is '0'. | |
| verbose Optional more output The default value is ''. | |
| Check if all sequences up to a length are weakly k-separable. | |
| Example calls: | |
| To check all firing sequences to up a length of 3: | |
| apt weak_separation_length petri_net.apt 3 | |
| To check all firing sequences to up a length of 3 and set k to 2: | |
| apt weak_separation_length petri_net.apt 3 2 | |
| To check all firing sequences to up a length of 3 and set k to 2 with more output: | |
| apt weak_separation_length petri_net.apt 3 2 verbose | |
| ----------- | |
| Usage: apt weakly_connected <graph> | |
| graph The graph that should be examined | |
| Check if a Petri net or LTS is weakly connected | |
| ----------- | |
| Usage: apt weakly_live <pn> [<transition>] | |
| pn The Petri net that should be examined | |
| transition A transition that should be checked for liveness | |
| Check if a Petri net or a transition (if given) is weakly live. A transition is weakly live if an infinite fire sequence exists which fires this transition infinitely often. A Petri net is weakly live when all of its transitions are weakly live | |
| ----------- | |
| Usage: apt word <pn> <word> | |
| pn The Petri net that should be examined | |
| word The word which should be checked | |
| Check if a word is in a Petri net's prefix language | |
| Format descriptions of parameters: | |
| word: | |
| Words can be specified in two different forms. | |
| The first format includes explicit delimiters between events. For delimiters, either commas, semicolons or spaces are allowed. An example of this format would be 'a, b, c'. Note that leading and trailing spaces are skipped. | |
| The second format expects events to be individual letters. The special prefix : is used to indicate this format. An example would be ':abc'. | |
| ----------- | |
| Usage: apt word_synthesize <options> <word> [<pn>] | |
| options Comma separated list of options | |
| word The word that should be synthesized | |
| pn Optional file name for writing the output to | |
| Synthesize a Petri Net from a word. | |
| Supported options are: none, [k]-bounded, safe, [k]-marking, pure, plain, tnet, generalized-marked-graph (gmg), marked-graph (mg), generalized-output-nonbranching (gon) output-nonbranching (on), conflict-free (cf), homogeneous, behaviourally-conflict-free (bcf), binary-conflict-free (bicf), upto-language-equivalence (language, le), cycle, minimize (minimal), verbose and quick-fail. | |
| The meaning of these options is as follows: | |
| - none: No further requirements are made. | |
| - [k]-bounded: In every reachable marking, every place contains at most [k] tokens. | |
| - safe: Equivalent to 1-bounded. | |
| - [k]-marking: The initial marking of each place is a multiple of k. | |
| - pure: Every transition either consumes or produces tokens on a place, but not both (=no side-conditions). | |
| - plain: Every flow has a weight of at most one. | |
| - tnet: Every place's preset and postset contains at most one entry. | |
| - generalized-marked-graph: Every place's preset and postset contains exactly one entry. | |
| - marked-graph: generalized-marked-graph + plain. | |
| - generalized-output-nonbranching: Every place's postset contains at most one entry. | |
| - output-nonbranching: generalized-output-nonbranching + plain. | |
| - conflict-free: The Petri net is plain and every place either has at most one entry in its postset or its preset is contained in its postset. | |
| - homogeneous: All outgoing flows from a place have the same weight. | |
| - behaviourally-conflict-free: In every reachable marking, the preset of activated transitions is disjoint. | |
| - binary-conflict-free: For every reachable marking and pair of activated transitions, enough tokens for both transitions are present. | |
| - minimize: The Petri net has as few places as possible. | |
| - cycle: Form a cyclic word representing w^* instead of solving the input word w directly | |
| The following options only affect the output, but not the produced Petri net: | |
| - verbose: Print details about each calculated region/place. | |
| - quick-fail: Stop the algorithm when the result 'success: No' is clear. | |
| This module tries to synthesize a Petri Net whose prefix language contains only the specified word. Thus, no other words are firable. If this fails, a list of separation failures is printed. | |
| Example calls: | |
| apt word_synthesize none a,b,a,b | |
| The above prints a Petri net | |
| apt word_synthesize pure,safe a,b,c,a | |
| This also prints a Petri net | |
| apt word_synthesize none a,b,b,a,a | |
| The above produces the following output: | |
| separationFailurePoints: a, b, [a] b, a, a | |
| Here three places where calculated. For example, the first one of them has an initial marking of one, transition 'a' consumes a token on this place and 'b' produces one. However, these three places are not enough for producing the requested word, because after firing 'a' and 'b' once, transition 'a' is enabled, but shouldn't. The module also could not calculate any place which would prevent 'a' from occurring in this state without also restricting 'a' in some state where it must occur. | |
| apt word_synthesize 2-bounded a,a,a | |
| The above produces the following output: | |
| separationFailurePoints: a, a, a [a] | |
| This means that there is no 2-bounded Petri Net where three a's are firable in sequence, but not also a fourth one can occur. | |
| Format descriptions of parameters: | |
| word: | |
| Words can be specified in two different forms. | |
| The first format includes explicit delimiters between events. For delimiters, either commas, semicolons or spaces are allowed. An example of this format would be 'a, b, c'. Note that leading and trailing spaces are skipped. | |
| The second format expects events to be individual letters. The special prefix : is used to indicate this format. An example would be ':abc'. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
I can see anything.