Wie wird eine nicht initialisierte Variable in Spin erstellt?

Question

Es scheint, dass Promela jede Variable initialisiert (standardmäßig auf 0 oder auf den Wert, der in der Deklaration angegeben ist).

Wie kann ich eine Variable deklarieren, die durch einen unbekannten Wert initialisiert wird?

Die Dokumentation schlägt if :: p = 0 :: p = 1 fi aber ich glaube nicht, dass es funktioniert: Spin prüft noch diese Behauptung

bit p 
init { if :: p = 0 :: p = 1 fi } 
ltl { ! p } 

(und fälscht p)

Was genau die Semantik von init ist? Es gibt noch einige "Pre-Initial" Zustand? Wie kann ich das umgehen - und meine Studenten nicht verwirren?

Answer 1

Dies ist eine interessante Frage.

Die documentation besagt, dass jede Variable auf 0 initialisiert wird, sofern das Modell nichts anderes angibt.

Wie bei allen Variablendeklarationen ist ein explizites Initialisierungsfeld optional. Der Standardanfangswert für alle Variablen ist Null. Dies gilt sowohl für skalare Variablen als auch für Array-Variablen und gilt sowohl für globale als auch für lokale Variablen.

In Ihrem Modell Du initialisiere die Variable nicht, wenn man es erklären, deshalb wird es anschließend auf den Wert 0 zugeordnet im Anfangszustand, der vor Ihrem Auftrag befindet:

bit p 

init { 
    // THE INITIAL STATE IS HERE 
    if 
    :: p = 0 
    :: p = 1 
    fi 
} 

ltl { ! p } 

---

Einige Experimente.

A „naive“ Idee, diese Einschränkung für Ausweichen zu ändern wäre, die c Quellcode von pan.c, die durch Spin erzeugt wird, wenn Sie ~$ spin -a test.pml aufrufen, so dass die Variable zufällig initialisiert .

Anstelle dieser Initialisierungsfunktion:

void 
iniglobals(int calling_pid) 
{ 
     now.p = 0; 
#ifdef VAR_RANGES 
     logval("p", now.p); 
#endif 
} 

man versuchen, dies zu schreiben kann:

void 
iniglobals(int calling_pid) 
{ 
     srand(time(NULL)); 
     now.p = rand() % 2; 
#ifdef VAR_RANGES 
     logval("p", now.p); 
#endif 
} 

und das Hinzufügen ein #include <time.h> im Kopfteil.

Sobald Sie jedoch, dass in einem Verifizierer mit gcc pan.c kompilieren, und Sie versuchen, es zu laufen, Sie nicht-deterministisches Verhalten in Abhängigkeit von der Initialisierung Wert der Variablen p erhalten.

Es kann sowohl bestimmen, dass das Eigentum verletzt wird:

~$ ./a.out -a 
pan:1: assertion violated !(!(!(p))) (at depth 0) 
pan: wrote test.pml.trail 

(Spin Version 6.4.3 -- 16 December 2014) 
Warning: Search not completed 
    + Partial Order Reduction 

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

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

Stats on memory usage (in Megabytes): 
    0.000 equivalent memory usage for states (stored*(State-vector + overhead)) 
    0.291 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 seconds 

oder drucken, dass die Eigenschaft erfüllt ist:

~$ ./a.out -a 
(Spin Version 6.4.3 -- 16 December 2014) 
    + Partial Order Reduction 

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

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

Stats on memory usage (in Megabytes): 
    0.000 equivalent memory usage for states (stored*(State-vector + overhead)) 
    0.291 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 


unreached in init 
    test.pml:8, state 5, "-end-" 
    (1 of 5 states) 
unreached in claim ltl_0 
    _spin_nvr.tmp:8, state 8, "-end-" 
    (1 of 8 states) 

pan: elapsed time 0 seconds 

klar, dass die Anfangszustand eines Modells Promela verifiziert von Spin wird angenommen, dass sie einzigartig sind. Afterall, das ist eine vernünftige Annahme, da es unnötig Dinge komplizieren würde: Sie können immer N ersetzen verschiedene Anfangszustände S_i mit einem Anfangszustand S S. T. S erlaubt es, jedes S_i mit einem Epsilon-Übergang zu erreichen. In diesem Zusammenhang ist das, was Sie bekommen, nicht wirklich ein Epsilon-Übergang, aber in der Praxis macht es wenig Unterschied.

EDIT(aus den Kommentaren): Grundsätzlich ist es möglich, diese Arbeit zu machen, indem pan.c ein wenig modifiziert weiter:

• verwandeln den Anfangszustand initialiser in einen Generator der Anfangszustände
• ändern Sie die Verifikationsroutine zu berücksichtigen, dass m ehr als ein Anfangszustand existieren könnte, und dass die Eigenschaft muss für jeden Anfangszustand

Having said diese halten, ist es wahrscheinlich nicht der Mühe wert, es sei denn, dies durch das Patchen Spin erfolgt ‚s-Quellcode.

---

Problemumgehung.

Wenn Sie angeben möchten, dass etwas im Ausgangszustand wahr ist, oder von dem Anfangszustand ausgehend, und berücksichtigen einige nicht-deterministisches Verhalten, dann sollten Sie etwas schreiben wie folgt:

bit p 
bool init_state = false 

init { 
    if 
    :: p = 0 
    :: p = 1 
    fi 
    init_state = true // TARGET STATE 
    init_state = false 
} 

ltl { init_state & ! p } 

, mit dem Sie erhalten:

~$ ./a.out -a 

pan:1: assertion violated !(!((initialised& !(p)))) (at depth 0) 
pan: wrote 2.pml.trail 

(Spin Version 6.4.3 -- 16 December 2014) 
Warning: Search not completed 
    + Partial Order Reduction 

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

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

Stats on memory usage (in Megabytes): 
    0.000 equivalent memory usage for states (stored*(State-vector + overhead)) 
    0.291 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 seconds 

---

Init Semantics.

Init wird einfach garantiert die erste Prozess sein zum Laichen und soll zum Laichen andere Prozesse verwendet werden, wenn zum-Beispiel nehmen die anderen Routinen als Eingangs einige Parameter, z.B Einige Ressourcen werden geteilt. Weitere Informationen here.

Ich glaube, dass dieses Fragment von documentation ist ein wenig irreführend:

Der init-Prozess wird am häufigsten verwendet, um global s Variable initialisieren, und anderen Prozessen zu instanziieren, durch die Verwendung des Laufes Operator, bevor die Systemausführung beginnt. Jeder Prozess, nicht nur die Init-Prozess, kann dies tun, obwohl

Da es Garantie möglich ist, dass der init-Prozess alle ihren Code vor jedem anderen Prozess ausführt mit der atomic { } Aussage, man könnte sagen, dass es verwendet werden kann, um Variablen zu initialisieren, bevor sie von anderen Prozessen aus dem Programmierpunkt verwendet werden. Aber das ist nur eine grobe Approximation, weil der Init-Prozess nicht einem eindeutigen Zustand im Ausführungsmodell entspricht, sondern eher der Baum der Staaten an der Wurzel und der Stamm selbst ist nur durch die globale Umgebung gegeben wie es ist, bevor ein Prozess beginnt.