Inhalt

• Abbildungsverzeichnis
• 1 Einleitung
  • 1.1 Überblick
  • 1.2 Darstellungsweise
    • <Taste> Beispielkommando
    • Besondere Tasten und Zeichen
    • Weitere Darstellungsweisen
• 2 Grundlagen
  • 2.1 Startvorbereitungen
    • Installation unter DOS
    • Installation unter UNIX
  • 2.2 Generelle Regeln für den Dialog mit INA
    • Beantwortung von Abfragen
    • Dateianforderungen
    • Editieren der Eingabe
    • Eingabe von Namen
    • Umschaltung in den Terminalmodus
    • Speichern von Daten
  • 2.3 Dateien, Extensionen, Formate und die Netzeingabe
    • 2.3.1 Wichtige Dateien
    • 2.3.2 Dateiextensionen
    • 2.3.3 Eingabe von Netzen
      • Ungefärbte Netze
      • Gefärbte Netze
    • 2.3.4 Dateiformate
      • Syntax der .pnt-Datei
      • Beispiel für eine .pnt-Datei
      • Syntax der .cnt-Datei
      • Beispiel für eine .cnt-Datei
  • 2.4 Die Struktur einer INA -Session
    • 2.4.1 Aufruf und Beenden von INA
    • 2.4.2 Der Session-Report
      • <S> read the session report
      • <D> delete the session report
    • 2.4.3 Analyse mehrerer Netze nach dem gleichen Schema
  • 2.5 Optionen
    • 2.5.1 Markenarten
      • <B> black (indistinguishable) tokens
      • <C> coloured tokens
    • 2.5.2 Zeitoption
      • <N> no times
      • <D> durations
      • <I> intervals
    • 2.5.3 Schaltregel
      • <N> normal firing rule
      • <C> normal firing rule with capacities
      • <S> safe firing rule
      • <V> Valk's firing rule
    • 2.5.4 Prioritäten
    • 2.5.5 Schaltstrategie
      • <T> fire single transitions
      • <S> fire maximal steps
    • 2.5.6 Zeilenlänge
• 3 Editor
  • <Q> Quit the editing process
  • 3.1 Einlesen und Schreiben
    • <R> <F> Read a net from a File
    • <R> <T> Read a net from the Terminal
    • <R> <N> Read a Node from the terminal
    • <R> <A> Read an Arc from the terminal
    • <W> <F> Write the net to a File
    • <W> <T> Write the net to the Terminal
  • 3.2 Löschen und Ändern
    • <D> <T> Delete the net Totally
    • <D> <N> Delete a Node
    • <D> <C> Delete a Colour
    • <D> <I> Delete all Isolated nodes/colours
    • <D> <A> Delete all input- or output-Arcs
    • <C> <F> Change Facts
    • <C> <P> Change Priorities
    • <C> <C> Change Capacities
    • <C> <I> Change Initial times
    • <C> <U> Change nUmbers
    • <C> <N> Change Names
    • <C> <M> Change Multiplicities
    • <C> <T> Change the Token load (marking)
  • 3.3 Verschmelzen
    • <N> <D> Node Doubling
    • <M> <O> Merge two nOdes
    • <M> <N> Merge two Nets
    • <T> <C> Test Connectedness
• 4 Schalten
  • 4.1 Grundlagen
  • 4.2 Zustandsdarstellung
    • 4.2.1 Zustandsdarstellung ohne Zeitbewertung
    • 4.2.2 Zustandsdarstellung unter Zeitbewertung
      • Zeitoption Dauer für Plätze - Verweildauer
      • Zeitoption Dauer für Transitionen - Schaltdauer
      • Zeitoption Intervalle für Transitionen - eft/lft
      • Zeitoption Intervalle für Bögen - Durchlaßfenster
  • 4.3 Hilfsfunktionen
    • <Q> Quit
    • <W> Write the actual marking to a file
    • <S> Show the stubborn set used by the stubborn red. reachab. graph
    • <A> All minimal stubborn sets to be shown
  • 4.4 Schaltfunktionen
    • 4.4.1 Allgemeines
      • <cr> fire the first element
      • <B> Back to the previous state
      • <R> Reset to the initial state
    • 4.4.2 Schalten unter Zeitbewertung
      • Zeitoption Dauer für Plätze - Verweildauer
      • Zeitoption Dauer für Transitionen - Schaltdauer
      • Zeitoption Intervalle für Transitionen - eft/lft
      • Zeitoption Intervalle für Bögen - Durchlaßfenster
  • 4.5 Beispiel
• 5 Reduktion
  • 5.1 Grundlagen
  • 5.2 Hilfsfunktionen
    • <P> Program a sequence of reduction steps
    • <X> change eXceptions
    • <T> connectedness Test
    • <N> save the actual net
    • <R> Raise node numbers with exceptions
    • <O> terminal Output of the current net
    • <I> reset to the Initial net
    • <S> Squeeze the node numbers
  • 5.3 Reduktionsprozeduren
    • <F> Fusion of congruent nodes
    • <M> Merging of equivalent places
    • <A> ELIMINATION of -places
    • <B> ELIMINATION of -places
    • <C> ELIMINATION of looping places
    • <U> DELETION of looping transitions
    • <V> DELETION of single output transitions
    • <W> DELETION of PTP-sequences
• 6 Analyse
  • 6.1 Grundlagen
  • 6.2 Analysestatus
    • 6.2.1 Elementare Netzeigenschaften
      • ORD: Gewöhnlichkeit - ordinary
      • HOM: Homogenität - homogenous
      • NBM: Nichtblockierende Vielfachheit - nonblocking multiplicity
      • PUR: Reinheit - pure
      • CSV: Konservativität - conservativ
      • SCF: Statische Konfliktfreiheit - static conflict free
      • CON: Zusammenhang - connected
      • SC: Starker Zusammenhang - strongly connected
      • Einseitige Knoten
      • Ft0: Transition ohne Vorplatz - transition without preplace
      • tF0: Transition ohne Nachplatz - transition without postplace
      • Fp0: Platz ohne Vortransition - place without pretransition
      • pF0: Platz ohne Nachtransition - place without posttransition
      • Strukturen
      • MG: Synchronisationsgraph - marked graph
      • SM: Zustandsmaschine - state machine
      • FC: Free-Choice-Netz - free choice
      • EFC: Extended-Free-Choice-Netz - extended free choice
      • ES: Extended-Simple-Netz - extended simple
    • 6.2.2 Weitere Netzeigenschaften
      • DTP: Deadlock-Falle-Eigenschaft - deadlock-trap-property
      • SMC: Zustandsmaschinenüberdeckbarkeit - state machine coverable
      • SMD: Zustandsmaschinendekomponierbarkeit - state machine decomposable
      • SMA: Zustandsmaschinenauswählbarkeit - state machine allocatable
      • CPI: Platzinvariantenüberdeckbarkeit - covered by place invariants
      • CTI: Transitionsinvariantenüberdeckbarkeit - covered by transition invariants
      • B : Beschränktheit - bounded
      • SB : Strukturelle Beschränktheit - structurally bounded
      • REV: Reversibilität - reversible
      • DSt: Erreichbarkeit eines toten Zustandes - dead state reachable
      • BSt: Fakt hat Konzession - bad state reachable
      • DTr: Tote Transition bei Anfangsmarkierung - dead transition at initial marking
      • DCF: Dynamische Konfliktfreiheit - dynamically conflictfree
      • L : Lebendigkeit - live
      • LV : Lebendigkeit (unter Ignorierung toter Trans.) - live if dead trans. ign.
      • L&S: Lebendig und Sicher - live and safe
      • Lebendigkeit für gefärbte Netze
      • WL : Schwache Lebendigkeit - weakly live
      • CL : Kollektive Lebendigkeit - collectively live
  • 6.3 Analysemenü und Voranalyse
    • Voranalyse
    • Beispiel
  • 6.4 Erreichbarkeitsanalyse
    • 6.4.1 Pfadberechnung
      • <P> Compute a shortest path from the initial state to a target marking
      • Ergebnisanzeige
    • 6.4.2 Reduktionen des Zustandsgraphen
      • Symmetrische Reduktion
      • <Y> Compute the symmetries of the net
      • Sture Reduktion
      • Überdeckbarkeitsgrahen
      • Finkels Methode zur Berechnung des minimalen Überdeckbarkeitsgraphen
    • 6.4.3 Graphberechnung
      • <R> Compute a reachability graph
      • <G> Compute a coverability graph
      • Optionen
      • Berechnungsarten
      • Tiefenbeschränkung
      • Schreiboptionen
      • Erreichbarkeits- bzw. Überdeckbarkeitstest
      • Ablauf der Berechnung
      • Ergebnisanzeige
      • Erreichbarkeits-/Überdeckbarkeitstest
    • 6.4.4 Graphanalyse
      • <A> Analyse the previously computed graph
      • Ablauf der Berechnung
      • Optionen
      • Einfache Schreiboptionen
      • Baumdarstellung des Zustandsgraphen
      • Schreiben der Schrittschaltliste
      • Matrixdarstellung des Zustandsgraphen
      • Berechnung dynamischer Konflikte
      • Berechnung der Distanzen
      • Berechnung der Kreise
      • Terminale starke Zusammenhangskomponenten und Rücksetztbarkeit
      • Lebendigkeitstest
  • 6.5 Invariantenanalyse
    • 6.5.1 Invariantenberechnung
      • Inzidenzmatrix
      • Ausgabeformate
      • <T> complete table
      • <Z> complete table, zero's not printed
      • <E> print non-zero entries only
      • <#> print non-zero entries with names
      • Basisberechnung
      • <I> Compute a base for all S/T-invariants
      • Beispiel für eine Invarianteninterpretation
      • Schneller Nichterreichbarkeitstest
    • 6.5.2 Semipositive Invarianten
      • Semipositive (Sub/Sur)-Invarianten
      • Bemerkungen zur Komplexität
      • Interaktive Berechnung
      • Ausgabeformate
      • <S> print supports
      • <N> print supports with names
      • Basisberechnung semipositiver (Sub/Sur)-Invarianten
      • <S> Compute a base for all semipositive S/T-[sub/sur]-invariants
      • Formatierung von Invarianten
      • <F> Format lines written to INVARI.hlp earlier
    • 6.5.3 Invariantentest
      • <T> Test place- or transition-vectors for invariant properties
      • Dateien öffnen
      • <O> open files (input and output)
      • <O> <1> open input file only
      • <O> <2> open output file only
      • <O> <3> open input file with restricted consistency test
      • <O> <4> open input file without consistency test
      • Dateien schließen
      • <C> close files (input and output)
      • <C> <1> close input file only
      • <C> <2> close output file only
      • Leseoperationen
      • <R> read vector
      • <R> <1> read vector without terminal protocol
      • Schreiboperationen
      • <W> write vector
      • <K> write headlines for vector
      • <F> change output format
      • Testfunktionen
      • <P> give properties of the vector
      • <B> give results of equations
      • <B> <1> give equations with non-zero results
      • <Q> show equations
      • <Q> <1> show single equation
      • Weitere Funktionen
      • <M> show (transposed) incidence matrix
      • <S> repeat function sequence
      • <H> help
      • <E> exit
  • 6.6 Strukturanalyse
    • <D> Check the deadlock-trap-, SMD-, SMA-properties
    • <C> Compute all components
    • <M> Decide state-machine coverability
• Literatur
• Index
• Über dieses Handbuch