University (CCS)

Here are some ways to fix it:

• Set the communication models to:

  causal,,studentname,resit,examreq,cancel,mark
  fifo11,,materials,exam
  async,,ok,ko,answers,coffee
  

• Add the analyzed_by_pf,,studentname,resit,examreq,cancel,mark,materials,exam,ok,ko,answers,coffee communication model, then attempt to infer the correct channel priorities.

Communication Model(s):

async,,studentname,resit,examreq,cancel,mark async,,materials,exam async,,ok,ko,answers,coffee

XPeer (CCS):

* initialstate Student agent Student = resit.(tau.'ko.0+tau.StudentOK); agent StudentOK = 'ok.'examreq.materials.exam.'answers.0;

XPeer (CCS):

* initialstate Supervisor agent Supervisor = 'studentname.'studentname.'resit.((ok.0+ko.'cancel.'mark.0)|(coffee.0));

XPeer (CCS):

* initialstate Secretary agent Secretary = 'coffee.studentname.mark.0;

XPeer (CCS):

* initialstate Teacher agent Teacher = studentname.(cancel.0+examreq.TeacherExam); agent TeacherExam = 'materials.'exam.answers.'mark.0;

Add CCS peerAdd LTS peer

Properties:

• All peers terminate.
• The network ends up empty.
• No peer goes into a forbidden state.
• No (global) deadlocks

Test properties Infer all constraint sets (pessimistic) Infer one constraint set (pessimistic) Infer some constraint sets (optimistic) Infer one constraint set (optimistic) Infer all constraint sets (pessimistic, listened) Infer one constraint set (pessimistic, listened) Infer some constraint sets (optimistic, listened) Infer one constraint set (optimistic, listened)