Index

#

Editieren der Eingabe

?

Editieren der Eingabe

Abbruch beim Invarianteneinlesen

<O> open files , <W> write vector

Abbruch durch Delete-Taste

Editieren der Eingabe

Abbruch durch Pfadnamen

Eingabe von Namen

Abbruch durch Sonderzeichen in Dateinamen

Eingabe von Namen

Abbruch eines Kommandos

2.4.1 Aufruf und Beenden

Abbruch Symmetrieberechnung

<Y> Compute the

Abbruch unter DOS

Installation unter DOS

Abfragen beantworten

2.2 Generelle Regeln für

actual net do not match

<F> Format lines

Analyse

(, 6 Analyse, )

Analyse Überdeckbarkeitsgraph

<A> Analyse the

Analyse Erreichbarkeitsgraph

<A> Analyse the

analyse graph

<A> Analyse the

Analyse Invarianten

6.5 Invariantenanalyse

analyse invariants

6.5 Invariantenanalyse

Analyse mehrerer Netze

2.4.3 Analyse mehrerer Netze

Analyse Menü

6.3 Analysemenü und Voranalyse

Analyse Platzmenge

<W> <F> Write

Analyse Status

6.2 Analysestatus

analyse structure

6.6 Strukturanalyse

Analyse Strukturen

6.6 Strukturanalyse

Analyse Voranalyse

Voranalyse

.atm

2.3.2 Dateiextensionen

Aufruf von INA

2.4.1 Aufruf und Beenden

Aufruf von INA Vorbereitungen

2.1 Startvorbereitungen

automatic mode

Interaktive Berechnung

B

B : Beschränktheit -

back to previous state

<B> Back to

backspace

Editieren der Eingabe

backtracking

Erreichbarkeits-/Überdeckbarkeitstest

bad state reachable

BSt: Fakt hat Konzession

Baumdarstellung

Baumdarstellung des Zustandsgraphen

Beenden von INA

2.4.1 Aufruf und Beenden

Berechnung Überdeckbarkeitsgraph

Überdeckbarkeitsgrahen, <G> Compute a

Berechnung Überdeckbarkeitsgraph nach Finkels Methode

Finkels Methode zur Berechnung , <G> Compute a

Berechnung Deadlock-Falle-Eigenschaft

<D> Check the

Berechnung Distanzen

Berechnung der Distanzen

Berechnung dynamische Konflikte

Berechnung dynamischer Konflikte, Berechnung dynamischer Konflikte

Berechnung Erreichbarkeitsgraph

<R> Compute a

Berechnung Erreichbarkeitsgraph stur reduziert

Sture Reduktion, <R> Compute a

Berechnung Erreichbarkeitsgraph symmetrisch reduziert

Symmetrische Reduktion, <R> Compute a

Berechnung Invariantenbasis

<I> Compute a

Berechnung Invariantenbasis semipositiv

<S> Compute a

Berechnung kürzester Pfad

<P> Compute a

Berechnung Komponenten

<C> Compute all

Berechnung Kreise

Berechnung der Kreise

Berechnung Speicherüberlauf

<P> Compute a

Berechnung statische Konflikte

Voranalyse

Berechnung Symmetrien

<Y> Compute the

Berechnung terminale starke Zshangskomp.

Terminale starke Zusammenhangskomponenten und

Berechnung TSZK

Terminale starke Zusammenhangskomponenten und

Berechnung Zustandsgraph

<R> Compute a

Berechnung Zustandsgraph stur reduziert

Sture Reduktion, <R> Compute a

Berechnung Zustandsgraph symmetrisch reduziert

Symmetrische Reduktion, <R> Compute a

Beschränktheit

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

Beschränktheit strukturelle

SB : Strukturelle Beschränktheit

black tokens

<B> black (indistinguishable)

Bogen ändern

<R> <A> Read

Bogen Durchlaßfenster

<I> intervals

Bogen eingeben

<R> <A> Read

Bogen löschen

<R> <A> Read , <D> <A> Delete

bounded

B : Beschränktheit -

BSt

BSt: Fakt hat Konzession

.cap

2.3.2 Dateiextensionen, <C> <C> Change

change capacities

<C> <C> Change

change exceptions

<X> change eXceptions

change facts

<C> <F> Change

change initial times

<C> <I> Change

change marking

<C> <T> Change

change multiplicities

<C> <M> Change

change names

<C> <N> Change

change numbers

<C> <U> Change

change output format

Ausgabeformate, Ausgabeformate, <F> change output

change priorities

<C> <P> Change

change token load

<C> <T> Change

circuits

Berechnung der Kreise

CL

CL : Kollektive Lebendigkeit , Lebendigkeitstest

clean

<D> Check the , <M> Decide state-machine

clocked net elements

<I> intervals

.cnt

2.3.2 Dateiextensionen, Syntax der .cnt-Datei

collectively live

CL : Kollektive Lebendigkeit , Lebendigkeitstest

colour set

Gefärbte Netze

coloured tokens

<C> coloured tokens

COMMAND.ina

2.3.1 Wichtige Dateien, 2.4.1 Aufruf und Beenden

complete table

<T> complete table

compute coverability graph

Überdeckbarkeitsgrahen, <G> Compute a

compute coverability graph Finkels method

Finkels Methode zur Berechnung , <G> Compute a

compute invariants semipositive

6.5.2 Semipositive Invarianten

compute reachability graph

<R> Compute a

compute reachability graph stubborn reduced

Sture Reduktion, <R> Compute a

compute reachability graph symmetrical reduced

Symmetrische Reduktion, <R> Compute a

compute shortest path

<P> Compute a

compute state graph

<R> Compute a

compute symmetries

<Y> Compute the

computed graph not complete

Ablauf der Berechnung

CON

CON: Zusammenhang - connected

connected

CON: Zusammenhang - connected

connectedness test

<T> <C> Test , <T> connectedness Test

conservativ

CSV: Konservativität - conservativ

coverability test

Erreichbarkeits- bzw. Überdeckbarkeitstest, Erreichbarkeits-/Überdeckbarkeitstest

covered by place invariants

CPI: Platzinvariantenüberdeckbarkeit - covered

covered by transition invariants

CTI: Transitionsinvariantenüberdeckbarkeit - covered

CPI

CPI: Platzinvariantenüberdeckbarkeit - covered

cr

Besondere Tasten und Zeichen, Dateianforderungen

CSV

CSV: Konservativität - conservativ

CTI

CTI: Transitionsinvariantenüberdeckbarkeit - covered , 6.5 Invariantenanalyse

Darstellungsweise

1.2 Darstellungsweise

Datei überschreiben

Speichern von Daten

Datei Anforderung

Dateianforderungen

Datei EBNF-Beschreibungen

2.3.4 Dateiformate

Datei Extensionen

Eingabe von Namen, 2.3.2 Dateiextensionen

Datei Formate

2.3.4 Dateiformate

Datei Namensvorgabe

Dateianforderungen

Datei Namensvorgabe übernehmen

Eingabe von Namen

Datei speichern

Speichern von Daten

Datei Umschaltung in Terminalmodus

Umschaltung in den Terminalmodus

Datei wichtige

2.3.1 Wichtige Dateien

DCF

DCF: Dynamische Konfliktfreiheit - , Berechnung dynamischer Konflikte

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-property

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

delete

Editieren der Eingabe

delete all facts

<I> reset to

delete colour

<D> <C> Delete

delete exceptions

<X> change eXceptions

delete facts

<C> <F> Change

delete fragmented net

<Q> Quit the

delete input/output arcs

<D> <A> Delete

delete isolated colour

<D> <I> Delete

delete isolated nodes

<D> <I> Delete

delete looping transitions

<U> DELETION of

delete net

<D> <T> Delete

delete node

<D> <N> Delete

delete old net

<R> <F> Read

delete PTP-sequences

<W> DELETION of

delete session report

<D> delete the

delete single output transitions

<V> DELETION of

depth restriction

Tiefenbeschränkung

diagonal

Gefärbte Netze

Dialog mit INA

2.2 Generelle Regeln für

distances

Berechnung der Distanzen

Distanzen

Berechnung der Distanzen

don't care

6.4.1 Pfadberechnung

DSt

DSt: Erreichbarkeit eines toten

DTP

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

DTr

DTr: Tote Transition bei , Lebendigkeitstest

durations

<D> durations

Durchlaßfenster

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

dynamic conflicts

Berechnung dynamischer Konflikte

dynamically conflictfree

DCF: Dynamische Konfliktfreiheit - , Berechnung dynamischer Konflikte

Dynamische Konflikte

Berechnung dynamischer Konflikte

Dynamische Konfliktfreiheit

DCF: Dynamische Konfliktfreiheit - , Berechnung dynamischer Konflikte

EBNF-Syntax

2.3.4 Dateiformate

Editor

(, 3 Editor, )

Editor Menü

3 Editor

EFC

EFC: Extended-Free-Choice-Netz - extended

eft/lft

<I> intervals, Zeitoption Intervalle für Transitionen , Zeitoption Intervalle für Transitionen

Eingabe

2.2 Generelle Regeln für

Eingabe editieren

Editieren der Eingabe

Eingabe fortsetzen

Ungefärbte Netze

Eingabe Name

2.3.3 Eingabe von Netzen

Eingabe Netz

2.3.3 Eingabe von Netzen, <R> <T> Read

Eingabe Nummer

2.3.3 Eingabe von Netzen

Eingabe Platz

2.3.3 Eingabe von Netzen, <R> <N> Read

Eingabe Transition

<R> <N> Read

elimination

<A> ELIMINATION of , <B> ELIMINATION of

elimination looping places

<C> ELIMINATION of

Erreichbarkeit ,,schlechter`` Zustand

BSt: Fakt hat Konzession

Erreichbarkeit toter Zustand

DSt: Erreichbarkeit eines toten , <D> Check the

Erreichbarkeit transiente Zustände

6.4.1 Pfadberechnung

Erreichbarkeitsgraph

<R> Compute a

Erreichbarkeitsgraph Analyse

<A> Analyse the

Erreichbarkeitsgraph Baumdarstellung

Baumdarstellung des Zustandsgraphen

Erreichbarkeitsgraph Kreise

Berechnung der Kreise

Erreichbarkeitsgraph Matrixdarstellung

Matrixdarstellung des Zustandsgraphen

Erreichbarkeitsgraph stur reduziert

Sture Reduktion, <R> Compute a

Erreichbarkeitsgraph symmetrisch reduziert

Symmetrische Reduktion, <R> Compute a

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

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

fact

Ungefärbte Netze, <C> <F> Change

fact has concession

BSt: Fakt hat Konzession

Fakten ändern

<C> <F> Change

Fakten bei der Reduktion

5.1 Grundlagen

Fakten kennzeichnen

Ungefärbte Netze

Fakten Konzessionierung

4.4.1 Allgemeines, BSt: Fakt hat Konzession

Fakten tote Transitionen

Lebendigkeitstest

Falle

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

Falten

<C> coloured tokens

Farben isolierte

<D> <I> Delete

Farben löschen

<D> <C> Delete

Farben verwerfen

<C> coloured tokens

Farbmengen

Gefärbte Netze

FC

FC: Free-Choice-Netz - free

Fehlerkorrektur

Editieren der Eingabe

fire maximal steps

<S> fire maximal

fire single transitions

<T> fire single

fire the first element

<cr> fire the

firing rule

2.5.3 Schaltregel

firing strategie

2.5.5 Schaltstrategie

first component

Gefärbte Netze

first part deleted

<D> delete the

fixpoints

<Y> Compute the

Fixpunkte

<Y> Compute the

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

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

fusion of congruent nodes

<F> Fusion of

Gewöhnlichkeit

ORD: Gewöhnlichkeit - ordinary

.gra

2.3.2 Dateiextensionen, Ablauf der Berechnung

graph analysis is impossible

Ablauf der Berechnung

graph as tree

Baumdarstellung des Zustandsgraphen

graph input file

Ablauf der Berechnung

graph matrix

Matrixdarstellung des Zustandsgraphen

Graphanalyse

<A> Analyse the

Graphberechnung

<R> Compute a

Graphberechnung Überdeckbarkeit

Überdeckbarkeitsgrahen, <G> Compute a

Graphberechnung Überdeckbarkeit nach Finkels Methode

Finkels Methode zur Berechnung , <G> Compute a

Graphberechnung Ablauf

Ablauf der Berechnung

Graphberechnung Ausgabe

Ergebnisanzeige

Graphberechnung Berechnungsarten

Berechnungsarten

Graphberechnung Optionen

Optionen

Graphberechnung Reduktionen

6.4.2 Reduktionen des Zustandsgraphen

Graphberechnung stur reduziert

Sture Reduktion, <R> Compute a

Graphberechnung symmetrisch reduziert

Symmetrische Reduktion, <R> Compute a

Graphberechnung Tiefenbeschränkung

Tiefenbeschränkung

Graphberechnung unvollständig

Ablauf der Berechnung

Hauptmenü

2.4.1 Aufruf und Beenden

his

Gefärbte Netze

.hlp

2.3.2 Dateiextensionen, <F> Format lines

HOM

HOM: Homogenität - homogenous

Homogenität

HOM: Homogenität - homogenous

homogenous

HOM: Homogenität - homogenous

identity is the only symmetry

<Y> Compute the

incidence matrix

6.5.1 Invariantenberechnung, <M> show (transposed)

ININET.pnt

2.3.1 Wichtige Dateien, <I> reset to

initial state is transient

Zeitoption Dauer für Transitionen

initial state to be symmetric

<Y> Compute the

Initiale Uhrenstellung ändern

<C> <I> Change

Initiale Uhrenstellung eingeben

Ungefärbte Netze

Installation unter DOS

Installation unter DOS

Installation unter UNIX

Installation unter UNIX

interactive mode

Interaktive Berechnung

intervals

<I> intervals

.inv

2.3.2 Dateiextensionen, <T> complete table, <I> Compute a , <F> Format lines , <O> open files

INVARI.hlp

2.3.1 Wichtige Dateien, <S> Compute a , <F> Format lines

invariant base

<I> Compute a

invariant base semiposotive

6.5.2 Semipositive Invarianten

invariant sub

Semipositive (Sub/Sur)-Invarianten

invariant sur

Semipositive (Sub/Sur)-Invarianten

Invarianten

6.5 Invariantenanalyse

Invarianten Ausgabeformate

Inzidenzmatrix, Interaktive Berechnung, <F> change output

Invarianten automatische Berechnung

Bemerkungen zur Komplexität

Invarianten Basisberechnung

<I> Compute a

Invarianten Basisberechnung semipositiv

<S> Compute a

Invarianten Dateien

<O> open files

Invarianten Eigenschaftstest

<P> give properties

Invarianten Formatierung

Formatierung von Invarianten

Invarianten Gleichungsresultat

<B> give results

Invarianten interaktive Berechnung

Bemerkungen zur Komplexität

Invarianten Interpretation

<I> Compute a

Invarianten Inzidenzmatrix

6.5.1 Invariantenberechnung, <M> show (transposed)

Invarianten Komplexität

Bemerkungen zur Komplexität

Invarianten Konsistenztest

<O> open files

Invarianten Nichterreichbarkeitstest

Beispiel für eine Invarianteninterpretation

Invarianten Optionen

6.5.1 Invariantenberechnung, Interaktive Berechnung

Invarianten semipositive

<#> print non-zero , 6.5.2 Semipositive Invarianten

Invarianten sub

Semipositive (Sub/Sur)-Invarianten

Invarianten Support

Ausgabeformate

Invarianten sur

Semipositive (Sub/Sur)-Invarianten

Invarianten testen

<T> Test place-

Invarianten Träger

Ausgabeformate

Invarianten Vektor ausgeben

<W> write vector

Invarianten Vektor Eigenschaften

<P> give properties

Invarianten Vektor eingeben

<R> read vector

Invarianten Vektor lesen

<R> read vector

Invarianten Vektor schreiben

<W> write vector

Invarianten Vektor testen

<T> Test place-

Inzidenzmatrix

6.5.1 Invariantenberechnung, <M> show (transposed)

.itm

2.3.2 Dateiextensionen, <C> <I> Change

jump mode

<R> read vector

Kapazität eingeben

Ungefärbte Netze

Kapazitäten

<C> normal firing

Kapazitäten ändern

<C> <C> Change

Kapazitäten benötigt

Ergebnisanzeige

Kapazitäten unendliche

Besondere Tasten und Zeichen, <C> normal firing

Kapazitätsschaltregel

<C> normal firing

Knoten äquivalente

<M> Merging of

Knoten eingeben

<R> <N> Read

Knoten einseitige

Einseitige Knoten

Knoten isolierte

<D> <I> Delete

Knoten löschen

<D> <N> Delete

Knoten parallele

<F> Fusion of

Knoten verdoppeln

<N> <D> Node

Knoten verschmelzen

<M> <O> Merge

Kollektive Lebendigkeit

CL : Kollektive Lebendigkeit , Lebendigkeitstest

Kommandos erneut ausführen

2.4.1 Aufruf und Beenden

Kommandos speichern

2.4.1 Aufruf und Beenden

Kommandos unterbrechen

2.4.1 Aufruf und Beenden

Komponenten berechnen

<C> Compute all

Komponenten starker Zusammenhang

<M> Decide state-machine

Komponenten Zustandsmaschine

<M> Decide state-machine

Konflikt dynamisch

Berechnung dynamischer Konflikte

Konflikt statisch

Voranalyse

Konflikte von Schritten

Berechnung dynamischer Konflikte

Konfliktfreiheit dynamische

DCF: Dynamische Konfliktfreiheit - , Berechnung dynamischer Konflikte

Konfliktfreiheit statische

SCF: Statische Konfliktfreiheit - , Voranalyse

Konservativität

CSV: Konservativität - conservativ

Korrektur

Editieren der Eingabe

Kreise

Berechnung der Kreise

L

L : Lebendigkeit -

L&S

L&S: Lebendig und Sicher

Lebendigkeit

L : Lebendigkeit - , <D> Check the

Lebendigkeit kollektive

CL : Kollektive Lebendigkeit , Lebendigkeitstest

Lebendigkeit schwache

WL : Schwache Lebendigkeit , Lebendigkeitstest

Lebendigkeit Test

Lebendigkeitstest

Lebendigkeit und Sicherheit

L&S: Lebendig und Sicher

Lebendigkeit unter Ign. toter Transitionen

LV : Lebendigkeit (unter , Lebendigkeitstest

line length

2.5.6 Zeilenlänge

lines input file

<F> Format lines , <F> Format lines

live

L : Lebendigkeit -

live and safe

L&S: Lebendig und Sicher

Livelock

Berechnung der Kreise, Berechnung der Kreise

liveness test

Lebendigkeitstest

LV

LV : Lebendigkeit (unter , Lebendigkeitstest

.mar

2.3.2 Dateiextensionen, <C> <T> Change , <W> Write the

marked graph

MG: Synchronisationsgraph - marked

Markenart

2.5.1 Markenarten

Markierung ändern

<C> <T> Change

maximal outdegree

Berechnung dynamischer Konflikte

maximal steps

<S> fire maximal

merge equivalent places

<M> Merging of

merge two nets

<M> <N> Merge

merge two nodes

<M> <O> Merge

MG

MG: Synchronisationsgraph - marked

mine

Gefärbte Netze

Namensvorgabe

Dateianforderungen

NBM

NBM: Nichtblockierende Vielfachheit -

needed capacities

Ergebnisanzeige

Netz ändern

<C> <U> Change , <C> <N> Change

Netz abspeichern

<W> <F> Write

Netz ausgeben

<W> <T> Write

Netz eingeben

2.3.3 Eingabe von Netzen, <R> <T> Read

Netz einlesen

<R> <F> Read

Netz elementare Eigenschaften

6.2.1 Elementare Netzeigenschaften

Netz entfalten

<C> coloured tokens

Netz Erreichbarkeitsanalyse

6.4 Erreichbarkeitsanalyse

Netz falten

<C> coloured tokens, <C> coloured tokens

Netz Farben verwerfen

<C> coloured tokens

Netz gefärbt

Gefärbte Netze, <C> coloured tokens

Netz Information

<W> <T> Write

Netz initiale Uhrenstellung

<C> <I> Change

Netz Inzidenzmatrix

6.5.1 Invariantenberechnung, <M> show (transposed)

Netz Kapazitäten

<C> normal firing , <C> <C> Change

Netz löschen

<D> <T> Delete

Netz löschen unvollständiges

<Q> Quit the

Netz lebendig

6.5 Invariantenanalyse

Netz Markenart

2.5.1 Markenarten

Netz Markierung

<C> <T> Change

Netz Name

Ungefärbte Netze

Netz Nummer

Ungefärbte Netze

Netz Platz/Transition

<B> black (indistinguishable)

Netz Platzmenge analysieren

<W> <F> Write

Netz Prioritäten

2.5.4 Prioritäten, <C> <P> Change

Netz selbstmodifizierendes

<V> Valk's firing

Netz ungefärbt

Ungefärbte Netze

Netz unvollständiges

3 Editor

Netz verschmelzen

<M> <N> Merge

Netz verwerfen

2.4.1 Aufruf und Beenden

Netz Voranalyse

Voranalyse

Netz Zeitbewertung

2.5.2 Zeitoption

Nichtblockierende Vielfachheit

NBM: Nichtblockierende Vielfachheit -

no application possible

5.1 Grundlagen

no decision possible

<P> Compute a

no net present

3 Editor

no space for reachab. test

Erreichbarkeits-/Überdeckbarkeitstest

no times

<N> no times

node doubling

<N> <D> Node

nodeoverflow

<P> Compute a

non-reachability test

Beispiel für eine Invarianteninterpretation

non-zero entries

<E> print non-zero

nonblocking multiplicity

NBM: Nichtblockierende Vielfachheit -

normal firing rule

<N> normal firing

normal firing rule with capacities

<C> normal firing

not found

Eingabe von Namen, Ablauf der Berechnung, <F> Format lines

not sufficiently marked

<D> Check the

only places/transitions present

3 Editor

oo

Besondere Tasten und Zeichen, <C> normal firing

Optionen

2.3.1 Wichtige Dateien, (, 2.5 Optionen, )

Optionen beim Schreiben

Schreiboptionen

Optionen Markenart

2.5.1 Markenarten

Optionen nach dem Start

2.5 Optionen

Optionen Prioritäten

2.5.4 Prioritäten

Optionen Schaltregel

2.5.3 Schaltregel

Optionen Schaltstrategie

2.5.5 Schaltstrategie

Optionen Zeilenlänge

2.5.6 Zeilenlänge

Optionen Zeitoption

2.5.2 Zeitoption

OPTIONS.ina

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

overloaded

<C> normal firing

overwrite

Speichern von Daten

.pdl

2.3.2 Dateiextensionen

pF0

pF0: Platz ohne Nachtransition

Pfadberechnung

6.4.1 Pfadberechnung

Pfadberechnung durch Backtracking

Erreichbarkeits-/Überdeckbarkeitstest

Pfadberechnung Ergebnisanzeige

Ergebnisanzeige

Philosophen Abbildung

Gefärbte Netze

Philosophen Datei

Beispiel für eine .cnt-Datei

Philosophen Eingabe

Gefärbte Netze

Philosophen kompletter Durchlauf

4.5 Beispiel

Philosophen Toter Zustand

4.5 Beispiel

place without posttransition

pF0: Platz ohne Nachtransition

place without pretransition

Fp0: Platz ohne Vortransition

Platz ändern

<C> <U> Change , <C> <N> Change

Platz überladen

<C> normal firing

Platz ausgeben

<W> <T> Write

Platz beschränkt

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

Platz eingeben

Ungefärbte Netze, <R> <N> Read

Platz Invariante

6.5 Invariantenanalyse

Platz Kapazität

<C> normal firing

Platz Name

Ungefärbte Netze

Platz Nummer

Ungefärbte Netze

Platz ohne Nachtransition

pF0: Platz ohne Nachtransition

Platz ohne Vortransition

Fp0: Platz ohne Vortransition

Platz Verweildauer

<D> durations

Platzinvariantenüberdeckbarkeit

CPI: Platzinvariantenüberdeckbarkeit - covered

.pnt

2.3.2 Dateiextensionen, Syntax der .pnt-Datei

.pri

2.3.2 Dateiextensionen, <C> <P> Change

Priorität eingeben

Ungefärbte Netze

Prioritäten

2.5.4 Prioritäten

Prioritäten ändern

<C> <P> Change

priorities

2.5.4 Prioritäten

program a sequence of reduction steps

<P> Program a

Programmende

2.4.1 Aufruf und Beenden

Programmstart

2.4.1 Aufruf und Beenden

properties of the vector

<P> give properties

PUR

PUR: Reinheit - pure

pure

PUR: Reinheit - pure

quit

2.4.1 Aufruf und Beenden

Rücksetzbarkeit

REV: Reversibilität - reversible, Terminale starke Zusammenhangskomponenten und

raise node numbers with exceptions

<R> Raise node

reachabel transient markings

6.4.1 Pfadberechnung

reachability test

<P> Compute a , Erreichbarkeits- bzw. Überdeckbarkeitstest, Erreichbarkeits-/Überdeckbarkeitstest

reachable bad state

BSt: Fakt hat Konzession

reachable dead state

DSt: Erreichbarkeit eines toten

read a net from a file

<R> <F> Read

read a net from the terminal

<R> <T> Read

read a node from the terminal

<R> <N> Read

read an arc from the terminal

<R> <A> Read

read the session report

<S> read the

.red

2.3.2 Dateiextensionen, <N> save the

Reduktion

(, )

Reduktion Äquivalente Knoten

<M> Merging of

Reduktion abbrechen

5.1 Grundlagen

Reduktion Ausnahmen

<X> change eXceptions

Reduktion Elimination Laufplätze

<C> ELIMINATION of

Reduktion Elimination Schleifen

<U> DELETION of

Reduktion Knotennummern erhöhen

<R> Raise node

Reduktion Knotennummern verdichten

<S> Squeeze the

Reduktion Löschen PTP-Sequenzen

<W> DELETION of

Reduktion Menü

5.1 Grundlagen

Reduktion Netz ausgeben

<O> terminal Output

Reduktion Netz speichern

<N> save the

Reduktion Netz zurücksetzen

<I> reset to

Reduktion Parallele Knoten

<F> Fusion of

Reduktion Programm

<P> Program a

Reduktion Verschmelzen Vor- mit Nachplätzen

<V> DELETION of

Reduktion Verschmelzen Vor- mit Nachtransitionen

<A> ELIMINATION of , <B> ELIMINATION of

Reduktion Zusammenhangstest

<T> connectedness Test

Reinheit

PUR: Reinheit - pure

rename SESSION.ina

2.4.1 Aufruf und Beenden

.res

2.3.2 Dateiextensionen, Ablauf der Berechnung, <T> complete table, <I> Compute a , <O> open files

reset to the initial net

<I> reset to

reset to the initial state

<R> Reset to

resetable

REV: Reversibilität - reversible, Terminale starke Zusammenhangskomponenten und

results by other format

<I> Compute a

results incomplete

<F> Format lines

results of equations

<B> give results

returning heap

6.1 Grundlagen

REV

REV: Reversibilität - reversible, Terminale starke Zusammenhangskomponenten und

Reversibilität

REV: Reversibilität - reversible, Terminale starke Zusammenhangskomponenten und

reversible

REV: Reversibilität - reversible, Terminale starke Zusammenhangskomponenten und

safe and live

L&S: Lebendig und Sicher

safe firing rule

<S> safe firing

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

SC

SC: Starker Zusammenhang -

SCF

SCF: Statische Konfliktfreiheit -

Schaltdauer

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

Schalten

(, 4 Schalten, ), 5 Reduktion

Schalten Funktionen

4.4.1 Allgemeines

Schalten Hilfsfunktionen

4.3 Hilfsfunktionen

Schalten Menü

4.1 Grundlagen

Schalten unter Zeitbewertung

4.4.2 Schalten unter Zeitbewertung

Schaltliste

4.4.1 Allgemeines, Ergebnisanzeige

Schaltregel

2.5.3 Schaltregel

Schaltstrategie

2.5.5 Schaltstrategie

Schleifenfreiheit

PUR: Reinheit - pure

Schritt

<S> fire maximal , Zeitoption Dauer für Plätze , Zeitoption Intervalle für Bögen

Schritt Konflikte

Berechnung dynamischer Konflikte

Schritt Lebendigkeit

Lebendigkeitstest

Schritt Liste

Ergebnisanzeige

Schrittschaltregel

<S> fire maximal

Schwache Lebendigkeit

WL : Schwache Lebendigkeit , Lebendigkeitstest

second component

Gefärbte Netze

Selbstmodifizierendes Netz

<V> Valk's firing

sequential mode

<R> read vector

session output file

2.4.1 Aufruf und Beenden

Session-Report

2.4.2 Der Session-Report

Session-Report löschen

<D> delete the

Session-Report lesen

<S> read the

SESSION.ina

2.3.1 Wichtige Dateien, 2.4.1 Aufruf und Beenden , 2.5.6 Zeilenlänge

set remaining components to zero

<R> read vector

show all stubborn sets

<A> All minimal

show stubborn sets

<S> Show the

Sichere Schaltregel

<S> safe firing

Sicherheit

L&S: Lebendig und Sicher

single transitions

<T> fire single

skip lines

<F> Format lines

SM

SM: Zustandsmaschine - state , <C> Compute all

SMA

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

SMC

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

SMD

SMD: Zustandsmaschinendekomponierbarkeit - state , <D> Check the , <C> Compute all

space

Besondere Tasten und Zeichen, Editieren der Eingabe

Speicher freigeben

6.1 Grundlagen

Speichern von Daten

Speichern von Daten

Speichern von Kommandos

2.4.1 Aufruf und Beenden

squeeze the node numbers

<S> Squeeze the

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

Starten von INA Vorbereitungen

2.1 Startvorbereitungen

state machine

SM: Zustandsmaschine - state , <M> Decide state-machine

state machine allocatable

SMA: Zustandsmaschinenauswählbarkeit - state

state machine coverability

<M> Decide state-machine

state machine coverable

SMC: Zustandsmaschinenüberdeckbarkeit - state

state machine decomposable

SMD: Zustandsmaschinendekomponierbarkeit - state

states generated

<P> Compute a

STATES.gra

2.3.1 Wichtige Dateien, <G> Compute a , 6.4.4 Graphanalyse

static conflict free

SCF: Statische Konfliktfreiheit -

static conflicts

Voranalyse

Statische Konflikte

Voranalyse

Statische Konfliktfreiheit

SCF: Statische Konfliktfreiheit - , Voranalyse

step live

Lebendigkeitstest

steplist

Ergebnisanzeige, Schreiben der Schrittschaltliste

steps in conflict

Berechnung dynamischer Konflikte

stopped

5.1 Grundlagen

strongly connected

SC: Starker Zusammenhang -

structurally bounded

SB : Strukturelle Beschränktheit

Strukturanalyse

6.6 Strukturanalyse

Strukturelle Beschränktheit

SB : Strukturelle Beschränktheit

Strukturen

Strukturen, 6.6 Strukturanalyse

Sture Mengen

Sture Reduktion

Sture Mengen anzeigen

<S> Show the

subconservativ

CSV: Konservativität - conservativ

Subkonservativität

CSV: Konservativität - conservativ

supports

Ausgabeformate

Symmetrien Anfangszustand

<Y> Compute the

Symmetrien berechnen

<Y> Compute the

Symmetrien Fixpunkte

<Y> Compute the

symmetries

<Y> Compute the

Synchronisationsgraph

MG: Synchronisationsgraph - marked

Syntax .pnt-Datei

Syntax der .pnt-Datei

Syntax .cnt-Datei

Syntax der .cnt-Datei

Syntax Platzeingabe

Ungefärbte Netze

Syntax Transitionseingabe

<R> <N> Read

terminal

Umschaltung in den Terminalmodus

terminal SC-components

Terminale starke Zusammenhangskomponenten und

Terminalmodus

Umschaltung in den Terminalmodus

Test Überdeckbarkeit

Erreichbarkeits- bzw. Überdeckbarkeitstest, Erreichbarkeits-/Überdeckbarkeitstest

Test auf Zusammenhang

<T> connectedness Test

test connectedness

<T> <C> Test , <T> connectedness Test

Test Erreichbarkeit

Erreichbarkeits- bzw. Überdeckbarkeitstest, Erreichbarkeits-/Überdeckbarkeitstest

Test Lebendigkeit

Lebendigkeitstest

Test Lebendigkeit von Schritten

Lebendigkeitstest

test liveness of steps

Lebendigkeitstest

Test Nichterrreichbarkeit

Beispiel für eine Invarianteninterpretation

Test Rücksetzbarkeit

Terminale starke Zusammenhangskomponenten und

test vectors for invariant props

<T> Test place-

Test Zusammenhang

<T> <C> Test

tF0

tF0: Transition ohne Nachplatz

.tim

2.3.2 Dateiextensionen

time option

2.5.2 Zeitoption

timetick

Zeitoption Intervalle für Transitionen

.tmd

2.3.2 Dateiextensionen

token type

2.5.1 Markenarten

transient state

Zeitoption Dauer für Plätze

Transiente Zustände

Zeitoption Dauer für Plätze , Zeitoption Intervalle für Bögen , 6.4.1 Pfadberechnung

Transition ändern

<C> <U> Change , <C> <N> Change

Transition eft/lft

<I> intervals

Transition als Fakt kennzeichnen

Ungefärbte Netze

Transition ausgeben

<W> <T> Write

Transition bei Anfangsmarkierung tot

DTr: Tote Transition bei , Lebendigkeitstest

Transition Bewertung

Berechnung der Kreise

Transition eingeben

<R> <N> Read

Transition im Livelock

Berechnung der Kreise

Transition Invariante

6.5 Invariantenanalyse

Transition Invariante realisierbare

Berechnung der Kreise

Transition Name

Ungefärbte Netze

Transition Nummer

Ungefärbte Netze

Transition ohne Nachplatz

tF0: Transition ohne Nachplatz

Transition ohne Vorplatz

5.1 Grundlagen, Ft0: Transition ohne Vorplatz

Transition Schaltdauer

<D> durations

Transition tot

<D> Check the

transition without postplace

tF0: Transition ohne Nachplatz

transition without preplace

5.1 Grundlagen, Ft0: Transition ohne Vorplatz

Transitionsinvariantenüberdeckbarkeit

CTI: Transitionsinvariantenüberdeckbarkeit - covered , 6.5 Invariantenanalyse

.tre

2.3.2 Dateiextensionen, Baumdarstellung des Zustandsgraphen

Überblick

1.1 Überblick

Überdeckbarkeit mit Transitionsinvarianten

CPI: Platzinvariantenüberdeckbarkeit - covered , CTI: Transitionsinvariantenüberdeckbarkeit - covered , 6.5 Invariantenanalyse

Überdeckbarkeitsgraph Matrixdarstellung

Überdeckbarkeitsgrahen, Finkels Methode zur Berechnung , <G> Compute a , <G> Compute a , <A> Analyse the , Baumdarstellung des Zustandsgraphen, Matrixdarstellung des Zustandsgraphen

use symmetries

<S> Compute a

.val

2.3.2 Dateiextensionen, Berechnung der Kreise

Valk's firing rule

<V> Valk's firing

Verweildauer

<D> durations, Zeitoption Dauer für Plätze , Zeitoption Dauer für Plätze

Vielfachheit

Ungefärbte Netze

Vielfachheit ändern

<R> <A> Read , <C> <M> Change

Vielfachheit nichtblockierend

NBM: Nichtblockierende Vielfachheit -

Voranalyse

Voranalyse

weakly live

WL : Schwache Lebendigkeit , Lebendigkeitstest

WL

WL : Schwache Lebendigkeit , Lebendigkeitstest

write marking to file

<W> Write the

write the net to a file

<W> <F> Write

write the net to the terminal

<W> <T> Write

wrong file

Ablauf der Berechnung

Zeilenlänge

2.5.6 Zeilenlänge

Zeitbewertung

2.5.2 Zeitoption

Zeitbewertung Schalten

4.4.2 Schalten unter Zeitbewertung

Zeitbewertung Zustand

4.2.2 Zustandsdarstellung unter Zeitbewertung

Zeitoption

2.5.2 Zeitoption

zero

Gefärbte Netze

Zusammenhang

CON: Zusammenhang - connected

Zusammenhang starker

SC: Starker Zusammenhang -

Zusammenhang Test

<T> <C> Test , <T> connectedness Test

Zustandsdarstellung ohne Zeitbewertung

4.2.1 Zustandsdarstellung ohne Zeitbewertung

Zustandsdarstellung unter Zeitbewertung

4.2.2 Zustandsdarstellung unter Zeitbewertung

Zustandsgraph

<R> Compute a

Zustandsgraph Analyse

<A> Analyse the

Zustandsgraph Baumdarstellung

Baumdarstellung des Zustandsgraphen

Zustandsgraph Kreise

Berechnung der Kreise

Zustandsgraph Matrixdarstellung

Matrixdarstellung des Zustandsgraphen

Zustandsgraph stur reduziert

Sture Reduktion, <R> Compute a

Zustandsgraph symmetrisch reduziert

Symmetrische Reduktion, <R> Compute a

Zustandsmaschine

SM: Zustandsmaschine - state

Zustandsmaschine Überdeckbarkeit

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

Zustandsmaschine Auswählbarkeit

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

Zustandsmaschine Dekomponierbarkeit

SMD: Zustandsmaschinendekomponierbarkeit - state , <D> Check the