Index

#

Editieren der Eingabe

?

Editieren der Eingabe

Abbruch eines Kommandos

2.4.1 Aufruf und Beenden

Abfragen beantworten

2.2 Generelle Regeln für

actual net do not match

<F> Format lines written

Analyse

6. Analyse | 6. Analyse to <M> Decide state-machine coverability

Expertsystem

6.1 Grundlagen

graph

6.5.4 Graphberechnung und -analyse

Graphen

6.5.4 Graphberechnung und -analyse

Invarianten

6.6 Invariantenanalyse

invariants

6.6 Invariantenanalyse

mehrerer Netze

2.4.3 Analyse mehrerer Netze

Menü

6.3 Analysemenü und Voranalyse

Pfade

6.5.3 Pfadberechnung

Platzmenge

<W> <F> Write the

Status

6.2 Analysestatus

structure

6.7 Strukturanalyse

Strukturen

6.7 Strukturanalyse

Voranalyse

Voranalyse

arcs generated

Ablauf der Berechnung

assume circuit-free graph

<A> compute distances

assumed place bound

Ablauf der Berechnung

.atm

2.3.2 Dateiextensionen

atom

Zustandsprädikate | Zustandsprädikate

Aufruf von INA

2.4.1 Aufruf und Beenden

Vorbereitungen

2.1 Startvorbereitungen

automatic mode

Interaktive Berechnung

B

B : Beschränktheit -

back to previous state

<B> Back to the

backspace

Editieren der Eingabe

backtracking

<R> test the reachability/coverability

bad state reachable

BSt: Schlechter Zustand erreichbar

Beenden von INA

2.4.1 Aufruf und Beenden

Berechnung

Überdeckbarkeitsgraph

Überdeckbarkeitsgrahen | <G> Compute a coverability

nach Finkels Methode

Finkels Methode zur Berechnung | <G> Compute a coverability

Deadlock-Falle-Eigenschaft

<D> Check the deadlock-trap-,

Distanzen

<A> compute distances

dynamische Konflikte

<Y> check dynamic conflicts

Erreichbarkeitsgraph

<R> Compute a reachability

stur reduziert

Sture Reduktion | <R> Compute a reachability

symmetrisch reduziert

Symmetrische Reduktion | <R> Compute a reachability

Generatoren

<Y> Compute the symmetries

Invariantenbasis

<I> Compute a base

semipositiv

<S> Compute a base

kürzester Pfad

<P> Compute a shortest

Komponenten

<C> Compute all components

Kreise

<K> compute circuits

minimaler Pfad

<P> Compute a shortest | <O> Compute a minimal

prädikatserfüllender Pfad

<O> Compute a minimal

Speicherüberlauf

<P> Compute a shortest

st. Zusammenhangskompo.

<V> compute strongly connected

statische Konflikte

Voranalyse

Symmetrien

<Y> Compute the symmetries

SZK

<V> compute strongly connected

Zustandsgraph

<R> Compute a reachability

stur reduziert

Sture Reduktion | <R> Compute a reachability

symmetrisch reduziert

Symmetrische Reduktion | <R> Compute a reachability

Beschränktheit

B : Beschränktheit - | <D> Check the deadlock-trap-, | <M> Decide state-machine coverability

strukturelle

SB : Strukturelle Beschränktheit

schneller Test

6.4.1 Schneller Beschränktheitstest

überdeckende Markierung

Ablauf der Berechnung

black tokens

<B> black (indistinguishable) tokens

Bogen

ändern

<R> <A> Read an

Durchlaßfenster

<I> intervals

eingeben

<R> <A> Read an

löschen

<R> <A> Read an | <D> <A> Delete all

bounded

B : Beschränktheit -

BSt

BSt: Schlechter Zustand erreichbar

.cap

2.3.2 Dateiextensionen | <C> <C> Change Capacities

change

capacities

<C> <C> Change Capacities

exceptions

<X> change eXceptions

initial times

<C> <I> Change Initial

marking

<C> <T> Change the

multiplicities

<C> <M> Change Multiplicities

names

<C> <N> Change Names

numbers

<C> <U> Change nUmbers

output format

Ausgabeformate | Ausgabeformate | <F> change output format

priorities

<C> <P> Change Priorities

token load

<C> <T> Change the

check a CTL-formula

<F> check a CTL-formula

.cir

2.3.2 Dateiextensionen | <K> compute circuits | <I> inspect a result

circuits

<K> compute circuits

CL

CL : Kollektive Lebendigkeit | <L> check liveness properties

clean

<D> Check the deadlock-trap-, | <M> Decide state-machine coverability

clock stop time

Zeitoption Intervalle für Bögen

clocked net elements

<I> intervals

.cnt

2.3.2 Dateiextensionen | Syntax der .cnt-Datei

collectively live

CL : Kollektive Lebendigkeit | <L> check liveness properties

colour set

Gefärbte Netze

coloured tokens

<C> coloured tokens

COMMAND.ina

Vorwort | 2.3.1 Wichtige Dateien | 2.4.1 Aufruf und Beenden

complete table

<T> complete table

compute

coverability graph

Überdeckbarkeitsgrahen | <G> Compute a coverability

Finkels method

Finkels Methode zur Berechnung | <G> Compute a coverability

invariants

6.6.1 Invariantenberechnung

semipositive

6.6.2 Semipositive Invarianten

minimal path

<O> Compute a minimal

minimal time path

<P> Compute a shortest | <O> Compute a minimal

minimal value path

<O> Compute a minimal

reachability graph

<R> Compute a reachability

stubborn reduced

Sture Reduktion | <R> Compute a reachability

symmetrical reduced

Symmetrische Reduktion | <R> Compute a reachability

shortest path

<P> Compute a shortest

state graph

<R> Compute a reachability

symmetries

<Y> Compute the symmetries

compute the symmetries once again

<Y> Compute the symmetries

computed graph not complete

Ablauf der Berechnung

CON

CON: Zusammenhang - connected

conjunktion

Zustandsprädikate

connected

CON: Zusammenhang - connected

connectedness test

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

conservativ

CSV: Konservativität - conservativ

convert a set of states to a prediacte

<C> convert a set

cosider structure as total

<F> check a CTL-formula

counterexamples

<F> check a CTL-formula

coverability test

<R> test the reachability/coverability

covered by place invariants

CPI: Platzinvariantenüberdeckbarkeit - covered

covered by transition invariants

CTI: Transitionsinvariantenüberdeckbarkeit - covered

covered solutions

<F> Format lines written

covering marking

<R> test the reachability/coverability

CPI

CPI: Platzinvariantenüberdeckbarkeit - covered

cr

Besondere Tasten und Zeichen | Dateianforderungen

CSV

CSV: Konservativität - conservativ

CTI

CTI: Transitionsinvariantenüberdeckbarkeit - covered | 6.6 Invariantenanalyse

.ctl

2.3.2 Dateiextensionen | 6.5.2 Prädikate und CTL-Modellchecking | <F> check a CTL-formula

Äquivalenzen

Äquivalenzen und weitere Anmerkungen

Atome

Zustandsprädikate | Modelchecking

Formeln

Syntax von CTL | Äquivalenzen und weitere Anmerkungen

Modelchecking

Modelchecking | CTL-Modelchecking und Prädikatdefinition

Prädikate

Zustandsprädikate

Semantik

Semantik von CTL

Syntax

Syntax von CTL

totale Struktur

Modelchecking | <F> check a CTL-formula

unendlicher Pfad

Semantik von CTL

Darstellungsweise

1.2 Darstellungsweise

Datei

Anforderung

Dateianforderungen

EBNF-Beschreibungen

2.3.4 Dateiformate

Extensionen

Eingabe von Namen | 2.3.2 Dateiextensionen

Formate

2.3.4 Dateiformate

Namensvorgabe

Dateianforderungen

übernehmen

Eingabe von Namen

speichern

Speichern von Daten

überschreiben

Speichern von Daten

Umschaltung in Terminalmodus

Umschaltung in den Terminalmodus

wichtige

2.3.1 Wichtige Dateien

DCF

DCF: Dynamische Konfliktfreiheit - | <Y> check dynamic conflicts

dead state reachable

DSt: Erreichbarkeit eines toten

dead transition

at initial marking

DTr: Tote Transition bei

Deadlock

DTP: Deadlock-Falle-Eigenschaft - deadlock-trap-property

Deadlock-Falle-Eigenschaft

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

deadlock-trap-property

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

delete

Editieren der Eingabe

colour

<D> <C> Delete a

exceptions

<X> change eXceptions

fragmented net

<Q> Quit the editing

input/output arcs

<D> <A> Delete all

isolated colour

<D> <I> Delete all

isolated nodes

<D> <I> Delete all

looping transitions

<U> DELETION of looping

net

<D> <T> Delete the

node

<D> <N> Delete a

old net

<R> <F> Read a

PTP-sequences

<W> DELETION of PTP-sequences

session report

<D> delete the session

single output transitions

<V> DELETION of single

depth restriction

Tiefenbeschränkung

diagonal

Gefärbte Netze

Dialog mit INA

2.2 Generelle Regeln für

Disjunktive Normalform

Zustandsprädikate

distances

<A> compute distances

Distanzen

<A> compute distances

don't care

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

DSt

DSt: Erreichbarkeit eines toten

DTP

DTP: Deadlock-Falle-Eigenschaft - deadlock-trap-property

DTr

DTr: Tote Transition bei | <L> check liveness properties

duplicate

<N> <D> Node Doubling

durations

<D> durations

Durchlaßfenster

<I> intervals | Zeitoption Intervalle für Bögen | Zeitoption Intervalle für Bögen

dynamic conflicts

<Y> check dynamic conflicts

dynamically conflictfree

DCF: Dynamische Konfliktfreiheit - | <Y> check dynamic conflicts

Dynamische Konflikte

<Y> check dynamic conflicts

Dynamische Konfliktfreiheit

DCF: Dynamische Konfliktfreiheit - | <Y> check dynamic conflicts

EBNF-Syntax

2.3.4 Dateiformate

Editor

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

Menü

3. Editor

EFC

EFC: Extended-Free-Choice-Netz - extended

eft/lft

<I> intervals | Zeitoption Intervalle für Transitionen eft/lft | Zeitoption Intervalle für Transitionen eft/lft

Eingabe

2.2 Generelle Regeln für

editieren

Editieren der Eingabe

fortsetzen

Ungefärbte Netze

Name

2.3.3 Eingabe von Netzen

Netz

2.3.3 Eingabe von Netzen | <R> <T> Read a

Nummer

2.3.3 Eingabe von Netzen

Platz

2.3.3 Eingabe von Netzen | <R> <N> Read a

Transition

<R> <N> Read a

eliminated columns

<B> Decide structural boundedness | <N> Non-reachability test of

elimination

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

looping places

<C> ELIMINATION of looping

enabledness predicate

<E> define an enabledness

Erreichbarkeit

,,schlechter`` Zustand

BSt: Schlechter Zustand erreichbar

toter Zustand

DSt: Erreichbarkeit eines toten | <D> Check the deadlock-trap-,

transienter Zustand

Zeitoption Dauer für Transitionen | 6.5.3 Pfadberechnung | 6.5.4 Graphberechnung und -analyse

Erreichbarkeitsgraph

stur reduziert

Sture Reduktion

symmetrisch reduziert

Symmetrische Reduktion

ES

ES: Extended-Simple-Netz - extended

esc

Besondere Tasten und Zeichen | Eingabe von Namen

.exc

2.3.2 Dateiextensionen | <X> change eXceptions

exceptions ok after reset

<I> reset to the

expected

<F> check a CTL-formula

Expertsystem

6.1 Grundlagen

extended free choice

EFC: Extended-Free-Choice-Netz - extended

extended simple

ES: Extended-Simple-Netz - extended

Extended-Free-Choice-Netz

EFC: Extended-Free-Choice-Netz - extended

Extended-Simple-Netz

ES: Extended-Simple-Netz - extended

Fakten

Vorwort

tote Transitionen

<L> check liveness properties

Falle

DTP: Deadlock-Falle-Eigenschaft - deadlock-trap-property

Falten

<C> coloured tokens

Farben

eingeben

Gefärbte Netze

isolierte

<D> <I> Delete all

löschen

<D> <C> Delete a

Option

<C> coloured tokens

verwerfen

<C> coloured tokens

Farbmengen

Gefärbte Netze

FC

FC: Free-Choice-Netz - free

Fehlerkorrektur

Editieren der Eingabe

fire maximal steps

<S> fire maximal steps

fire single transitions

<T> fire single transitions

fire the first element

<cr> fire the first

firing rule

2.5.3 Schaltregel

firing strategie

2.5.5 Schaltstrategie

first component

Gefärbte Netze

first part deleted

<D> delete the session

fixpoints

<Y> Compute the symmetries

Fixpunkte

<Y> Compute the symmetries

fold the net

<C> coloured tokens

forget the colour structure

<C> coloured tokens

forget the net

2.4.1 Aufruf und Beenden

format lines

<F> Format lines written

Fp0

Fp0: Platz ohne Vortransition

free choice

FC: Free-Choice-Netz - free

Free-Choice-Netz

FC: Free-Choice-Netz - free

Ft0

Ft0: Transition ohne Vorplatz

function sequence

<S> repeat function sequence

fusion of congruent nodes

<F> Fusion of congruent

gefärbte Netze

Gefärbte Netze | <C> coloured tokens

Generatoren

<Y> Compute the symmetries

generators

<Y> Compute the symmetries

Gewöhnlichkeit

ORD: Gewöhnlichkeit - ordinary

graph matrix

<M> write the matrix

Graphanalyse

Weitere Graphanalyse to <I> inspect a result

CTL-Modelchecking

CTL-Modelchecking und Prädikatdefinition

Distanzen

<A> compute distances

dynamische Konflikte

<Y> check dynamic conflicts

Erreichbarkeitstest

<R> test the reachability/coverability

Kreise

<K> compute circuits

Lebendigkeit

<L> check liveness properties

Matrixdarstellung

<M> write the matrix

Prädikate

<E> define an enabledness

Schreibfunktionen

Schreibfunktionen

st. Zusammenhangskompo.

<V> compute strongly connected

Graphberechnung

<R> Compute a reachability to Ablauf der Berechnung

Ablauf

Ablauf der Berechnung

Berechnungsarten

Berechnungsart

Dateien anzeigen

Dateien anzeigen

Optionen

Optionen

Reduktionen

6.5.1 Reduktionen des Zustandsgraphen

stur reduziert

Sture Reduktion | <R> Compute a reachability

symmetrisch reduziert

Symmetrische Reduktion | <R> Compute a reachability

Tiefenbeschränkung

Tiefenbeschränkung

Überdeckbarkeit

Überdeckbarkeitsgrahen | <G> Compute a coverability

nach Finkels Methode

Finkels Methode zur Berechnung | <G> Compute a coverability

überdeckende Markierung

Ablauf der Berechnung

unvollständig

Ablauf der Berechnung

halt

2.3.1 Wichtige Dateien

Hauptmenü

2.4.1 Aufruf und Beenden

his

Gefärbte Netze

.hlp

2.3.2 Dateiextensionen | <F> Format lines written

HOM

HOM: Homogenität - homogenous

Homogenität

HOM: Homogenität - homogenous

homogenous

HOM: Homogenität - homogenous

.icp

2.3.2 Dateiextensionen | <C> <I> Change Initial

.ict

2.3.2 Dateiextensionen | <C> <I> Change Initial

identity is the only symmetry

<Y> Compute the symmetries

incidence matrix

6.6.1 Invariantenberechnung | <M> show (transposed) incidence

ININET.pnt

2.3.1 Wichtige Dateien | <I> reset to the

initial state is transient

Zeitoption Dauer für Transitionen

initial state to be symmetric

<Y> Compute the symmetries

Initiale Uhrenstellung

ändern

<C> <I> Change Initial

eingeben

Ungefärbte Netze

Installation

2.1 Startvorbereitungen

interactive mode

Interaktive Berechnung

intervals

<I> intervals

.inv

2.3.2 Dateiextensionen | <T> complete table | <I> Compute a base | <F> Format lines written | <O> open files (input

INVARI.hlp

2.3.1 Wichtige Dateien | <S> Compute a base | <F> Format lines written

invariant

base

<I> Compute a base

semiposotive

6.6.2 Semipositive Invarianten

sub

Semipositive (Sub/Sur)-Invarianten

sur

Semipositive (Sub/Sur)-Invarianten

Invarianten

6.6 Invariantenanalyse

Ausgabeformate

Inzidenzmatrix | Interaktive Berechnung | <F> change output format

automatische Berechnung

Bemerkungen zur Komplexität

Basisberechnung

<I> Compute a base

semipositiv

<S> Compute a base

Dateien

<O> open files (input

Eigenschaftstest

<P> give properties of

Formatierung

Formatierung von Invarianten

Gleichungsresultat

<B> give results of

interaktive Berechnung

Bemerkungen zur Komplexität

Interpretation

<I> Compute a base

Inzidenzmatrix

6.6.1 Invariantenberechnung | <M> show (transposed) incidence

Komplexität

Bemerkungen zur Komplexität

Konsistenztest

<O> open files (input

Nichterreichbarkeitstest

Schneller Nichterreichbarkeitstest

Optionen

6.6.1 Invariantenberechnung | Interaktive Berechnung

semipositive

<#> print non-zero entries | 6.6.2 Semipositive Invarianten

sub

Semipositive (Sub/Sur)-Invarianten

Support

Ausgabeformate

sur

Semipositive (Sub/Sur)-Invarianten

testen

<T> Test place- or

Träger

Ausgabeformate

Vektor

ausgeben

<W> write vector

Eigenschaften

<P> give properties of

eingeben

<R> read vector

lesen

<R> read vector

schreiben

<W> write vector

testen

<T> Test place- or

Inzidenzmatrix

6.6.1 Invariantenberechnung | <M> show (transposed) incidence

jump mode

<R> read vector

Kapazität

eingeben

Ungefärbte Netze

Kapazitäten

<C> normal firing rule

ändern

<C> <C> Change Capacities

benötigt

Ablauf der Berechnung

unendliche

Besondere Tasten und Zeichen | <C> normal firing rule

Kapazitätsschaltregel

<C> normal firing rule

Knoten

äquivalente

<M> Merging of equivalent

eingeben

<R> <N> Read a

einseitige

Einseitige Knoten

isolierte

<D> <I> Delete all

löschen

<D> <N> Delete a

parallele

<F> Fusion of congruent

verdoppeln

<N> <D> Node Doubling

verschmelzen

<M> <O> Merge two

Kollektive Lebendigkeit

CL : Kollektive Lebendigkeit | <L> check liveness properties

Kommandos

erneut ausführen

2.4.1 Aufruf und Beenden

speichern

2.4.1 Aufruf und Beenden

unterbrechen

2.4.1 Aufruf und Beenden

Kommentare

Hinweis

Komponenten

berechnen

<C> Compute all components

starker Zusammenhang

<M> Decide state-machine coverability

Zustandsmaschine

<M> Decide state-machine coverability

Konflikt

dynamisch

<Y> check dynamic conflicts

statisch

Voranalyse

Konflikte

von Schritten

<Y> check dynamic conflicts

Konfliktfreiheit

dynamische

DCF: Dynamische Konfliktfreiheit - | <Y> check dynamic conflicts

statische

SCF: Statische Konfliktfreiheit - | Voranalyse

Konservativität

CSV: Konservativität - conservativ

Korrektur

Editieren der Eingabe

Kreise

<K> compute circuits

L

L : Lebendigkeit -

L&S

L&S: Lebendig und Sicher

Laufplatz

<R> <P> Insert a

Lebendigkeit

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

kollektive

CL : Kollektive Lebendigkeit | <L> check liveness properties

schwache

WL : Schwache Lebendigkeit | <L> check liveness properties

Test

<L> check liveness properties

und Sicherheit

L&S: Lebendig und Sicher

unter Ign. toter Transitionen

LV : Lebendigkeit (unter | <L> check liveness properties

line length

2.5.6 Zeilenlänge

lines input file

<F> Format lines written | <F> Format lines written

live

L : Lebendigkeit -

live and safe

L&S: Lebendig und Sicher

livelock

<K> compute circuits | <K> compute circuits

liveness test

<L> check liveness properties

loop

<R> <L> Add a | Zeitoption Dauer für Transitionen

lower bound

Zustandsprädikate

LV

LV : Lebendigkeit (unter | <L> check liveness properties

.mar

2.3.2 Dateiextensionen | <C> <T> Change the | <W> Write the actual

marked graph

MG: Synchronisationsgraph - marked

Markenart

2.5.1 Markenarten

Markierung

ändern

<C> <T> Change the

maximal steps

<S> fire maximal steps

merge

equivalent places

<M> Merging of equivalent

two nets

<M> <N> Merge two

two nodes

<M> <O> Merge two

MG

MG: Synchronisationsgraph - marked

mine

Gefärbte Netze

Modelchecking

Modelchecking | CTL-Modelchecking und Prädikatdefinition

Namensvorgabe

Dateianforderungen

NBM

NBM: Nichtblockierende Vielfachheit -

needed capacities

Ablauf der Berechnung

Netz

abspeichern

<W> <F> Write the

ausgeben

<W> <T> Write the

eingeben

2.3.3 Eingabe von Netzen | <R> <T> Read a

einlesen

<R> <F> Read a

elementare Eigenschaften

6.2.1 Elementare Netzeigenschaften

entfalten

<C> coloured tokens

Erreichbarkeitsanalyse

6.5 Erreichbarkeitsanalyse

falten

<C> coloured tokens | <C> coloured tokens

Farben verwerfen

<C> coloured tokens

gefärbt

Gefärbte Netze | <C> coloured tokens

Information

<W> <T> Write the

initiale Uhrenstellung

<C> <I> Change Initial

Inzidenzmatrix

6.6.1 Invariantenberechnung | <M> show (transposed) incidence

Kapazitäten

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

Kommentare

Hinweis

löschen

<D> <T> Delete the

Laufplatz

<R> <P> Insert a

lebendig

6.6 Invariantenanalyse

löschen

unvollständiges

<Q> Quit the editing

Markenart

2.5.1 Markenarten

Markierung

<C> <T> Change the

Name

Ungefärbte Netze

ändern

<C> <N> Change Names

Nummer

Ungefärbte Netze

ändern

<C> <U> Change nUmbers

Platz/Transition

<B> black (indistinguishable) tokens

Platzmenge analysieren

<W> <F> Write the

Prioritäten

2.5.4 Prioritäten | <C> <P> Change Priorities

Schleife

<R> <L> Add a | Zeitoption Dauer für Transitionen

selbstmodifizierendes

Vorwort

ungefärbt

Ungefärbte Netze

unvollständiges

3. Editor

verschmelzen

<M> <N> Merge two

verwerfen

2.4.1 Aufruf und Beenden

Voranalyse

Voranalyse

Zeitbewertung

2.5.2 Zeitoption

next conjunction

Zustandsprädikate

Nichtblockierende Vielfachheit

NBM: Nichtblockierende Vielfachheit -

Nichterreichbarkeit

über Invarianten

Schneller Nichterreichbarkeitstest

über Zustandsgl.

6.4.2 Schneller Nichterreichbarkeitstest

no application possible

5.1 Grundlagen

no decision possible

<P> Compute a shortest | <F> check a CTL-formula

no net present

3. Editor

no times

<N> no times

node doubling

<N> <D> Node Doubling

nodeoverflow

<P> Compute a shortest

non-reachability test

6.4.2 Schneller Nichterreichbarkeitstest | Schneller Nichterreichbarkeitstest

non-zero entries

<E> print non-zero entries

nonblocking multiplicity

NBM: Nichtblockierende Vielfachheit -

normal firing rule

<N> normal firing rule

with capacities

<C> normal firing rule

not found

Eingabe von Namen | <F> Format lines written

not sufficiently marked

<D> Check the deadlock-trap-,

omit boundedness test

Ablauf der Berechnung

only places/transitions present

3. Editor

oo

Besondere Tasten und Zeichen | <C> normal firing rule

Optionen

2.3.1 Wichtige Dateien | 2.5 Optionen | 2.5 Optionen to 2.5.6 Zeilenlänge

Markenart

2.5.1 Markenarten

nach dem Start

2.5 Optionen

Prioritäten

2.5.4 Prioritäten

Schaltregel

2.5.3 Schaltregel

Schaltstrategie

2.5.5 Schaltstrategie

Zeilenlänge

2.5.6 Zeilenlänge

Zeitoption

2.5.2 Zeitoption

OPTIONS.ina

Vorwort | 2.3.1 Wichtige Dateien | 2.4.1 Aufruf und Beenden | 2.5 Optionen

ORD

ORD: Gewöhnlichkeit - ordinary

ordinary

ORD: Gewöhnlichkeit - ordinary

output file

Speichern von Daten

output format

Ausgabeformate | Ausgabeformate | <F> change output format

overloaded

<C> normal firing rule

overwrite

Speichern von Daten

.pdc

2.3.2 Dateiextensionen | Zustandsprädikate

pF0

pF0: Platz ohne Nachtransition

Pfadberechnung

6.5.3 Pfadberechnung

durch Backtracking

<R> test the reachability/coverability

Ergebnisanzeige

Ergebnisanzeige

Philosophen

Abbildung

Gefärbte Netze

Datei

Beispiel für eine .cnt-Datei

Eingabe

Gefärbte Netze

kompletter Durchlauf

4.5 Beispiel

Toter Zustand

4.5 Beispiel

place

without posttransition

pF0: Platz ohne Nachtransition

without pretransition

Fp0: Platz ohne Vortransition

Platz

ausgeben

<W> <T> Write the

beschränkt

Semipositive (Sub/Sur)-Invarianten | <M> Decide state-machine coverability

eingeben

Ungefärbte Netze | <R> <N> Read a

Invariante

6.6 Invariantenanalyse

Kapazität

<C> normal firing rule

Laufplatz

<R> <P> Insert a

Name

Ungefärbte Netze

ändern

<C> <N> Change Names

Nummer

Ungefärbte Netze

ändern

<C> <U> Change nUmbers

ohne Nachtransition

pF0: Platz ohne Nachtransition

ohne Vortransition

Fp0: Platz ohne Vortransition

überladen

<C> normal firing rule

Verweildauer

Vorwort

Platzinvariantenüberdeckbarkeit

CPI: Platzinvariantenüberdeckbarkeit - covered

.pnt

2.3.2 Dateiextensionen | Syntax der .pnt-Datei

Prädikat

Atom

Zustandsprädikate

aus Zustandsmenge

<C> convert a set

,,bad``

,,Bad`` Prädikat

Disjunktive Normalform

Zustandsprädikate

Funktionen

CTL-Modelchecking und Prädikatdefinition

zur Transitionskonzession

<E> define an enabledness

predicate

Zustandsprädikate

bad

,,Bad`` Prädikat

convert a set of states

<C> convert a set

enabledness

<E> define an enabledness

.prf

2.3.2 Dateiextensionen | <F> check a CTL-formula | <I> inspect a result

.pri

2.3.2 Dateiextensionen | <C> <P> Change Priorities

Priorität

eingeben

Ungefärbte Netze

Prioritäten

2.5.4 Prioritäten

ändern

<C> <P> Change Priorities

priorities

2.5.4 Prioritäten

program a sequence of reduction steps

<P> Program a sequence

Programmende

2.4.1 Aufruf und Beenden

Programmstart

2.4.1 Aufruf und Beenden

proof

<F> check a CTL-formula

properties of the vector

<P> give properties of

proposal

<S> Compute a base

PUR

PUR: Reinheit - pure

pure

PUR: Reinheit - pure

quit

2.4.1 Aufruf und Beenden

Rücksetzbarkeit

REV: Reversibilität - reversible | <V> compute strongly connected

raise node numbers with exceptions

<R> Raise node numbers

reachabel

transient markings

6.5.3 Pfadberechnung

reachability test

<P> Compute a shortest | <O> Compute a minimal | <R> test the reachability/coverability

reachable

bad state

BSt: Schlechter Zustand erreichbar

dead state

DSt: Erreichbarkeit eines toten

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

read the session report

<S> read the session

.red

2.3.2 Dateiextensionen | <N> save the actual

Reduktion

5. Reduktion to <W> DELETION of PTP-sequences

Äquivalente Knoten

<M> Merging of equivalent

abbrechen

5.1 Grundlagen

Ausnahmen

<X> change eXceptions

Elimination

Laufplätze

<C> ELIMINATION of looping

Schleifen

<U> DELETION of looping

Knotennummern

erhöhen

<R> Raise node numbers

verdichten

<S> Squeeze the node

Löschen

PTP-Sequenzen

<W> DELETION of PTP-sequences

Menü

5.1 Grundlagen

Netz

ausgeben

<O> terminal Output of

speichern

<N> save the actual

zurücksetzen

<I> reset to the

Parallele Knoten

<F> Fusion of congruent

Programm

<P> Program a sequence

Verschmelzen

Vor- mit Nachplätzen

<V> DELETION of single

Vor- mit Nachtransitionen

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

Zusammenhangstest

<T> connectedness Test

Reinheit

PUR: Reinheit - pure

rename SESSION.ina

2.4.1 Aufruf und Beenden

.res

2.3.2 Dateiextensionen | <V> compute strongly connected | <M> write the matrix | <I> inspect a result | <T> complete table | <I> Compute a base | <O> open files (input

reset to the initial net

<I> reset to the

reset to the initial state

<R> Reset to the

resetable

REV: Reversibilität - reversible | <V> compute strongly connected

results by other format

<I> Compute a base

results incomplete

<F> Format lines written

results of equations

<B> give results of

returning heap

6.1 Grundlagen

REV

REV: Reversibilität - reversible | <V> compute strongly connected

Reversibilität

REV: Reversibilität - reversible | <V> compute strongly connected

reversible

REV: Reversibilität - reversible | <V> compute strongly connected

run-place

<R> <P> Insert a

safe and live

L&S: Lebendig und Sicher

safe firing rule

<S> safe firing rule

same procedure as last time

2.3.1 Wichtige Dateien | 2.4.1 Aufruf und Beenden

save commands to COMMAND.ina

2.4.1 Aufruf und Beenden

SB

SB : Strukturelle Beschränktheit | 6.4.1 Schneller Beschränktheitstest

SC

SC: Starker Zusammenhang -

SC-components

<V> compute strongly connected

SCF

SCF: Statische Konfliktfreiheit -

Schaltdauer

<D> durations | Zeitoption Dauer für Transitionen | Zeitoption Dauer für Transitionen

Schalten

4. Schalten | 4. Schalten to 4.5 Beispiel | 5. Reduktion

Funktionen

4.4.1 Allgemeines

Hilfsfunktionen

4.3 Hilfsfunktionen

Menü

4.1 Grundlagen

unter Zeitbewertung

4.4.2 Schalten unter Zeitbewertung

Schaltliste

4.4.1 Allgemeines | <S> write the list

Schaltregel

2.5.3 Schaltregel

Schaltstrategie

2.5.5 Schaltstrategie

Schleife

<R> <L> Add a | Zeitoption Dauer für Transitionen

Schleifenfreiheit

PUR: Reinheit - pure

Schritt

<S> fire maximal steps | Zeitoption Intervalle für Bögen

Konflikte

<Y> check dynamic conflicts

Lebendigkeit

<L> check liveness properties

Liste

<S> write the list

Schrittschaltregel

<S> fire maximal steps

Schwache Lebendigkeit

WL : Schwache Lebendigkeit | <L> check liveness properties

second component

Gefärbte Netze

sequential mode

<R> read vector

session output file

2.4.1 Aufruf und Beenden

Session-Report

2.4.2 Der Session-Report

löschen

<D> delete the session

lesen

<S> read the session

SESSION.ina

2.3.1 Wichtige Dateien | 2.4.1 Aufruf und Beenden | 2.5.6 Zeilenlänge | <I> inspect a result

set remaining components to zero

<R> read vector

show all stubborn sets

<A> All minimal stubborn

show stubborn sets

<S> Show the stubborn

Sichere Schaltregel

<S> safe firing rule

Sicherheit

L&S: Lebendig und Sicher

single transitions

<T> fire single transitions

skip lines

<F> Format lines written

SM

SM: Zustandsmaschine - state | <C> Compute all components

SMA

SMA: Zustandsmaschinenauswählbarkeit - state | <D> Check the deadlock-trap-, | <C> Compute all components

SMC

SMC: Zustandsmaschinenüberdeckbarkeit - state | <M> Decide state-machine coverability

SMD

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

space

Besondere Tasten und Zeichen | Editieren der Eingabe

Speicher freigeben

6.1 Grundlagen

Speichern

von Daten

Speichern von Daten

von Kommandos

2.4.1 Aufruf und Beenden

squeeze the node numbers

<S> Squeeze the node

.sta

2.3.2 Dateiextensionen | <W> write all computed | <I> inspect a result

stabilisation time

Zeitoption Dauer für Transitionen

standard

Gefärbte Netze

Standardoptionen

2.5 Optionen

Starker Zusammenhang

SC: Starker Zusammenhang -

Starten von INA

2.4.1 Aufruf und Beenden

Vorbereitungen

2.1 Startvorbereitungen

state machine

SM: Zustandsmaschine - state | <M> Decide state-machine coverability

state machine allocatable

SMA: Zustandsmaschinenauswählbarkeit - state

state machine coverability

<M> Decide state-machine coverability

state machine coverable

SMC: Zustandsmaschinenüberdeckbarkeit - state

state machine decomposable

SMD: Zustandsmaschinendekomponierbarkeit - state

states generated

<P> Compute a shortest | Ablauf der Berechnung

STATES.gra

Vorwort

static conflict free

SCF: Statische Konfliktfreiheit -

static conflicts

Voranalyse

Statische Konflikte

Voranalyse

Statische Konfliktfreiheit

SCF: Statische Konfliktfreiheit - | Voranalyse

step live

<L> check liveness properties

steplist

<S> write the list

stopped

5.1 Grundlagen

strongly connected

SC: Starker Zusammenhang -

structurally bounded

SB : Strukturelle Beschränktheit | 6.4.1 Schneller Beschränktheitstest

Strukturanalyse

6.7 Strukturanalyse

Strukturelle Beschränktheit

SB : Strukturelle Beschränktheit

schneller Test

6.4.1 Schneller Beschränktheitstest

Strukturen

Strukturen | 6.7 Strukturanalyse

Sture Mengen

Sture Reduktion

anzeigen

<S> Show the stubborn

subconservativ

CSV: Konservativität - conservativ

Subkonservativität

CSV: Konservativität - conservativ

supports

Ausgabeformate

Symmetrien

Anfangszustand

<Y> Compute the symmetries

berechnen

<Y> Compute the symmetries

Fixpunkte

<Y> Compute the symmetries

Generatoren

<Y> Compute the symmetries

symmetries

<Y> Compute the symmetries

Synchronisationsgraph

MG: Synchronisationsgraph - marked

Syntax

.pnt-Datei

Syntax der .pnt-Datei

.cnt-Datei

Syntax der .cnt-Datei

Platzeingabe

Ungefärbte Netze

Transitionseingabe

<R> <N> Read a

terminal

Umschaltung in den Terminalmodus

Terminalmodus

Umschaltung in den Terminalmodus

Test

Überdeckbarkeit

<R> test the reachability/coverability

auf Zusammenhang

<T> connectedness Test

Erreichbarkeit

<R> test the reachability/coverability

Lebendigkeit

<L> check liveness properties

von Schritten

<L> check liveness properties

Nichterrreichbarkeit

6.4.2 Schneller Nichterreichbarkeitstest | Schneller Nichterreichbarkeitstest

Rücksetzbarkeit

<V> compute strongly connected

Zusammenhang

<T> <C> Test Connectedness

test connectedness

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

test liveness of steps

<L> check liveness properties

test vectors for invariant props

<T> Test place- or

tF0

tF0: Transition ohne Nachplatz

.tim

2.3.2 Dateiextensionen

time option

2.5.2 Zeitoption

timetick

Zeitoption Intervalle für Transitionen eft/lft

.tmd

2.3.2 Dateiextensionen

token type

2.5.1 Markenarten

.tra

2.3.2 Dateiextensionen | <P> Compute a shortest | <R> test the reachability/coverability | <I> inspect a result

transient state

<R> <L> Add a | Zeitoption Dauer für Transitionen

Transiente Zustände

<R> <L> Add a | Zeitoption Dauer für Transitionen | Zeitoption Intervalle für Bögen | 6.5.3 Pfadberechnung

Transition

ausgeben

<W> <T> Write the

bei Anfangsmarkierung tot

DTr: Tote Transition bei | <L> check liveness properties

Bewertung

<K> compute circuits

eft/lft

<I> intervals

eingeben

<R> <N> Read a

im Livelock

<K> compute circuits

Invariante

6.6 Invariantenanalyse

realisierbare

<K> compute circuits

Name

Ungefärbte Netze

ändern

<C> <N> Change Names

Nummer

Ungefärbte Netze

ändern

<C> <U> Change nUmbers

ohne Nachplatz

tF0: Transition ohne Nachplatz

ohne Vorplatz

5.1 Grundlagen | Ft0: Transition ohne Vorplatz

Schaltdauer

<D> durations

tot

<D> Check the deadlock-trap-,

without postplace

tF0: Transition ohne Nachplatz

without preplace

Ft0: Transition ohne Vorplatz

transition without preplace

5.1 Grundlagen

Transitionsinvariantenüberdeckbarkeit

CTI: Transitionsinvariantenüberdeckbarkeit - covered | 6.6 Invariantenanalyse

trivial transition partition

<Y> Compute the symmetries

Überblick

1.1 Überblick

Überdeckbarkeit

mit Platzinvarianten

CPI: Platzinvariantenüberdeckbarkeit - covered

mit Transitionsinvarianten

CTI: Transitionsinvariantenüberdeckbarkeit - covered | 6.6 Invariantenanalyse

Überdeckbarkeitsgraph

Überdeckbarkeitsgrahen | <G> Compute a coverability

nach Finkels Methode

Finkels Methode zur Berechnung

upper bound

Zustandsprädikate

.val

2.3.2 Dateiextensionen | <O> Compute a minimal | <K> compute circuits

Vielfachheit

Ungefärbte Netze

ändern

<R> <A> Read an

ändern

<C> <M> Change Multiplicities

nichtblockierend

NBM: Nichtblockierende Vielfachheit -

Voranalyse

Voranalyse

weakly live

WL : Schwache Lebendigkeit | <L> check liveness properties

witnesses

<F> check a CTL-formula

WL

WL : Schwache Lebendigkeit | <L> check liveness properties

write

marking to file

<W> Write the actual

the net to a file

<W> <F> Write the

the net to the terminal

<W> <T> Write the

Zeilenlänge

2.5.6 Zeilenlänge

Zeitbewertung

2.5.2 Zeitoption

Schalten

4.4.2 Schalten unter Zeitbewertung

Zustand

4.2.2 Zustandsdarstellung unter Zeitbewertung

Zeitoption

2.5.2 Zeitoption

zero

Gefärbte Netze

Zusammenhang

CON: Zusammenhang - connected

starker

SC: Starker Zusammenhang -

Test

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

Zustand

mit Zeitbewertung

4.2.2 Zustandsdarstellung unter Zeitbewertung

ohne Zeitbewertung

4.2.1 Zustandsdarstellung ohne Zeitbewertung

,,schlecht``

BSt: Schlechter Zustand erreichbar | 6.5.4 Graphberechnung und -analyse | <B> write the bad

stabil

Zeitoption Dauer für Transitionen | Zeitoption Intervalle für Bögen

tot

DSt: Erreichbarkeit eines toten | 6.5.3 Pfadberechnung | 6.5.4 Graphberechnung und -analyse | <D> write the dead

transient

<R> <L> Add a | Zeitoption Dauer für Transitionen | Zeitoption Intervalle für Bögen | 6.5.3 Pfadberechnung | 6.5.4 Graphberechnung und -analyse

Zustandsgraph

Bogenanzahl

Ablauf der Berechnung

stur reduziert

Sture Reduktion

symmetrisch reduziert

Symmetrische Reduktion

Zustandsanzahl

Ablauf der Berechnung

Zustandsmaschine

SM: Zustandsmaschine - state

Überdeckbarkeit

<M> Decide state-machine coverability

Auswählbarkeit

SMA: Zustandsmaschinenauswählbarkeit - state | <D> Check the deadlock-trap-,

Dekomponierbarkeit

SMD: Zustandsmaschinendekomponierbarkeit - state | <D> Check the deadlock-trap-,

Überdeckbarkeit

SMC: Zustandsmaschinenüberdeckbarkeit - state