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 Teacher agent Teacher = studentname.(cancel.0+examreq.TeacherExam); agent TeacherExam = 'materials.'exam.answers.'mark.0;

XPeer (CCS):

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

XPeer (CCS):

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

XPeer (CCS):

* initialstate Student agent Student = resit.(tau.'ko.0+tau.StudentOK); agent StudentOK = 'ok.'examreq.materials.exam.'answers.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)