school.dve

input byte questions = 5, students = 2, threshold = 4;
channel cgrade;
channel answer;

process professor {
    byte requirements[questions], qid, sid, grade, ans;
    state idle,prepare,examine, ask;
    init idle;
    trans
        idle -> prepare {effect qid = 0;}
        prepare -> prepare { guard qid < questions; effect requirements[qid] = requirements[qid] + 1; }
        prepare -> prepare { guard qid < questions; effect qid = qid + 1; }
        prepare -> examine { guard qid == questions; effect qid = 0, sid = 0, grade = 0; }
        examine -> examine { guard qid < questions, sid < students; sync answer?ans; effect grade = grade + ( ans - requirements[ qid ] ), qid = qid + 1; }
        examine -> examine { guard qid == questions, sid < students; sync cgrade!grade; effect qid = 0, grade = 0; sid = sid + 1; }
        examine -> idle { guard qid == questions, sid == students; }
    ;
}

process student( key id, strategy, cheatFrom ) {
    byte learned[questions], qid, qval, grade;
    channel {byte,byte} cheatChan;
    state idle, study, answer, graded, passed;
    init idle;
        idle -> study { effect qid = 0;}
        study -> study { effect learned[qid] = learned[qid] + 1, qid = (qid + strategy) % questions; }
        study -> study { sync cheatChan!{qid, learned[qid]}; }
        study -> answer {}
        answer -> answer { guard id == professor->sid; sync answer!learned[ professor->qid ]; }
        answer -> answer { guard id != cheatFrom; sync student(cheatFrom)->cheatChan?{qid, qval}; effect learned[qid] = qval; }
        answer -> graded { sync cgrade?grade; }
        graded -> passed { guard grade >= threshold; }
        grade -> idle { guard grade < threshold; }
    ;
}

for( i: 0..students-1 ) {
    process student(i, i+1 (i + 2) % students);
}