Wozu PROMELA when man auf plain C schreiben kann?

[klte]

Hi Leute!

Die drei Zeilen in PROMELA-Sprache sagen viel aus:

c_code {
\#include "someheaders.h"
\#include "someCcode.c"
};

[yourmaninamsterdam]

Man kann das schon machen, aber C-Code wird vom Verifier als korrekt angenommen. Da es hier nicht im Kern um Programmierung, sondern um Modellierung und Verifikation geht, hast du nichts davon, dass Promela embedded C unterstützt. Promela selbst hat andere Kerneigenschaften als C, z. B. Nichtdeterminismus der Ausführung.