Now there are two options for customer, phone call and sms to clinic to book an appointment with doctor. The phone call or sms need to deliver to phone attender or reception, then do the next.... Well as we know, the phone call and sms can successful deliver or fail deliver, the solution of fail deliver will continue to try again the same way of user select or another one.
Based on the above background, I write some codes for doing model checking behavior to implement it. I am quite new of the class, anyone can help to find the anything wrong with my codes.
MODULE call
VAR
option:{call,sms};
call:{successful,fail,again};
sms:{successful,fail,again};
phone_attender:{available,unavailable};
ASSIGN
init(option):=call|sms;
next(call):=case
call=successful:successful;
call=successful&phone_attender=available:{successful,available};
call=fail&phone_attender=fail:{fail,unavailable};
call=fail&phone_attender=fail:{again,unavailable};
call=again&phone_attender=successful:{again,available};
1:{successful,fail,again};
esac;
next(sms):=case
sms=successful&phone_attender:successful{successful};
sms=fail&phone_attender=fail:{fail,unavailable};
sms=fail&phone_attender=fail:{again,unavailable};
sms=again&phone_attender=successful:{again,available};
1:{successful,fail,again};
next(phone_attender):=case
phone_attender=available(call=successful|call=again)&(sms=successful|sms=again);
phone_attender=unavailable(call=fail|call=again)&(sms=fail|sms=again);
1:phone_attender;
esac;
It always remainder me syntax errors and run in the terminal with nuXmv.
Line 20:
file test.smv: line 20: at token "{": syntax error
The problem is given by the following condition:
sms=successful&phone_attender:successful{successful};
The value successful{successful} doesn't make any sense, choose between successful or {succesful}. Both are interpreted in the same way.
Line 26:
file test.smv: line 26: at token ":=": syntax error
You did not close the case construct of the previous assignment. Add esac; after the last condition.
Lines 28/29:
file test.smv: line 28: at token ";": syntax error
file test.smv: line 29: at token ";": syntax error
You did not provide the next value for phone_attender for the first two cases.
Note: I did not check the semantics of your model, since it is not even syntactically correct.