Index

?

abort commands

Course of the computation

analysis

6. Analysis | 6. Analysis to <M> Decide state machine

expert system: 6.1 Fundamentals
graphs: 6.5.4 Computation and analysis
invariants: 6.6 Invariant analysis
menu: 6.3 Analysis menu and
of several nets: 2.4.3 Analysis of several
paths: 6.5.3 Computation of paths
place set: <W> <F> Write the
pre-analysis: Pre-analysis
status: 6.2 Analysis status
structures: 6.7 Structural analysis

arc

change: <R> <A> Read an
delete: <R> <A> Read an | <D> <A> Delete all
diagonal: Coloured nets
entry: <R> <A> Read an
first component: Coloured nets
his: Coloured nets
mine: Coloured nets
multiplicity: Uncoloured nets
permeability:  intervals | Time option intervals for | Time option intervals for
second component: Coloured nets

assumed place bound

.atm

2.3.2 File extensions

atom

B

B : bounded

backspace

<R> test the reachability/coverability

backtracking

bad state reachable

BSt: bad state reachable

black tokens

 black (indistinguishable) tokens

bounded

B : bounded | <D> Check the deadlock-trap-, | <M> Decide state machine

assumed place bound: Course of the computation
covering marking: Course of the computation

BSt

BSt: bad state reachable

calling INA

2.1 Getting started

.cap

2.3.2 File extensions | <C> <C> Change Capacities

capacities

<C> normal firing rule

change: <C> <C> Change Capacities
entry: Uncoloured nets
firing rule: <C> normal firing rule
infinite: Special keys and symbols | <C> normal firing rule
needed: Course of the computation

change

capacities: <C> <C> Change Capacities
exceptions: <X> change eXceptions
initial clock position: <C>  Change Initial
initial times: <C>  Change Initial
marking: <C> <T> Change the
multiplicities: <C> <M> Change Multiplicities
names: <C> <N> Change Names
numbers: <C>  Change numbers
priorities: <C>  Change Priorities
token load: <C> <T> Change the

check a CTL-formula

Time option intervals for

.cir

2.3.2 File extensions | <K> compute circuits |  inspect a result

circuit-free graph

<A> compute distances

circuits

<K> compute circuits

CL

CL : collectively live | <L> check liveness properties

clock evaluation

2.5.2 Time option

firing: 4.4.2 Firing under time
state representation: 4.2.2 State representation under

clock stop time

clocked net elements

 intervals

.cnt

2.3.2 File extensions | Syntax of the .cnt-file

collectively live

CL : collectively live | <L> check liveness properties

coloured nets

Coloured nets | <C> coloured tokens

live: Liveness for coloured nets | <L> check liveness properties

coloured tokens

colours

see node

construction: Coloured nets
delete: <D> <C> Delete a
discard: <C> coloured tokens
entry: Coloured nets
isolated: <D>  Delete all
options: <C> coloured tokens

COMMAND.ina

commands

<D> Check the deadlock-trap-,

comments

Note

components

compute: <C> Compute all components
state machine: <M> Decide state machine
strong connection: <M> Decide state machine

computation

stubborn reduction: Stubborn reduction | <R> Compute a reachability

circuits

<K> compute circuits

components

<C> Compute all components

coverability graph

Coverability graphs | <G> Compute a coverability

deadlock-trap-property

distances

<A> compute distances

dynamic conflicts

<Y> check dynamic conflicts

Finkel's method

Finkel's Method of computing | <G> Compute a coverability

invariants

6.6.1 Computing invariants

invariants basis

 Compute a basis | <S> Compute a basis

minimal path

 Compute a shortest | <O> Compute a minimal

minimal time path

 Compute a shortest | <O> Compute a minimal

minimal value path

<O> Compute a minimal

path

6.5.3 Computation of paths

reachability graph

<R> Compute a reachability

returning heap

6.1 Fundamentals

semipositive invariants

6.6.2 Semipositive invariants

shortest path

 Compute a shortest

state graph

<R> Compute a reachability

strongly connected components

<V> compute strongly connected

symmetric reduction

Symmetrical reduction | <R> Compute a reachability

symmetries

<Y> Compute the symmetries

CON

CON: connected

conflict

SCF: static conflict free | DCF: dynamically conflict free | Pre-analysis | <Y> check dynamic conflicts

between steps: <Y> check dynamic conflicts

conjunction

connectedness

CON: connected

test: <T> <C> Test Connectedness | <T> connectedness Test

conservative

consider structure as total

convert a set of states to a predicate

<C> convert a set

correction

counterexamples

CTI: covered by transition | 6.6 Invariant analysis

covered by place invariants

CPI: covered by place

covered by transition invariants

CPI

CPI: covered by place

cr

Special keys and symbols | Requesting files and entering

CSV

CTI: covered by transition | 6.6 Invariant analysis

CTI

.ctl

2.3.2 File extensions | 6.5.2 Predicates and CTL | <F> check a CTL-formula

atom: State predicates | Model checking
atomic mode: <F> check a CTL-formula
counterexamples: <F> check a CTL-formula
equivalences: Equivalences and further notes
formulae: Syntax of CTL | Equivalences and further notes
infinite path: Semantics of CTL
model checking: Model checking | CTL model checking and
predicate: State predicates
proof: <F> check a CTL-formula
semantics: Semantics of CTL
syntax: Syntax of CTL | <F> check a CTL-formula
total structure: Model checking | <F> check a CTL-formula
witnesses: <F> check a CTL-formula

DCF

DCF: dynamically conflict free | <Y> check dynamic conflicts

dead state reachable

DSt: dead state reachable

dead transition at initial marking

DTr: dead transition at

deadlock

DTP: deadlock-trap-property

deadlock-trap-property

DTP: deadlock-trap-property | <D> Check the deadlock-trap-,

default options

2.5 Options

delete

1.2 Form of representation

arcs: <D> <A> Delete all
colour: <D> <C> Delete a
exceptions: <X> change eXceptions
incomplete net: <Q> Quit the editing
isolated nodes: <D>  Delete all
net: <D> <T> Delete the
node: <D> <N> Delete a
old net: <R> <F> Read a
session report: <D> delete the session

depth restriction

Depth restriction

description

dialogue

2.2 General rules for

distances

<A> compute distances

don't care

<N> Non-reachability test of |  Compute a shortest

DSt

DSt: dead state reachable

DTP

DTP: deadlock-trap-property

DTr

DTr: dead transition at | <L> check liveness properties

duration

<D> durations | Time option duration for | Time option Duration for

dynamic conflict

DCF: dynamically conflict free | <Y> check dynamic conflicts

EBNF

2.3.4 File formats

editor

3. Editor | 3. Editor to <T> <C> Test Connectedness

menu: 3. Editor

EFC

EFC: extended free choice

eft/lft

 intervals | Time option intervals for eft/lft | Time option intervals for eft/lft

elementary properties

6.2.1 Elementary net properties

elimination

<A> ELIMINATION of F(pF)=p |  ELIMINATION of (Fp)F=p

entry

2.2 General rules for

continue: Uncoloured nets
editing: Requesting files and entering
name: 2.3.3 Entering nets
net: 2.3.3 Entering nets | <R> <T> Read a
not found: Requesting files and entering
number: 2.3.3 Entering nets
place: 2.3.3 Entering nets | <R> <N> Read a
transition: <R> <N> Read a

error correction

Special keys and symbols | Requesting files and entering

ES

ES: extended simple

esc

.exc

2.3.2 File extensions | <X> change eXceptions

exceptions

5.1 Fundamentals | <X> change eXceptions

ok after reset:  reset to the

exiting INA

EFC: extended free choice

expert system

6.1 Fundamentals

extended free choice

extended simple

ES: extended simple

facts

DTr: dead transition at

dead transitions: <L> check liveness properties

FC

FC: free choice

file

see entry

EBNF syntax: 2.3.4 File formats
extensions: Requesting files and entering | 2.3.2 File extensions
formats: 2.3.4 File formats
important: 2.3.1 Important files
name suggestion: Requesting files and entering | Requesting files and entering
not found: Requesting files and entering
overwrite: Saving data
request: Requesting files and entering
switch to terminal mode: Switching to the terminal
write: Saving data

Finkel's method

Finkel's Method of computing | <G> Compute a coverability

firing

4. Firing | 4. Firing to 4.5 Example

auxiliary functions: 4.3 Auxiliary functions
back to previous state:  Back to the
duration: Time option duration for | Time option Duration for
eft/lft: Time option intervals for eft/lft
executed steps: <S> write the list
first element: <cr> fire the first
functions: 4.4.1 General remarks
list: 4.4.1 General remarks
maximal steps: <S> firing maximal steps
menu: 4.1 Fundamentals
permeability: Time option intervals for | Time option intervals for
reset to initial state: <R> Reset to the
rule: 2.5.3 Firing rule
single transitions: <T> fire single transitions
strategy: 2.5.5 Firing strategy
under timing: 4.2.2 State representation under | 4.4.2 Firing under time
write marking: <W> Write the actual

first part deleted

<D> delete the session

fixpoints

<Y> Compute the symmetries

forget the net

Fp0: place without pre-transition

Fp0

free choice

FC: free choice

Ft0

Ft0: transition without pre-place

fusion of congruent nodes

<F> Fusion of congruent

.gra

<W> write the computed

graph analysis

Further graph analysis to  inspect a result

circuits: <K> compute circuits
CTL model checking: CTL model checking and
distances: <A> compute distances
dynamic conflicts: <Y> check dynamic conflicts
liveness: <L> check liveness properties
predicate: CTL model checking and
reachability test: <R> test the reachability/coverability
strongly connected components: <V> compute strongly connected
writing functions: Writing functions

graph computation

<R> Compute a reachability to Course of the computation

course: Course of the computation
coverability graph: Coverability graphs | Finkel's Method of computing | <G> Compute a coverability
covering marking: Course of the computation
depth restriction: Depth restriction
incomplete: Course of the computation
inspect files: Inspect files
modes: Calculation mode
number of arcs: Course of the computation
number of states: Course of the computation
options: Options
reduction: 6.5.1 Reductions of the
stubborn reduction: Stubborn reduction | <R> Compute a reachability
symmetric reduction: Symmetrical reduction | <R> Compute a reachability

.hlp

2.3.2 File extensions | <F> Format lines written

HOM

HOM: homogenous

homogeneous

HOM: homogenous

.icp

2.3.2 File extensions | <C>  Change Initial

.ict

2.3.2 File extensions | <C>  Change Initial

incidence matrix

Incidence matrix | <M> show (transposed) incidence

ININET.pnt

2.3.1 Important files |  reset to the

initial clock position

Uncoloured nets | Coloured nets | <C>  Change Initial

installation

2.1 Getting started

interupt commands

.inv

2.3.2 File extensions | <T> complete table |  Compute a basis | <F> Format lines written | <O> open files (input

INVARI.hlp

2.3.1 Important files | <F> Format lines written

invariants

6.6 Invariant analysis

automatic computation: Interactive computation
basis: 6.6.1 Computing invariants |  Compute a basis | 6.6.2 Semipositive invariants
complexity: Notes on complexity
computate basis: <S> Compute a basis
computation: 6.6.1 Computing invariants
consistency test: <O> open files (input
covered solutions: <F> Format lines written
enter vector: <R> read vector
equation results:  give results of
files: <O> open files (input
format lines: <F> Format lines written
formatting: Formatting invariants
incidence matrix: Incidence matrix | <M> show (transposed) incidence
incomplete results: <F> Format lines written
interactive computation: Interactive computation
interpretation: Example of an invariant
jump mode: <R> read vector
lines input file: <F> Format lines written
non-reachability test: Fast non-reachability test
options: Incidence matrix | Output formats
output format: Output formats | Output formats | <F> change output format
properties:  give properties of
proposal: <S> Compute a basis
read vector: <R> read vector
realizable: <K> compute circuits
repeat function sequence: <S> repeat function sequence
results by other format:  Compute a basis
semipositive: <#> print non-zero entries | 6.6.2 Semipositive invariants
sequential mode: <R> read vector
skip lines: <F> Format lines written
sub: Semipositive (sub/sur)-invariants
support: Output formats
sur: Semipositive (sub/sur)-invariants
test: <T> Test place- or |  give properties of
write vector: <W> write vector

Karp/Miller

L

L&S

line length

live

L : live | <D> Check the deadlock-trap-,

and safe: L&S: live and safe
checking: <L> check liveness properties
collectively: CL : collectively live | <L> check liveness properties
weakly: WL : weakly live | <L> check liveness properties
when ignoring dead transitions: LV : live when | <L> check liveness properties

livelock

<K> compute circuits

loop

<R> <L> Add a | Time option Duration for

loop-free

lower bound

LV

LV : live when | <L> check liveness properties

main menu

.mar

2.3.2 File extensions | <C> <T> Change the | <W> Write the actual

marked graph

MG: marked graph

marking

see state

change: <C> <T> Change the
covering: Course of the computation | <R> test the reachability/coverability
standard: Coloured nets
zero: Coloured nets

merge

nets: <M> <N> Merge two
nodes: <M> <O> Merge two

MG

MG: marked graph

model checking

Model checking | CTL model checking and | see CTL

multiplicity

Uncoloured nets

change: <R> <A> Read an | <C> <M> Change Multiplicities
non-blocking: NBM: non-blocking multiplicity

name suggestion

NBM: non-blocking multiplicity

NBM

needed capacities

Course of the computation

net

see example nets

analyse place set

<W> <F> Write the

bounded

B : bounded

capacities

<C> normal firing rule | <C> <C> Change Capacities

coloured

Coloured nets | <C> coloured tokens

comments

Note

connected

CON: connected

conservative

Course of the computation

covered by invariants

CPI: covered by place | 6.6 Invariant analysis

covering marking

deadlock-trap-property

DTP: deadlock-trap-property | <D> Check the deadlock-trap-,

delete

<Q> Quit the editing | <D> <T> Delete the

discard

discard colours

DCF: dynamically conflict free

dynamic conflict

entry

2.3.3 Entering nets | <R> <T> Read a

extended free choice

EFC: extended free choice

extended simple

ES: extended simple

fold

NBM: non-blocking multiplicity

free choice

FC: free choice

homogenous

HOM: homogenous

incidence matrix

Incidence matrix | <M> show (transposed) incidence

incomplete

3. Editor

Information

<W> <T> Write the

live

L : live | 6.6 Invariant analysis

and safe: L&S: live and safe

loop

<R> <L> Add a | Time option Duration for

marked graph

MG: marked graph

Marking

<C> <T> Change the

merge

<M> <N> Merge two

name

Uncoloured nets | <C> <N> Change Names

non-blocking multiplicity

number

Uncoloured nets | <C>  Change numbers

ordinary

ORD: ordinary

place/transition

 black (indistinguishable) tokens

pre-analysis

Pre-analysis

priorities

2.5.4 Priorities | <C>  Change Priorities

pure

6.5 Reachability analysis

reachability analysis

read

<R> <F> Read a

resetable

REV: reversible

reversible

REV: reversible

run-place

<R>  Insert a

state machine

SM: state machine

state machine allocatable

SMA: state machine allocatable

state machine coverable

SMC: state machine coverable

state machine decomposable

SMD: state machine decomposable

static conflict

SCF: static conflict free | Pre-analysis

strongly connected

SC: strongly connected

structural properties

6.2.1 Elementary net properties | Pre-analysis | 6.7 Structural analysis

structurally bounded

SB : structurally bounded

sub-conservative

time option

2.5.2 Time option | 4.2.2 State representation under | 4.4.2 Firing under time

token type

2.5.1 Token types

uncoloured

Uncoloured nets

unfold

write

<W> <F> Write the

write to the terminal

<W> <T> Write the

next conjunction

NBM: non-blocking multiplicity

node

see place, transition

congruent: <F> Fusion of congruent
delete: <D> <N> Delete a
doubling: <N> <D> Node Doubling
entry: <R> <N> Read a
equivalent: <M> Merging of equivalent
isolated: <D>  Delete all
merge: <M> <O> Merge two
one-sided: One-sided nodes

non-blocking multiplicity

non-reachability test

6.4.2 Fast non-reachability test | Fast non-reachability test

normal firing rule

<N> normal firing rule

only places/transitions present

3. Editor

oo

Special keys and symbols | <C> normal firing rule

options

2.3.1 Important files | 2.5 Options | 2.5 Options to 2.5.6 Line length

at start ofprogram: 2.5 Options
default: 2.5 Options
firing rule: 2.5.3 Firing rule
firing strategy: 2.5.5 Firing strategy
line length: 2.5.6 Line length
priorities: 2.5.4 Priorities
time option: 2.5.2 Time option | 4.2.2 State representation under | 4.4.2 Firing under time
token type: 2.5.1 Token types

OPTIONS.ina

2.3.1 Important files | 2.4.1 Starting and exiting | 2.5 Options

ORD

ORD: ordinary

ordinary

ORD: ordinary

output file

Saving data

output format

<F> change output format

overview

1.1 Overview

overwrite

Saving data

path computation

6.5.3 Computation of paths

by backtracking: <R> test the reachability/coverability
display of results: Display of results

.pdc

2.3.2 File extensions | State predicates

pF0

pF0: place without post-transition

philosophers

complete run: 4.5 Example
dead state: 4.5 Example
entry: Coloured nets
figure: Coloured nets
file: Example for a .cnt-file

place

see node

assumed bound: Course of the computation
bounded: Semipositive (sub/sur)-invariants | <M> Decide state machine
capacity: <C> normal firing rule
entry: Uncoloured nets | <R> <N> Read a
invariant: 6.6 Invariant analysis
name: Uncoloured nets | <C> <N> Change Names
number: Uncoloured nets | <C>  Change numbers
overloaded: <C> normal firing rule
run-place: <R>  Insert a
without post-transition: pF0: place without post-transition
without pre-transition: Fp0: place without pre-transition
write to the terminal: <W> <T> Write the

.pnt

2.3.2 File extensions | Syntax of a .pnt-file

pre-analysis

Pre-analysis

predicate

bad: Bad predicate
convert a set of states: <C> convert a set
disjunctive normal form: State predicates
enabledness predicate: <E> define an enabledness
functions: CTL model checking and

preparation

2.1 Getting started

.prf

2.3.2 File extensions | <F> check a CTL-formula |  inspect a result

.pri

2.3.2 File extensions | <C>  Change Priorities

priority

2.5.4 Priorities

change: <C>  Change Priorities
entry: Uncoloured nets

program a sequence of reduction steps

 Program a sequence

proof

<W> DELETION of PTP-sequences

PTP-sequences

PUR

pure

quit

raise node numbers with exceptions

<R> Raise node numbers

reachability

bad state: BSt: bad state reachable
dead state: DSt: dead state reachable | <D> Check the deadlock-trap-,
transient state: Time option Duration for | 6.5.4 Computation and analysis

reachability graph

see graph

reachability test

 Compute a shortest | <O> Compute a minimal

read

a net from a file: <R> <F> Read a
a net from the terminal: <R> <T> Read a
a node from the terminal: <R> <N> Read a
an arc from the terminal: <R> <A> Read an

.red

2.3.2 File extensions | <N> save the actual

reduction

5. Reduction | 5. Reduction to <W> DELETION of PTP-sequences

abort: 5.1 Fundamentals
congruent nodes: <F> Fusion of congruent
equivalent nodes: <M> Merging of equivalent
equivalent places: <M> Merging of equivalent
exceptions: 5.1 Fundamentals | <X> change eXceptions
looping places: <C> ELIMINATION of looping
looping transitions:  DELETION of looping
menu: 5.1 Fundamentals
no application possible: 5.1 Fundamentals
pre- and post-places: <V> DELETION of single
pre- and post-transitions: <A> ELIMINATION of F(pF)=p |  ELIMINATION of (Fp)F=p
program:  Program a sequence
PTP-sequences: <W> DELETION of PTP-sequences
raise node numbers: <R> Raise node numbers
reset:  reset to the
save: <N> save the actual
show: <O> terminal Output of
single output transitions: <V> DELETION of single
squeeze node numbers: <S> Squeeze the node
stopped: 5.1 Fundamentals
test for connectedness: <T> connectedness Test

replying to requests

2.2 General rules for

.res

reset to the initial net

 reset to the

resetable

REV: reversible | <V> compute strongly connected

returning heap

6.1 Fundamentals

REV

REV: reversible | <V> compute strongly connected

reversible

REV: reversible | <V> compute strongly connected

run-place

<R>  Insert a

safe firing rule

<S> safe firing rule

same procedure as last time

save commands

SB : structurally bounded | 6.4.1 Fast boundedness test

SB

SC

SC: strongly connected

SCF

SCF: static conflict free

session report

2.3.1 Important files | 2.4.2 The session report

delete: <D> delete the session
first part deleted: <D> delete the session
read: <S> read the session |  inspect a result
rename: 2.4.1 Starting and exiting

SESSION.ina

2.3.1 Important files | 2.4.1 Starting and exiting | 2.5.6 Line length |  inspect a result

SM

SM: state machine | <C> Compute all components

SMA

SMA: state machine allocatable | <D> Check the deadlock-trap-, | <C> Compute all components

SMC

SMC: state machine coverable | <M> Decide state machine

SMD

SMD: state machine decomposable | <D> Check the deadlock-trap-, | <C> Compute all components

space

Special keys and symbols | Requesting files and entering

squeeze the node numbers

<S> Squeeze the node

.sta

2.3.2 File extensions | <M> write all states |  inspect a result

stabilization time

Time option Duration for

stable states

Time option Duration for

starting INA

2.1 Getting started | 2.4.1 Starting and exiting

state

bad: BSt: bad state reachable | 6.5.4 Computation and analysis |  write the bad
dead: DSt: dead state reachable | 6.5.3 Computation of paths | 6.5.4 Computation and analysis | <D> write the dead
generated:  Compute a shortest
representation: 4.2 State representations
stable: Time option Duration for | Time option intervals for
transient: <R> <L> Add a | Time option Duration for | Time option intervals for | 6.5.3 Computation of paths | 6.5.4 Computation and analysis
under time allocation: 4.2.2 State representation under
without time allocation: 4.2.1 State representation without

state equation

6.4.2 Fast non-reachability test

state graph

see graph

state machine

SM: state machine | <M> Decide state machine

allocatability: SMA: state machine allocatable | <D> Check the deadlock-trap-,
coverability: SMC: state machine coverable | <M> Decide state machine
decomposability: SMD: state machine decomposable | <D> Check the deadlock-trap-,

static conflict

SCF: static conflict free | Pre-analysis

step

<S> firing maximal steps | Time option intervals for

conflicts: <Y> check dynamic conflicts
executed: <S> write the list
firing rule: <S> firing maximal steps
list: <S> write the list
liveness: <L> check liveness properties

strongly connected

SC: strongly connected

components: <V> compute strongly connected

structural analysis

Structures | 6.7 Structural analysis

structural properties

6.2.1 Elementary net properties | Structures | Pre-analysis | 6.7 Structural analysis

structurally bounded

SB : structurally bounded

fast test: 6.4.1 Fast boundedness test

stubborn set

<S> Show the stubborn | Stubborn reduction

show all: <A> All minimal stubborn
show used: <S> Show the stubborn

sub-conservative

Switching to the terminal

symmetries

<Y> Compute the symmetries

compute again: <Y> Compute the symmetries
fixpoints: <Y> Compute the symmetries
identity: <Y> Compute the symmetries
initial state: <Y> Compute the symmetries
trivial transition partition: <Y> Compute the symmetries

syntax

.pnt-file: Syntax of a .pnt-file
.cnt-file: Syntax of the .cnt-file
CTL: Syntax of CTL
EBNF: 2.3.4 File formats
files: 2.3.4 File formats
place entry: Uncoloured nets
transition entry: <R> <N> Read a

terminal mode

terminating the program

tF0: transition without post-place

test

connectedness: <T> <C> Test Connectedness | <T> connectedness Test
coverability: <R> test the reachability/coverability
invariant properties: <T> Test place- or
liveness: <L> check liveness properties
non-reachability: 6.4.2 Fast non-reachability test | Fast non-reachability test
reachability:  Compute a shortest | <O> Compute a minimal | <R> test the reachability/coverability
reversibility: <V> compute strongly connected
structural boundedness: 6.4.1 Fast boundedness test
vectors for invariant properties: <T> Test place- or

tF0

.tim

2.3.2 File extensions

time allocation

2.5.2 Time option

firing: 4.4.2 Firing under time
state representation: 4.2.2 State representation under

time interval

 intervals | Time option intervals for eft/lft

time option

2.5.2 Time option

firing: 4.4.2 Firing under time
state representation: 4.2.2 State representation under

.tmd

2.3.2 File extensions

token type

2.5.1 Token types

.tra

2.3.2 File extensions |  Compute a shortest | <R> test the reachability/coverability |  inspect a result

transient state

Time option Duration for

transition

see node

dead: DTr: dead transition at | <L> check liveness properties | <D> Check the deadlock-trap-,
dead at initial marking: DTr: dead transition at
duration: <D> durations | Time option duration for | Time option Duration for
eft/lft:  intervals | Time option intervals for eft/lft | Time option intervals for eft/lft
entry: <R> <N> Read a
facts: DTr: dead transition at
in livelock: <K> compute circuits
invariants: 6.6 Invariant analysis
live: L : live
name: Uncoloured nets | <C> <N> Change Names
number: Uncoloured nets | <C>  Change numbers
realizable invariants: <K> compute circuits
value assignment:  Compute a shortest | <O> Compute a minimal | <K> compute circuits
without post-place: tF0: transition without post-place
without pre-place: 5.1 Fundamentals | Ft0: transition without pre-place
write to the terminal: <W> <T> Write the

trap

DTP: deadlock-trap-property

upper bound

.val

2.3.2 File extensions | <O> Compute a minimal | <K> compute circuits

weakly live

WL : weakly live | <L> check liveness properties

witnesses