Deklarationen in atomic-Blöcken

[null]

Hallo zusammen,

könnte mir jemand erklären, warum ich Deklarationen von Variablen nicht in atomic-Blöcke schreiben darf?

Vielen Dank

[yourmaninamsterdam]

Das hat nicht unbedingt was mit atomic-Blöcken zu tun, sondern damit, dass Promela Deklarationen immer an den Beginn der Prozesse schiebt. Meines Erachtens lohnt es sich nicht wirklich, sich zu fragen, warum oder ob das toll ist, sondern man muss einfach damit leben.

[null]

Aber es gibt ja konkrete Unterschiede. Schau dir mal diesen Code an:

Code: Alles auswählen

byte b = 0;

proctype P(){
	atomic{
		byte tmp = b;		//Ohne den atomic-Block käme es zu Verschränkungen
		tmp++;
		b = tmp;
	}
}


init {
	run P();
	run P();
	(_nr_pr == 1) -> assert (b ==2 );
}

Hier ist das assert nicht true, obwohl die die Anweisungen in einem atomic-Block stehen. Damit die Aussage in assert wahr wird, muss ich folgendes schreiben:

Code: Alles auswählen

byte tmp = 0;
atomic {
            tmp = b;
//...

Warum gibt es diesen doch sehr großen Unterschied?
Danke!

[yourmaninamsterdam]

Das ändert ja nichts daran, dass es genaugenommen unzulässig ist, Deklarationen von Variablen nicht zu Beginn des Prozesses zu machen. Ich halte es zwar für eine schlechte Idee, das so zu handhaben, wie Promela das macht, nämlich über die Unzulässigkeit zu schweigen und irgendwelche Anweisungen zu verschieben, aber das tut ja für den konkreten Fall nichts zur Sache. Wenn du in deinem Beispiel die Deklaration 'byte tmp = b;' gedanklich an den Anfang des Prozesses verschiebst (was ja beim Ausführen auf die ein oder andere Weise geschieht), dann siehst du auch, warum das assert am Ende nicht unbedingt stimmt.

Die Essenz hier muss einfach sein: Richtig programmieren, also Deklarationen immer am Anfang, dann klappt es auch mit den asserts.