Keine Gleichverteilung bei select?

barracuda317
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 187
Registriert: 12. Okt 2011 18:15

Keine Gleichverteilung bei select?

Beitrag von barracuda317 »

Hallo,

gerade habe ich das Beispielprogramm von Folie 23 für select (Introduction Promela) ausprobiert?

Die erhaltenen Werte machen mich jedoch etwas stutzig. Bei meinen Aufrufen (etwa 100) kam sehr oft 0, 1 und gelegentlich 2,3,4). Höhere Werte waren garnicht anzutreffen.

Sollte select nicht eigentlich eine kürzere Schreibweise für die do-Schleife auf Folie 22 sein und eine nicht-deterministische und gleichverteilte Auswahl aus der Menge bieten?

Das wir keinen perfekten gleichverteilten Nichtdeterminismus hinbekommen, ist mir klar. Aber diese Auswahl erscheint mir schon arg ungleich.

Benutzeravatar
mmi1991
Computerversteher
Computerversteher
Beiträge: 349
Registriert: 20. Okt 2011 18:46
Wohnort: Hattersheim

Re: Keine Gleichverteilung bei select?

Beitrag von mmi1991 »

Hi,
leider hast du völlig recht - eine Gleichverteilung hat aber auch niemand gefordert bei select…

Siehe auch
http://spinroot.com/spin/Man/select.html

Es wird also wirklich einfach nur diese Umwandlung durchgeführt.

Der Vollständigkeit halber sei auch hier erwähnt: Für die Verifikation ist die Verteilung egal.

EDIT:
ich habe mal ein Beispiel aufgesetzt, das eine Gleichverteilung generiert. Ist allerdings ziemlich hässlich. Zur Verifikation NICHT zu empfehlen :D

Code: Alles auswählen

inline rand(r, max)
{
	{
	bit n[max];
	int lastFound;
	int i;
	for (i: 1 .. max) {
		n[i - 1] = 0;
	}
	do
		:: true ->
			lastFound = -1;
			for (i: 1 .. max) {
				if
					:: (n[i - 1] == 1) ->
						if
							:: (lastFound == -1) ->
								lastFound = i - 1;
							:: else ->
								goto afterSeek;
						fi
					:: else -> true;
				fi
			};
			if
				:: (lastFound != -1) ->
					goto Ex;
				:: else -> true;
			fi;
	afterSeek:
			for (i: 1 .. max) {
				n[i - 1] = 0;
			}
			
			for (i: 1 .. max) {
				if
				:: true -> n[i - 1] = 1;
				:: true -> n[i - 1] = 0;
				fi
			}
	od;
Ex:
	r = lastFound;
	}
}

active proctype test() {
	int dice, c;
	int counts[6];
	for (c: 1 .. 10000) {
		rand(dice, 6);
		counts[dice]++;
		dice++;
	}
	for (c: 1 .. 6) {
		printf("Wuerfelzahl %d wurde %d mal gewuerfelt\n", c, counts[c - 1]);
	}
}

Code: Alles auswählen

spin randomSelect.pml 
      Wuerfelzahl 1 wurde 1670 mal gewuerfelt
      Wuerfelzahl 2 wurde 1664 mal gewuerfelt
      Wuerfelzahl 3 wurde 1658 mal gewuerfelt
      Wuerfelzahl 4 wurde 1577 mal gewuerfelt
      Wuerfelzahl 5 wurde 1745 mal gewuerfelt
      Wuerfelzahl 6 wurde 1686 mal gewuerfelt
1 process created
Bei 1.000.000 Würfen

Code: Alles auswählen

      Wuerfelzahl 1 wurde 167160 mal gewuerfelt
      Wuerfelzahl 2 wurde 166665 mal gewuerfelt
      Wuerfelzahl 3 wurde 166463 mal gewuerfelt
      Wuerfelzahl 4 wurde 166661 mal gewuerfelt
      Wuerfelzahl 5 wurde 166708 mal gewuerfelt
      Wuerfelzahl 6 wurde 166343 mal gewuerfelt
1 process created

real	2m19.009s
user	2m18.809s
sys	0m0.012s
Im Prinzip erzeuge ich nur ein großes Array, das so groß ist wie der Zufallszahlenraum. Ich setze so lange zufällig die Arraywerte zwischen 0 und 1, bis zufällig genau eines = 1 ist. Das nehme ich dann.
Nat. bei viel größeren Arrays deutlich inperformanter.

Viele Grüße
Ophasentutor SoSe 2014, WiSe 2015/16
Alle Angaben wie immer ohne Gewähr

verklixt1
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 156
Registriert: 29. Dez 2007 20:22

Re: Keine Gleichverteilung bei select?

Beitrag von verklixt1 »

Wollte schon die selbe Frage stellen.

Wichtig wäre jetzt nur noch zu wissen ob select, obwohl diese nicht richtig funktioniert in der Klausur als nicht-deterministischer Zufallsgenerator angenommen werden darf!?

yourmaninamsterdam
Nerd
Nerd
Beiträge: 681
Registriert: 26. Okt 2006 14:04
Kontaktdaten:

Re: Keine Gleichverteilung bei select?

Beitrag von yourmaninamsterdam »

verklixt1 hat geschrieben:Wichtig wäre jetzt nur noch zu wissen ob select, obwohl diese nicht richtig funktioniert in der Klausur als nicht-deterministischer Zufallsgenerator angenommen werden darf!?
Wer hat denn gesagt, dass select nicht funktioniert? Es erzeugt lediglich keine Gleichverteilung. Für die Verifikation des Modells ist das aber, wie mmi1991 schon angemerkt hat, völlig unerheblich.

Antworten

Zurück zu „Archiv“