Umwandlung eines Systemmodells in ein Übergangssystem zur Modellprüfung

Question

Momentan versuche ich, einen Systemprototyp in das Übergangssystemmodell zu konvertieren. Ich habe einige LTL-Eigenschaften und ich möchte diese Eigenschaften mit Model-Check-Tool NuSMV überprüfen. Ich habe gerade Informationen, wie man Modellierung beginnt, indem man atomoische Eigenschaften und andere mathematische Aspekte definiert.

Pictorial Representation of Model

Answer 1

Eine sehr einfache Codierung in NuSMV dieses Übergangssystem würde

MODULE main() 
VAR 
    state : { GETINFO, ACK, SEND }; 
ASSIGN 
    init(state) := GETINFO; 
    next(state) := case 
    state = GETINFO : SEND; 
    state = SEND : ACK; 
    state = ACK  : {GETINFO, SEND}; 
    esac; 

Wie dem auch sei, ich denke, dass das Modell Sie ein bisschen zu einfach versehen ist, mit Ihrer übereinstimmen Problembeschreibung, so lade ich Sie ein, zusätzliche Informationen zu geben, was Sie vorhaben zu tun.