Übung3 Aufgabe 7 - Label Variante

Benutzeravatar
Dennis
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 102
Registriert: 29. Sep 2008 21:15

Übung3 Aufgabe 7 - Label Variante

Beitrag von Dennis »

Ich muss irgendwo einen Fehler machen, aber die Musterlösung beendet sich bei mir mit Error: 1. Kann mir jemand auf die Sprünge helfen? :oops:

Code: Alles auswählen

spin -v
Spin Version 6.2.7 -- 2 March 2014

spin -a problem7_Label.pml

gcc -o pan pan.c

./pan -a
pan:1: assertion violated  !( !(( !((p._p==terminated))||(value==100)))) (at depth 24)
pan: wrote problem7_Label.pml.trail

(Spin Version 6.2.7 -- 2 March 2014)
Warning: Search not completed
        + Partial Order Reduction

Full statespace search for:
        never claim             + (valueRead)
        assertion violations    + (if within scope of claim)
        acceptance   cycles     + (fairness disabled)
        invalid end states      - (disabled by never claim)

State-vector 44 byte, depth reached 24, errors: 1
       13 states, stored
        0 states, matched
       13 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.001       equivalent memory usage for states (stored*(State-vector + overhead))
    0.289       actual memory usage for states
  128.000       memory used for hash table (-w24)
    0.534       memory used for DFS stack (-m10000)
  128.730       total actual memory usage



pan: elapsed time 0.01 seconds


./pan -a -f
error: p.o. reduction not compatible with fairness (-f) in models
       with rendezvous operations: recompile with -DNOREDUCE

pan: elapsed time 1.43e+07 seconds
pan: rate         0 states/second
...fragt stellvertretend für alle Freunde...

himbaer
Mausschubser
Mausschubser
Beiträge: 98
Registriert: 28. Apr 2010 19:29
Kontaktdaten:

Re: Übung3 Aufgabe 7 - Label Variante

Beitrag von himbaer »

In der Lösungsdatei steht ja auch folgender Satz:
It is possible that process p does not read at all from the channel.
This happens in any run where the "p"'s loop always chooses the first alternative.
Ich denke damit sollte klar sein, warum du deine LTL-Formel nicht beweisen kannst?!
meine Testsignatur :!:

Antworten

Zurück zu „Archiv“