/* * * FSP model of the Jobshop originally formulated in CCS. * (c) Wolfgang Schreiner, 2009 * * */ // gives error, don't know why // SEM = (get->put->SEM). // HAMMER = SEM/{geth/get, puth/put}. // MALLET = SEM/{getm/get, putm/put}. // the tools HAMMER = (geth->puth->HAMMER). MALLET = (getm->putm->MALLET). // job characteristics const EASY = 0 const NORMAL = 1 const HARD = 2 const DONE = 3 range JOB = EASY..HARD // in contrast to CCS, every reference to a process identifier // must be prefixed by an action, thus the model becomes a bit more complex JOBBER = ( in[job: JOB] -> if job == EASY then (out[job+DONE] -> JOBBER) else if job == HARD then (geth -> UHAMMER[job]) else (geth -> UHAMMER[job] | getm -> UMALLET[job]) ), UHAMMER[job: JOB] = (puth -> FINISH[job]), UMALLET[job: JOB] = (putm -> FINISH[job]), FINISH[job: JOB] = (out[job+DONE]->JOBBER). // number of jobbers const N = 2 // progress is made if some output occurs progress INOUT = { j[i:1..N].out[EASY+DONE], j[i:1..N].out[NORMAL+DONE], j[i:1..N].out[HARD+DONE] } // a jobber that copes without tools can simulate a jobber with tools property STRONGJOBBER = (in[job: JOB] -> out[job+DONE] -> STRONGJOBBER). ||JOBSHOP = ( forall[i:1..N] j[i]:JOBBER || {j[i:1..N]}::HAMMER || {j[i:1..N]}::MALLET // conjoining N STRONGJOBBERs passes the safety check (i.e. leaves the model unchanged) // || forall[i:1..N] j[i]:STRONGJOBBER )\{j[1..N].geth, j[1..N].puth, j[1..N].getm, j[1..N].putm}. // FLTL property checking fluent WORK[i:1..N][job:JOB] = < { j[i].in[job] }, { j[i].out[job+DONE] } > assert WORKING = forall[i:1..N] []<> exists[job:JOB] WORK[i][job] menu MENU = { j[1..N].in[JOB], j[1..N].out[JOB] }