***(% \subsection{Auxiliary modules} We start presenting some auxiliary modules. These are auxiliary modules defining sorts \verb+Paper+ and \verb+Name+, and several constants of each one. \small \begin{verbatim} %) (fmod PAPER is sort Paper . ops p1 p2 p3 p4 p5 : -> Paper . op final-version : Paper -> Paper . op rejected : Paper -> Paper . endfm) (view Paper from TRIV to PAPER is sort Elt to Paper . endv) (fmod NAME is sort Name . ops author1 author2 author3 author4 conf-chair program-chair pc-member1 pc-member2 reviewer1 reviewer2 reviewer3 : -> Name . endfm) (view Name from TRIV to NAME is sort Elt to Name . endv) ***(% \end{verbatim} \normalsize The following module defines an operation \texttt{broadcast} used to send the same message content to a set of the mobile objects . \small \begin{verbatim} %) (mod BROADCAST is pr MOBILE-OBJECT-ADDITIONAL-DEFS . pr SET[Mid] * (op __ : Set[Mid] Set[Mid] -> Set[Mid] to _._) . op broadcast : Set[Mid] Contents -> MsgSet . var O : Mid . var OS : Set[Mid] . var MC : Contents . eq broadcast((O . OS), MC) = (to O : MC) broadcast(OS, MC) . eq broadcast(mt, MC) = none . endm) ***(% \end{verbatim} \normalsize Module \texttt{CHOOSE-REVIEWERS} defines the \texttt{choose} operation, that nondeterministically chooses a given number of mobile object identifiers from a given set. \small \begin{verbatim} %) (mod CHOOSE-REVIEWERS is pr MOBILE-OBJECT-ADDITIONAL-DEFS . pr SET[Mid] * (op __ : Set[Mid] Set[Mid] -> Set[Mid] to _._) . op choose : Set[Mid] MachineInt -> Set[Mid] . var O : Mid . var OS : Set[Mid] . var I : MachineInt . rl [choose-reviewers] : choose(OS, 0) => mt . crl [choose-reviewers] : choose(O . OS, I) => O . choose(OS, _-_(I, 1)) if I > 0 . endm) ***(% \end{verbatim} \normalsize We assume that a reviewer can only accept or reject the paper. In the current version there are no more possibilities and no comments. \small \begin{verbatim} %) (fmod SCORE is sort Score . ops accept reject : -> Score . op opp : Score -> Score . eq opp(accept) = reject . eq opp(reject) = accept . endfm) (view Score from TRIV to SCORE is sort Elt to Score . endv) ***(% \end{verbatim} \normalsize %) *** list.fm *** august 23, 2000 (fmod LIST[X :: TRIV] is sort List[X] . subsort Elt.X < List[X] . op nil : -> List[X] . op __ : List[X] List[X] -> List[X] [assoc id: nil] . endfm) ***(% \subsection{Review Forms} These are the messages interchanged between a review form and a reviewer: \small \begin{verbatim} %) (omod REVIEW-FORM-REVIEWER-MSGS is inc MOBILE-OBJECT-ADDITIONAL-DEFS . pr PAPER . pr SCORE . pr (LIST * (op nil to no-id, op __ to _&_))[Mid] . pr SET[Mid] * (op __ : Set[Mid] Set[Mid] -> Set[Mid] to _._) . op review_excluding_from`:_ : Paper Set[Mid] Mid -> Contents . op delegate-to_ : Mid -> Contents . op review-result_ : Score -> Contents . op check-review__from`:_ : Paper Score Mid -> Contents . op check-review-result_ : Score -> Contents . op cannot-review : -> Contents . op finish : -> Contents . op unresolved : -> Contents . op unresolved-review_from`:_reviewers_ : Paper Mid List[Mid] -> Contents . op unresolved-delegate : -> Contents . op unresolved-review-result_ : Score -> Contents . endom) ***(% \end{verbatim} \normalsize \noindent and the message that a review form sends to the program chair: \small \begin{verbatim} %) (omod REVIEW-FORM-PROGR-CHAIR-MSGS is inc MOBILE-OBJECT-ADDITIONAL-DEFS . pr PAPER + SCORE . op review-result__from`:_ : Paper Score Mid -> Contents . endom) ***(% \end{verbatim} \normalsize %) ***(% \label{review-form} \small \begin{verbatim} %) (omod REVIEW-FORM is *** inc MOBILE-OBJECT-ADDITIONAL-DEFS . inc REVIEW-FORM-REVIEWER-MSGS . inc REVIEW-FORM-PROGR-CHAIR-MSGS . *** pr PAPER . pr NAME . pr DEFAULT[Score] . *** pr (LIST * (op nil to no-id, op __ to _&_))[Mid] . ***(% \end{verbatim} \normalsize % When a submission form creates several review forms, these are % given a \texttt{tmp-id} identifier, which is replaced by the % name of the mobile object in which they are placed by % \texttt{start-up} messages. In order to distinguish the different states in which a review form can be, the class \texttt{ReviewForm} has an attribute \texttt{state} of sort \texttt{ReviewFormState} with the following possible values. \small \begin{verbatim} %) sort ReviewFormState . ops inactive towards-reviewer back unresolved-towards-reviewer unresolved-back : -> ReviewFormState . ***(% \end{verbatim} \normalsize A reviewer may decide to review a paper assigned to him/her directly, or to send it to another reviewer. The review form must keep track of the chain of reviewers so that it can find its way back when either completed or refused, and so that each reviewer can check the work of the subreviewers. In case there is no agreement on the scores for a paper, a review form must go back to its reviewer. Objects of class \texttt{ReviewForm} have two attributes of sort \texttt{List[Mid]}. The attribute \texttt{chain} contains initially the id of the program committee assigned to it, and all the succesive subreviewers are added to this list. When the paper is finally reviewed, the form finds its way back by extracting the ids from the lists in a \emph{last-in-first-out} manner. Nevertheless, instead of discarding these ids, they are included in the list in the second attribute, \texttt{chain-back}, so that it can follow its reviewing path again if necessary. \small \begin{verbatim} %) class ReviewForm | paper : Paper, program-chair : Mid, chain : List[Mid], chain-back : List[Mid], refused : Set[Mid], score : Default[Score], state : ReviewFormState . var P : Paper . var PI : Pid . var I : MachineInt . vars O O' : Mid . vars OL OL' : List[Mid] . var OS : Set[Mid] . var Sc : Score . var Conf : Configuration . ***(% \end{verbatim} \normalsize When the mobile object form is created, the name of the form object in its belly must be started up, initializing its name and putting it in the \texttt{towards-reviewer} state. Note that changing the name of an object implies destroying the object in the lhs of the rule and creating a new one in the rhs with a different name, and therefore all attributes must be explicitly copied. This rule does not work for objects in subclasses in which new attributes are added. \small \begin{verbatim} %) rl [start-up] : < tmp-id : ReviewForm | paper : P, program-chair : O, chain : o(PI, I), chain-back : no-id, refused : mt, score : null, state : inactive > (to tmp-id : start-up(O')) Conf & none => < O' : ReviewForm | paper : P, chain : o(PI, I), chain-back : no-id, refused : mt, score : null, state : towards-reviewer, program-chair : O > Conf & go-find(o(PI, I), PI) . ***(% \end{verbatim} \normalsize We assume that, once the \texttt{go-find} command is given in the start-up rule, the review form object will not be able to do anything until the mobile object in which it is embedded is set to active, that is, until it has reached the assigned program committee member's process. This prevents from starting the exchange of messages before arriving to the author's object, which seems not to have much sense in this context. However, there is no reason to forbid this systematically, since there could be applications in which this is useful. % \framebox{\texttt{Quizas deberiamos ilustrar % ambos comportamientos}} The review form keeps track of the chain of reviewers so that it can find its way back when either completed or refused, and so that each reviewer can check the work of the subreviewers. When a review form gets to the process of a reviewer, which would be a program committee member in the first place, it sends a review message to the given reviewer (saying which reviewers he cannot delegate on) and waits for an answer. \small \begin{verbatim} %) op listToSet : List[Mid] -> Set[Mid] . eq listToSet(no-id) = mt . eq listToSet(O & OL) = (O . listToSet(OL)) . rl [ask-for-review] : < O : ReviewForm | paper : P, chain : OL & O', state : towards-reviewer, refused : OS, score : null > Conf & none => < O : ReviewForm | state : inactive > Conf & (to O' : review P excluding (listToSet(OL) . OS) from : O) . ***(% \end{verbatim} \normalsize Since in order to simplify the specification most of the messages do not contain any data, it does not make much sense to encrypt them. However, it is assumed that all messages are encrypted. Such an encryptation could be easily added by using encrypt and decrypt functions as follows. If an object \texttt{A} sends a message \texttt{M} to another object \texttt{B} we generally have a message \texttt{(to B :\ M from :\ A)}. Instead, if we assume \texttt{KU} and \texttt{KP} \texttt{B}'s public and private keys, respectively, we can consider a message \texttt{(to B :\ encrypt(M, KU) from :\ A)}, which can then be decrypted by \texttt{B} using its private key with an equation as \texttt{decrypt(encrypt(M, KU), KP) = M}. By using the keys in the reverse order we have the usual signing, that is, we can use private keys to sign messages and then used the corresponding public one to read it \texttt{decrypt(encrypt(M, KP), KU) = M}. There can be three different messages back: delegating the review to some subreviewer, refusing the review, or giving the review itself. If delegated, the form must find its way to the indicated subreviewer. \small \begin{verbatim} %) rl [review-delegation] : < O : ReviewForm | state : inactive, chain : OL > (to O : delegate-to o(PI, I)) Conf & none => < O : ReviewForm | state : towards-reviewer, chain : OL & o(PI, I) > Conf & go-find(o(PI, I), PI) . ***(% \end{verbatim} \normalsize If a reviewer refuses a review, the review form has to go back to the last reviewer who delegated, adding the refuser to the \texttt{refused} attribute. \small \begin{verbatim} %) rl [review-refused] : < O : ReviewForm | state : inactive, chain : OL & o(PI,I) & O', refused : OS > (to O : cannot-review) Conf & none => < O : ReviewForm | state : towards-reviewer, chain : OL & o(PI,I), refused : OS . O' > Conf & go-find(o(PI,I),PI) . ***(% \end{verbatim} \normalsize Once a review is obtained, depending on whether there is only one reviewer in the chain or more than one, the form goes back to the program chair---if there is only one then he/she is the program committee member himself/herself---or back to the reviewer that delegated on this one. \small \begin{verbatim} %) rl [review-result] : < O : ReviewForm | state : inactive, chain : O', chain-back : OL, program-chair : o(PI, I) > (to O : review-result Sc) Conf & none => < O : ReviewForm | state : back, score : Sc, chain : no-id, chain-back : O' & OL > Conf & go-find(o(PI, I), PI) . rl [review-result] : < O : ReviewForm | state : inactive, chain : OL & O' & o(PI, I), chain-back : OL' > (to O : review-result Sc) Conf & none => < O : ReviewForm | state : back, score : Sc, chain : OL & O', chain-back : o(PI, I) & OL' > Conf & go-find(o(PI, I), PI) . ***(% \end{verbatim} \normalsize In its way back, each reviewer checks the review. The review form passes by the processes of each of the reviewers, in such a way that each time it reaches the process of a new reviewer it request a checking from the reviewer, which may confirm or contradict the review. We assume that the score given by a reviewer prevails over the score given by his/her subreviewers. Another possibility would be to send it back to the subreviewer, asking for confirmation, or even for rectification. \small \begin{verbatim} %) rl [way-back] : < O : ReviewForm | paper : P, chain : OL & O', state : back, score : Sc > Conf & none => < O : ReviewForm | state : inactive > Conf & (to O' : check-review P Sc from : O) . rl [get-checked-review] : < O : ReviewForm | state : inactive, program-chair : o(PI, I), chain : O', chain-back : OL > (to O : check-review-result Sc) Conf & none => < O : ReviewForm | state : back, score : Sc, chain : no-id, chain-back : O' & OL > Conf & go-find(o(PI, I), PI) . rl [get-checked-review] : < O : ReviewForm | chain : OL & O' & o(PI, I), chain-back : OL', state : inactive > (to O : check-review-result Sc) Conf & none => < O : ReviewForm | score : Sc, state : back, chain : OL & O', chain-back : o(PI, I) & OL' > Conf & go-find(o(PI, I), PI) . ***(% \end{verbatim} \normalsize At some point, following the chain of reviewers, the review form reaches the program chair, which receives the review result. \small \begin{verbatim} %) rl [back-to-the-program-chair] : < O : ReviewForm | paper : P, chain : no-id, state : back, score : Sc, program-chair : O' > Conf & none => < O : ReviewForm | state : inactive > Conf & (to O' : review-result P Sc from : O) . ***(% \end{verbatim} \normalsize The program chair can say to a review form that it has finished. \small \begin{verbatim} %) rl [dead] : < O : ReviewForm | chain : no-id, state : inactive > (to O : finish) & none => (none).Configuration & kill . ***(% \end{verbatim} \normalsize The program chair can declare the review form unresolved. \small \begin{verbatim} %) rl [unresolved] : < O : ReviewForm | chain : no-id, chain-back : o(PI,I) & OL, state : inactive > (to O : unresolved) Conf & none => < O : ReviewForm | chain : o(PI,I), chain-back : OL, state : unresolved-towards-reviewer > Conf & go-find(o(PI,I), PI) . rl [unresolved-ask-for-review] : < O : ReviewForm | paper : P, chain : OL & O', chain-back : OL', state : unresolved-towards-reviewer > Conf & none => < O : ReviewForm | state : inactive > Conf & (to O' : unresolved-review P from : O reviewers OL') . rl [unresolved-review-delegation] : < O : ReviewForm | chain : OL, chain-back : o(PI,I) & OL', state : inactive > (to O : unresolved-delegate) Conf & none => < O : ReviewForm | chain : OL & o(PI,I), chain-back : OL', state : unresolved-towards-reviewer > Conf & go-find(o(PI,I), PI) . ***(% \end{verbatim} \normalsize When an unresolved review form receives a new result, it goes directly to the program chair. \small \begin{verbatim} %) rl [unresolved-review-result] : < O : ReviewForm | chain : OL, program-chair : o(PI,I), chain-back : OL', state : inactive > (to O : unresolved-review-result Sc) Conf & none => < O : ReviewForm | score : Sc, chain : no-id, chain-back : OL & OL', state : unresolved-back > Conf & go-find(o(PI,I), PI) . rl [unresolved-back-to-the-program-chair] : < O : ReviewForm | paper : P, chain : no-id, state : unresolved-back, score : Sc, program-chair : O' > Conf & none => < O : ReviewForm | state : inactive > Conf & (to O' : review-result P Sc from : O) . endom) ***(% \end{verbatim} \normalsize \subsection{Submission Form} \label{submission-form} These are the messages that a submission form and an author interchange: \small \begin{verbatim} %) (omod SUBMISSION-FORM-AUTHOR-MSGS is inc MOBILE-OBJECT-ADDITIONAL-DEFS . pr NAME + PAPER . op subm-form-gets-to-author`from`:_ : Mid -> Contents . op activate-subm-form : -> Contents . op request-author-name : -> Contents . op author-name : Name -> Contents . op request-paper : -> Contents . op paper : Paper -> Contents . endom) ***(% \end{verbatim} \normalsize \noindent and the messages that a submission form and the program chair interchange: \small \begin{verbatim} %) (omod SUBMISSION-FORM-PROGR-CHAIR-MSGS is inc MOBILE-OBJECT-ADDITIONAL-DEFS . pr NAME + PAPER . pr SET[Mid] * (op __ : Set[Mid] Set[Mid] -> Set[Mid] to _._) . op submission___from`:_ : Name Mid Paper Mid -> Contents . op generate-review-forms : Set[Mid] -> Contents . endom) ***(% \end{verbatim} \normalsize Once activated, the submission form actively guides most of the submission process. Each author fills an instance of the form and attaches a paper. The form checks that none of the required fields are left blank and finds its way to the program chair. \small \begin{verbatim} %) (omod SUBMISSION-FORM is *** inc MOBILE-OBJECT-ADDITIONAL-DEFS . inc SUBMISSION-FORM-AUTHOR-MSGS . inc SUBMISSION-FORM-PROGR-CHAIR-MSGS . pr REVIEW-FORM . pr DEFAULT[Name] . pr DEFAULT[Paper] . pr CHOOSE-REVIEWERS . *** pr SET[Mid] * (op __ : Set[Mid] Set[Mid] -> Set[Mid] to _._) . ***(% \end{verbatim} \normalsize % When the conference chair creates a form, it has \texttt{tmp-id} as identifier % initially, which is then replaced by the name of the mobile object in which % it is placed by a start-up message. In order to distinguish the different states in which a form can be, class \texttt{SubmForm} has an attribute \texttt{state} of sort \texttt{SubmFormState} with the following possible values. \small \begin{verbatim} %) sort SubmFormState . ops inactive towards-author waiting active towards-pc finishing finished : -> SubmFormState . ***(% \end{verbatim} \normalsize In fact, it is possibly enough with two states, so that we are able to detect the moment at which a form object arrives to the process of an author or program chair and then starts the communication with it. \small \begin{verbatim} %) class SubmForm | conf-chair : Mid, author : Mid, program-chair : Mid, author-name : Default[Name], paper : Default[Paper], state : SubmFormState . vars O O' O'' : Mid . var OS : Set[Mid] . var PI : Pid . var I : MachineInt . var Conf : Configuration . var N : Name . var P : Paper . var DN : Default[Name] . var DP : Default[Paper] . ***(% \end{verbatim} \normalsize When the mobile object submission form is created, the name of the form object in its belly must be started up, initializing its name and putting it in the \texttt{towards-author} state. \small \begin{verbatim} %) rl [start-up] : < tmp-id : SubmForm | author : o(PI, I), state : (inactive).SubmFormState, conf-chair : O', program-chair : O'', author-name : DN, paper : DP > (to tmp-id : start-up(O)) Conf & none => < O : SubmForm | author : o(PI, I), state : towards-author, conf-chair : O', program-chair : O'', author-name : DN, paper : DP > Conf & go-find(o(PI, I), PI) . ***(% \end{verbatim} \normalsize Once the form is in the \texttt{towards-author} state, it can initiate the validation process. Once the form reaches the author, the validation process is started by sending a \texttt{subm-form-gets-to-author} message. Then, the form goes to the \texttt{waiting} state, and is in such a state until it gets an \texttt{activate-subm-form} message from the corresponding author. \small \begin{verbatim} %) rl [request-activation] : < O : SubmForm | author : O', state : towards-author > Conf & none => < O : SubmForm | state : waiting > Conf & (to O' : subm-form-gets-to-author from : O) . ***(% \end{verbatim} \normalsize When the author accepts the form, that is, when it receives the \texttt{subm-form-gets-to-author} message from the form, then the author sends an \texttt{activate-subm-form} message to the form. The information about the author and the paper are then requested. Note that in the current version this is the only information being requested, and that since the communication between the form and the author is already established these messages do not include the form's identifier. Note also that the form goes to the active state. \small \begin{verbatim} %) rl [activation] : < O : SubmForm | author : O', state : waiting > (to O : activate-subm-form) Conf & none => < O : SubmForm | state : active > Conf & (to O' : request-author-name) (to O' : request-paper) . ***(% \end{verbatim} \normalsize When the submission form receives the messages with the name and the paper the corresponding attributes are updated. \small \begin{verbatim} %) rl [author-name] : < O : SubmForm | state : active > (to O : author-name(N)) => < O : SubmForm | author-name : N > . rl [paper] : < O : SubmForm | state : active > (to O : paper(P)) => < O : SubmForm | paper : P > . ***(% \end{verbatim} \normalsize When the submission form has the author's name and paper, then it moves to the program chair's process. Note that \texttt{N} and \texttt{P} are, respectively, variables of sorts \texttt{Name} and \texttt{Paper}, and therefore, if there is a match with this rule it is because the name and the paper are not null any more. \small \begin{verbatim} %) rl [move] : < O : SubmForm | author-name : N, paper : P, program-chair : o(PI, I), state : (active).SubmFormState > Conf & none => < O : SubmForm | state : towards-pc > Conf & go-find(o(PI, I), PI) . ***(% \end{verbatim} \normalsize When a submission form reaches the program chair the form gives the information about the submission to the program chair. \small \begin{verbatim} %) rl [get-to-pc] : < O : SubmForm | author-name : N, author : O'', paper : P, program-chair : O', state : towards-pc > Conf & none => < O : SubmForm | state : waiting > Conf & (to O' : submission N O'' P from : O) . ***(% \end{verbatim} \normalsize The program chair then assigns the submissions to the committee members, by instructing each submission form to generate a review form for each assigned member. \begin{comment} \small \begin{verbatim} %) ***( rl [gen-review-forms] : < O : SubmForm | program-chair : O' > (to O : generate-review-forms(O'' . OS)) Conf & none => < O : SubmForm | > (to O : generate-review-forms(OS)) Conf & newo(up(REVIEW-FORM), < tmp-id : ReviewForm | state : (inactive).ReviewFormState, score : null, program-chair : O', chain : O'', chain-back : no-id, paper : P >, tmp-id) . rl [gen-review-forms] : < O : SubmForm | > (to O : generate-review-forms(mt)) => (none).Configuration . ) ***(% \end{verbatim} \normalsize \end{comment} \small \begin{verbatim} %) op create-review-forms : Paper Mid Set[Mid] -> MsgSet . eq create-review-forms(P, O', mt) = (none).MsgSet . eq create-review-forms(P, O', O'' . OS) = newo(up(REVIEW-FORM), < tmp-id : ReviewForm | state : (inactive).ReviewFormState, score : null, program-chair : O', chain : O'', chain-back : no-id, refused : mt, paper : P >, tmp-id) create-review-forms(P, O', OS) . rl [gen-review-forms] : < O : SubmForm | program-chair : O', paper : P > (to O : generate-review-forms(OS)) Conf & none => < O : SubmForm | state : finishing > Conf & create-review-forms(P, O', OS) . ***(% \end{verbatim} \normalsize Here, we are assuming that \texttt{newo} takes a module (a term of sort \texttt{Module} metarepresenting a module), a configuration (which will be the initial configuration to put in the belly of the mobile object to be created), and the provisional identifier of the main object in the configuration given as second argument. We assume that the first action accomplished by the system when it detects the \texttt{newo} message is to create a new mobile object with the configuration given as second argument of the \texttt{newo} message in it, and then sending a \texttt{start-up} message to the main object with its new name, so it coincides with the name of the mobile object it is in. Mobile objects take their names when they are created, and they are of the form \texttt{o(P, N)}, where \texttt{P} is the name of the mobile object's home process and \texttt{N} is a number. This is done in this way because we follow the convention of naming the `main' object in a mobile object as such a mobile object, so that it just have to move messages down into its belly. Another alternative would be, for example, to make each mobile object keep the identifier of this main object, and then change the addresse of the messages before taking it in. A submission form kills itself after generating the review forms. \small \begin{verbatim} %) rl [dead] : < O : SubmForm | state : finishing > Conf & none => < O : SubmForm | state : finished > Conf & kill . endom) ***(% \end{verbatim} \normalsize \subsection{Author} These are the message contents that the conference chair and an author interchange. \texttt{announcement} is the message that the conference chair sends to each author announcing a conference (and providing the conference chair id), and \texttt{submission-request} is the author's response (providing his id). \small \begin{verbatim} %) (omod CONF-CHAIR-AUTHOR-MSGS is inc MOBILE-OBJECT-ADDITIONAL-DEFS . op announcement`from`:_ : Mid -> Contents . op submission-request`from`:_ : Mid -> Contents . endom) ***(% \end{verbatim} \normalsize %) ***(% %\subsection{Author} And the messages that an author interchange with a report form or a final submission form: \small \begin{verbatim} %) (omod REPORT-FORM-AUTHOR-MSGS is inc MOBILE-OBJECT-ADDITIONAL-DEFS . op congratulations : -> Contents . op regrets : -> Contents . endom) (omod FINAL-SUBMISSION-FORM-AUTHOR-MSGS is inc MOBILE-OBJECT-ADDITIONAL-DEFS . pr PAPER . op final-subm-form-gets-to-author`from`:_ : Mid -> Contents . op final-paper : Paper -> Contents . endom) ***(% \end{verbatim} \normalsize We suppose that each author has at most one paper. \small \begin{verbatim} %) (omod AUTHOR is *** inc MOBILE-OBJECT-ADDITIONAL-DEFS . inc SUBMISSION-FORM-AUTHOR-MSGS . inc CONF-CHAIR-AUTHOR-MSGS . inc REPORT-FORM-AUTHOR-MSGS . inc FINAL-SUBMISSION-FORM-AUTHOR-MSGS . pr DEFAULT[Mid] . pr DEFAULT[Paper] . pr NAME . class Author | name : Name, paper : Default[Paper], submission-form : Default[Mid] . vars O O' : Mid . var Conf : Configuration . var N : Name . var P : Paper . ***(% \end{verbatim} \normalsize When an author receives a conference's announcement, he/she decides whether requesting a submission form or not. \small \begin{verbatim} %) rl [author-gets-announcement] : < O : Author | paper : P > (to O : announcement from : O') Conf & none => < O : Author | > Conf & (to O' : submission-request from : O) . ***(% \end{verbatim} \normalsize In order to see what is happening when executing the system we assume that if an author has a paper then he/she requests a submission form. Hence, we omit the following rule: \small \begin{verbatim} rl [author-gets-announcement] : < O : Author | > (to O : announcement from : O') => < O : Author | > . \end{verbatim} \normalsize When the submission form mobile object reaches the process in which there is an author, the form sends a message \texttt{subm-form-gets-to-author} to let the author know about it, which responds activating the form to initiate the submission process. The author should check the chairman's signature before activating the submission form. \small \begin{verbatim} %) rl [activate-form] : < O : Author | > (to O : subm-form-gets-to-author from : O') Conf & none => < O : Author | submission-form : O' > Conf & to O' : activate-subm-form . ***(% \end{verbatim} \normalsize The author sends its name and paper to the submission form when requested. \small \begin{verbatim} %) rl [request-name] : < O : Author | name : N, submission-form : O' > (to O : request-author-name) Conf & none => < O : Author | > Conf & to O' : author-name(N) . rl [request-paper] : < O : Author | paper : P, submission-form : O' > (to O : request-paper) Conf & none => < O : Author | > Conf & to O' : paper(P) . ***(% \end{verbatim} \normalsize An author can receive congratulations or regrets from a report form. \small \begin{verbatim} %) rl [get-congratulations] : < O : Author | > (to O : congratulations) Conf & none => < O : Author | > Conf & none . rl [get-regrets] : < O : Author | paper : P > (to O : regrets) Conf & none => < O : Author | paper : rejected(P) > Conf & none . ***(% \end{verbatim} \normalsize When the final submission form is created by an accepted paper report form, it sends a message \texttt{final-subm-form-gets-to-author} to the author, which responds sending it the final version of the paper. \small \begin{verbatim} %) rl [send-final-version] : < O : Author | paper : P > (to O : final-subm-form-gets-to-author from : O') Conf & none => < O : Author | paper : final-version(P) > Conf & (to O' : final-paper(final-version(P))) . endom) ***(% \end{verbatim} \normalsize %) ***(% \subsection{Reviewers} \small \begin{verbatim} %) (omod REVIEWER is inc REVIEW-FORM-REVIEWER-MSGS . pr AUTHOR . *** pr SCORE . *** pr SET[Mid] * (op __ : Set[Mid] Set[Mid] -> Set[Mid] to _._) . pr SET[Paper] * (op __ : Set[Paper] Set[Paper] -> Set[Paper] to _._) . class Reviewer | subreviewers : Set[Mid], done : Set[Paper] . ***(% \end{verbatim} \normalsize Any reviewer can be interested in submitting a paper to the conference. \small \begin{verbatim} %) subclass Reviewer < Author . var P : Paper . var PS : Set[Paper] . vars O O' O'' : Mid . vars OS OS' : Set[Mid] . var OL : List[Mid] . var Sc : Score . var Conf : Configuration . ***(% \end{verbatim} \normalsize A reviewer can give three different answers to a review message: it can delegate in some other reviewer, it can refuse the review because it has already participated in the review of the given paper, or it can do the review and send back the result, which can be accept or reject. A reviewer should only be able to delegate in someone who has not accepted or delegated the paper yet. The review form keeps this information, and send it in the ``excluding'' part of the review request. \small \begin{verbatim} %) crl [delegate-review] : < O : Reviewer | subreviewers : O' . OS, done : PS > (to O : review P excluding OS' from : O'') Conf & none => < O : Reviewer | done : PS . P > Conf & (to O'' : delegate-to O') if not (O' in OS') . rl [review-accept] : < O : Reviewer | done : PS > (to O : review P excluding OS from : O') Conf & none => if (P in PS) then (< O : Reviewer | > Conf & (to O' : cannot-review)) else (< O : Reviewer | done : PS . P > Conf & (to O' : review-result accept)) fi . rl [review-reject] : < O : Reviewer | done : PS > (to O : review P excluding OS from : O') Conf & none => if P in PS then < O : Reviewer | > Conf & (to O' : cannot-review) else < O : Reviewer | done : PS . P > Conf & (to O' : review-result reject) fi . ***(% \end{verbatim} \normalsize In the way back of the review form, each reviewer checks the review. \small \begin{verbatim} %) rl [agree-review-check] : < O : Reviewer | > (to O : check-review P Sc from : O') Conf & none => < O : Reviewer | > Conf & (to O' : check-review-result Sc) . rl [disagree-review-check] : < O : Reviewer | > (to O : check-review P Sc from : O') Conf & none => < O : Reviewer | > Conf & (to O' : check-review-result opp(Sc)) . ***(% \end{verbatim} \normalsize When an unresolved review form asks for a new review, the reviewer can delegate again, or give a result. \small \begin{verbatim} %) rl [unresolved-delegate-review] : < O : Reviewer | > (to O : unresolved-review P from : O' reviewers O'' & OL) Conf & none => < O : Reviewer | > Conf & (to O' : unresolved-delegate) . rl [unresolved-review-accept] : < O : Reviewer | > (to O : unresolved-review P from : O' reviewers OL) Conf & none => < O : Reviewer | > Conf & (to O' : unresolved-review-result accept) . rl [unresolved-review-reject] : < O : Reviewer | > (to O : unresolved-review P from : O' reviewers OL) Conf & none => < O : Reviewer | > Conf & (to O' : unresolved-review-result reject) . endom) ***(% \end{verbatim} \normalsize %) ***(% \subsection{Conference Chair} The following module defines the message sent by the program chair to the conference chair when the proceedings are complete. \small \begin{verbatim} %) (omod CONF-CHAIR-PROGR-CHAIR-MSGS is inc MOBILE-OBJECT-ADDITIONAL-DEFS . pr SET[Paper] * (op __ : Set[Paper] Set[Paper] -> Set[Paper] to _._) . op proceedings : Set[Paper] -> Contents . endom) (omod CONF-CHAIR is pr SUBMISSION-FORM . pr CONF-CHAIR-AUTHOR-MSGS . inc CONF-CHAIR-PROGR-CHAIR-MSGS . inc REVIEWER . pr BROADCAST . *** pr SET[Mid] * (op __ : Set[Mid] Set[Mid] -> Set[Mid] to _._) . *** pr SET[Paper] * (op __ : Set[Paper] Set[Paper] -> Set[Paper] to _._) . class ConfChair | mailing-list : Set[Mid], program-chair : Mid, proceedings : Set[Paper] . ***(% \end{verbatim} \normalsize A conference chair can also be a reviewer and an author. \small \begin{verbatim} %) subclasses ConfChair < Author Reviewer . ***(% \end{verbatim} \normalsize The \texttt{start} message is used when simulating an example. It is sent to the conference chair in order to start all the process. \small \begin{verbatim} %) op start : -> Contents . var MS : MsgSet . vars O O' O'' : Mid . var OS : Set[Mid] . var Conf : Configuration . var MC : Contents . var PS : Set[Paper] . ***(% \end{verbatim} \normalsize The conference review process starts with the broadcasting of the announcement message to all the potential authors in its mailing list. \small \begin{verbatim} %) rl [review-process-starts] : < O : ConfChair | mailing-list : OS > (to O : start) Conf & none => < O : ConfChair | > Conf & broadcast(OS, announcement from : O) . ***(% \end{verbatim} \normalsize Each of the authors receives the announcement and decides whether requesting a submission form or not. They request a form by sending a \texttt{submission-request} message to the conference chair, who then creates the corresponding forms and sends them to the authors. When the conference chair receives a \texttt{submission-request} message he/she creates a submission form, which finds its way to the corresponding author. It could have been specified in other ways, e.g., the forms could be created by the respective authors after receiving the message from the conference chair. Note that the conference chair does not keep track of the potential authors to which he/she is sending the submission forms. We may assume that such forms are destroyed if certain deadline is reached. \small \begin{verbatim} %) rl [conf-chair-receives-submission-request] : < O : ConfChair | program-chair : O' > (to O : submission-request from : O'') Conf & none => < O : ConfChair | > Conf & newo(up(SUBMISSION-FORM), < tmp-id : SubmForm | author : O'', conf-chair : O, program-chair : O', author-name : null, paper : null, state : (inactive).SubmFormState >, tmp-id) . ***(% \end{verbatim} \normalsize When all the review process has finished, the conference chair receives the proceedings from the program chair. Note that we make sure that this message is received only if there are no proceedings already available. \small \begin{verbatim} %) rl [receive-proceedings] : < O : ConfChair | proceedings : mt > (to O : proceedings(PS)) => < O : ConfChair | proceedings : PS > . endom) ***(% \end{verbatim} \normalsize %) ***(% \subsection{Final Submission Form} A final submission form communicates its final paper to the program chair by using the message \texttt{final-paper}. \small \begin{verbatim} %) (omod FINAL-SUBMISSION-FORM-PROGR-CHAIR-MSGS is inc MOBILE-OBJECT-ADDITIONAL-DEFS . inc PAPER . op final-paper : Mid Paper -> Contents . endom) (omod FINAL-SUBMISSION-FORM is inc MOBILE-OBJECT-ADDITIONAL-DEFS . inc FINAL-SUBMISSION-FORM-AUTHOR-MSGS . inc FINAL-SUBMISSION-FORM-PROGR-CHAIR-MSGS . *** pr PAPER . sort FinalSubmFormState . ops inactive waiting towards-pc finished : -> FinalSubmFormState . class FinalSubmForm | author : Mid, state : FinalSubmFormState, paper : Paper, program-chair : Mid . vars O O' O'' : Mid . vars P P' : Paper . var PI : Pid . var I : MachineInt . var Conf : Configuration . rl [start-up] : < tmp-id : FinalSubmForm | author : O', state : inactive, paper : P, program-chair : O'' > (to tmp-id : start-up(O)) Conf & none => < O : FinalSubmForm | author : O', state : waiting, paper : P, program-chair : O'' > Conf & (to O' : final-subm-form-gets-to-author from : O) . *** rl [notify-author] : *** < O : FinalSubmForm | author : O', state : inactive > Conf & none *** => < O : FinalSubmForm | author : O', state : waiting > *** Conf & (to O' : final-subm-form-gets-to-author from : O) . ***(% \end{verbatim} \normalsize When the final submission form gets the final version of the paper from the author, it goes towards the program chair. \small \begin{verbatim} %) rl [get-final-version] : < O : FinalSubmForm | paper : P, state : waiting, program-chair : o(PI, I) > (to O : final-paper(P')) Conf & none => < O : FinalSubmForm | paper : P', state : towards-pc > Conf & go-find(o(PI,I), PI) . ***(% \end{verbatim} \normalsize Once the final submission form reaches the program chair, it sends the final paper to him and dies. \small \begin{verbatim} %) rl [send-final-version] : < O : FinalSubmForm | author : O', paper : P, state : towards-pc, program-chair : O'' > Conf & none => < O : FinalSubmForm | state : finished > Conf & (to O'' : final-paper(O', P)) . rl [dead] : < O : FinalSubmForm | state : finished > Conf & none => none & kill . endom) ***(% \end{verbatim} \normalsize %) ***(% \subsection{Report Form} \small \begin{verbatim} %) (omod REPORT-FORM is *** inc MOBILE-OBJECT-ADDITIONAL-DEFS . inc REPORT-FORM-AUTHOR-MSGS . pr FINAL-SUBMISSION-FORM . pr SCORE . *** pr PAPER . sort ReportFormState . ops inactive towards-author finished : -> ReportFormState . class ReportForm | paper : Paper, author : Mid, score : Score, state : ReportFormState, program-chair : Mid . vars O O' O'' O''' : Mid . var PI : Pid . var I : MachineInt . var Conf : Configuration . var P : Paper . var Sc : Score . ***(% \end{verbatim} \normalsize When a report form is created, the name of the form object in its belly must be started up, initializing its name and putting it in the \texttt{towards-author} state. \small \begin{verbatim} %) rl [start-up] : < tmp-id : ReportForm | paper : P, author : o(PI, I), score : Sc, state : (inactive).ReportFormState, program-chair : O' > (to tmp-id : start-up(O)) Conf & none => < O : ReportForm | paper : P, author : o(PI, I), score : Sc, state : towards-author, program-chair : O' > Conf & go-find(o(PI, I), PI) . ***(% \end{verbatim} \normalsize When an accepted paper report form reaches the author, it sends congratulations and spawns a final submission form, which will ask the author for the final version of the paper. After that, the final submission form dies. \small \begin{verbatim} %) rl [send-congratulations] : < O : ReportForm | paper : P, author : O', score : accept, state : towards-author, program-chair : O'' > Conf & none => < O : ReportForm | state : (finished).ReportFormState > Conf & (to O' : congratulations) newo(up(FINAL-SUBMISSION-FORM), < tmp-id : FinalSubmForm | author : O', state : (inactive).FinalSubmFormState, paper : P, program-chair : O'' >, tmp-id) . *** rl [send-congratulations-and-transform-into-a-final-form] : *** < O : ReportForm | paper : P, author : O', score : accept, *** state : towards-author, program-chair : O'' > Conf & none *** => < O : FinalSubmForm | author : O', state : (inactive).FinalSubmFormState, *** paper : P, program-chair : O'' > Conf *** & (to O' : congratulations) . ***(% \end{verbatim} \normalsize When a rejected paper report form reaches the author, it sends regrets and dies. \small \begin{verbatim} %) *** rl [send-regrets-and-die] : *** < O : ReportForm | author : O', score : reject, state : towards-author > *** Conf & none *** => none & (to O' : regrets) kill . rl [send-regrets-and-finish] : < O : ReportForm | author : O', score : reject, state : towards-author > Conf & none => < O : ReportForm | state : (finished).ReportFormState > Conf & (to O' : regrets) . rl [dead] : < O : ReportForm | state : (finished).ReportFormState > Conf & none => none & kill . endom) ***(% \end{verbatim} \normalsize %) ***(% \subsection{Program Chair} The submission info that the program chair maintains consists of the name and address of the contact author, title of the paper, and the set of scores received so far for the given paper. \small \begin{verbatim} %) (view Set`[Mid`] from TRIV to SET[Mid] * (op __ : Set[Mid] Set[Mid] -> Set[Mid] to _._) is sort Elt to Set[Mid] . endv) ***(view Bag`[Score`] from TRIV to BAG[Score] is sort Elt to Bag[Score] . endv) ***(% \end{verbatim} \normalsize The so far received scores are kept in a set of tuples (Mid, Score). The module \texttt{SET-RESULT} defines several operations to work with these sets. \small \begin{verbatim} %) (view Result from TRIV to TUPLE(2)[Mid, Score] * (sort Tuple[Mid, Score] to Result) is sort Elt to Result . endv) (fmod SET-RESULT is pr SET[Result] * (op __ : Set[Result] Set[Result] -> Set[Result] to _._) . pr SET[Mid] * (op __ : Set[Mid] Set[Mid] -> Set[Mid] to _._) . pr SCORE . op size : Set[Result] -> MachineInt . op agreement : Set[Result] -> Bool . op all-equal : Score Set[Result] -> Bool . op reviewers : Set[Result] -> Set[Mid] . op decision : Set[Result] -> Score . op majority : Set[Result] -> Score . var R : Result . var RS : Set[Result] . vars O O' : Mid . vars Sc Sc' : Score . eq size(mt) = 0 . eq size(R . RS) = 1 + size(RS) . eq agreement(mt) = true . eq agreement((O, Sc) . RS) = all-equal(Sc, RS) . eq all-equal(Sc, mt) = true . eq all-equal(Sc, (O, Sc') . RS) = (Sc == Sc') and all-equal(Sc, RS) . eq reviewers(mt) = mt . eq reviewers((O, Sc') . RS) = O . reviewers(RS) . eq decision(mt) = accept . ceq decision((O, Sc) . RS) = Sc if agreement((O, Sc) . RS) . ceq decision(RS) = majority(RS) if not agreement(RS) . ceq majority(RS) = decision(RS) if agreement(RS) . ceq majority((O, reject) . (O', accept) . RS) = majority(RS) if not agreement((O, reject) . (O', accept) . RS) . endfm) (view Set`[Result`] from TRIV to SET-RESULT is sort Elt to Set[Result] . endv) (view SubmissionInfo from TRIV to TUPLE(5)[Name, Mid, Paper, Set`[Result`], MachineInt] * (sort Tuple[Name, Mid, Paper, Set`[Result`], MachineInt] to SubmissionInfo) is sort Elt to SubmissionInfo . endv) (omod PROGR-CHAIR is *** inc MOBILE-OBJECT-ADDITIONAL-DEFS . *** inc AUTHOR . inc SUBMISSION-FORM-PROGR-CHAIR-MSGS . inc REVIEW-FORM-PROGR-CHAIR-MSGS . inc CONF-CHAIR-PROGR-CHAIR-MSGS . inc REVIEWER . pr SET[SubmissionInfo] . *** pr SET[Mid] * (op __ : Set[Mid] Set[Mid] -> Set[Mid] to _._) . *** pr SET[Paper] * (op __ : Set[Paper] Set[Paper] -> Set[Paper] to _._) . *** pr BAG[Score] . pr REPORT-FORM . pr BROADCAST . pr CHOOSE-REVIEWERS . class ProgrChair | conference-chair : Mid, committee-members : Set[Mid], number-of-reviewers : MachineInt, submissions : Set[SubmissionInfo], accepted : Set[Mid], proceedings : Set[Paper] . ***(% \end{verbatim} \normalsize A program chair can also be an author and a reviewer. \small \begin{verbatim} %) subclasses ProgrChair < Author Reviewer . var N : Name . var P : Paper . vars O O' O'' CM CM' : Mid . vars OS OS' : Set[Mid] . var Conf : Configuration . var Subms : Set[SubmissionInfo] . *** var ScB : Bag[Score] . vars Sc Sc' : Score . var PS : Set[Paper] . vars I I' : MachineInt . var MC : Contents . var TS : Set[Result] . ***(% \end{verbatim} \normalsize When the program chair gets a submission then he/she assigns it to two committee members (hopefully, following some criteria, although here they are chosen nondeterministically; it could be two, three, or any other number of referees, or even a nonfix number). % We assume that there are two reviewers per paper. The program chair asks the submission form to create a review form for each assigned member. \small \begin{verbatim} %) rl [pc-gets-submission] : < O : ProgrChair | committee-members : OS, submissions : Subms, number-of-reviewers : I > (to O : submission N O'' P from : O') Conf & none => < O : ProgrChair | submissions : ((N, O'', P, mt, 0) Subms) > Conf & (to O' : generate-review-forms(choose(OS, I))) . ***(% \end{verbatim} \normalsize When the review forms come back to the program chair's process, they send him the results of the review. The program chair saves this information together with the corresponding submission. \small \begin{verbatim} %) rl [pc-gets-review-result] : < O : ProgrChair | submissions : ((N, O'', P, TS, I) Subms) > (to O : review-result P Sc from : O') => < O : ProgrChair | submissions : ((N, O'', P, TS . (O', Sc), I) Subms) > . ***(% \end{verbatim} \normalsize If the reviews are in disagreement, the program chair declares the review forms unresolved unless three review rounds have been done yet. \small \begin{verbatim} %) crl [disagreement] : < O : ProgrChair | submissions : ((N, O', P, TS, I) Subms), number-of-reviewers : I' > Conf & none => < O : ProgrChair | submissions : ((N, O', P, mt, I + 1) Subms) > Conf & broadcast(reviewers(TS), unresolved) if (size(TS) == I') and (I < 2) and (not agreement(TS)). ***(% \end{verbatim} \normalsize If the reviews are in agreement or the number of rounds reaches the limit, the program chair creates a report form that will find its way back to the author and sends termination messages to all the review forms related to this paper. If there is an agreement then the \texttt{decision} function returns the agreed score, otherwise the majority decides. In case of disagreement with an even result then the paper is accepted. \small \begin{verbatim} %) crl [agreement] : < O : ProgrChair | submissions : ((N, O', P, TS, I) Subms), accepted : OS, number-of-reviewers : I' > Conf & none => < O : ProgrChair | submissions : Subms, accepted : (if decision(TS) == accept then O' . OS else OS fi) > Conf & newo(up(REPORT-FORM), < tmp-id : ReportForm | paper : P, author : O', score : decision(TS), state : (inactive).ReportFormState, program-chair : O >, tmp-id) broadcast(reviewers(TS), finish) if (size(TS) == I') and (agreement(TS) or (I == 2)) . ***(% \end{verbatim} \normalsize Finally, the final submission form with the final version of the paper, sends it to the program chair, which will merge the papers into the proceedings. \small \begin{verbatim} %) rl [get-final-versions] : < O : ProgrChair | proceedings : PS, accepted : O' . OS > (to O : final-paper(O', P)) => < O : ProgrChair | proceedings : PS . P, accepted : OS > . ***(% \end{verbatim} \normalsize When the final versions of all accepted papers have arrived to the program chair, and there is no unresolved submission, the program chair sends the proceedings to the conference chair. \small \begin{verbatim} %) crl [send-proceedings] : < O : ProgrChair | proceedings : PS, submissions : mt, accepted : mt, conference-chair : O' > Conf & none => < O : ProgrChair | proceedings : mt > Conf & (to O' : proceedings(PS)) if PS =/= mt . endom) ***(% \end{verbatim} \normalsize %) ***(% \subsection{Program committee members} \small \begin{verbatim} %) (omod PROGRAM-COMMITTEE-MEMBER is inc REVIEWER . inc AUTHOR . class PCMember . subclass PCMember < Reviewer Author . endom) ***(% \end{verbatim} \normalsize %) ***(% \subsection{Example} It is supposed all communications are signed and encrypted! % In the current version we are just dealing with the part in % which the papers are submitted. In the final state we'll have % all the forms with the papers and the author's info in the % process with the program chair. \small \begin{verbatim} %) (omod CONF-REVIEW is inc MOBILE-MAUDE . pr CONF-CHAIR . pr PROGRAM-COMMITTEE-MEMBER . pr PROGR-CHAIR . op m# : Qid -> Module . op m# : Qid MobObjState -> Term . op initial : -> Configuration . ***(% \end{verbatim} \normalsize In this initial configuration there are one conference chair, one program chair, and four authors. Each of these objects is in a different process. These processes are distributed in three locations as follows: \small \begin{verbatim} %) *** 'l0 *** p('l0, 0) *** o(p('l0, 0), 0) ConfChair *** o(p('l0, 0), 1) Reviewer *** p('l0, 1) *** o(p('l0, 1), 0) Author *** o(p('l0, 1), 1) PCMember *** 'l1 *** p('l1, 0) *** o(p('l1, 0), 0) Author *** p('l1, 1) *** o(p('l1, 1), 0) Author *** o(p('l1, 1), 1) PCMember *** 'l2 *** p('l2, 0) *** o(p('l2, 0), 0) ProgrChair *** p('l2, 1) *** o(p('l2, 1), 0) Author *** o(p('l2, 1), 1) Reviewer *** p('l2, 2) *** o(p('l2, 2), 0) Reviewer rl [initial-state] : initial => < 'l0 : R | cnt : 2 > < 'l1 : R | cnt : 2 > < 'l2 : R | cnt : 3 > < p('l0, 0) : P | cnt : 2, cf : < o(p('l0, 0), 0) : MO | mod : up(CONF-CHAIR), s : up(CONF-CHAIR, < o(p('l0, 0), 0) : ConfChair | hidden-gas : 300, submission-form : null, name : conf-chair, paper : null, subreviewers : o(p('l0, 0), 1), done : mt, mailing-list : (o(p('l0, 1), 0) . o(p('l1, 0), 0) . o(p('l1, 1), 0) . o(p('l2, 1), 0)), program-chair : o(p('l2, 0), 0), proceedings : mt > (to o(p('l0, 0), 0) : start) & none), p : p('l0, 0), gas : 300, hops : 0, mode : active > < o(p('l0, 0), 1) : MO | mod : up(REVIEWER), s : up(REVIEWER, < o(p('l0, 0), 1) : Reviewer | hidden-gas : 300, submission-form : null, name : reviewer1, paper : null, subreviewers : mt, done : mt > & none), p : p('l0, 0), gas : 300, hops : 0, mode : active >, guests : o(p('l0, 0), 0) . o(p('l0, 0), 1), forward : (0, (p('l0, 0), 0)) (1, (p('l0, 0), 0)) > < p('l0, 1) : P | cnt : 2, cf : < o(p('l0, 1), 0) : MO | mod : up(AUTHOR), s : up(AUTHOR, < o(p('l0, 1), 0) : Author | hidden-gas : 300, submission-form : null, name : author1, paper : p1 > & none), p : p('l0, 1), gas : 300, hops : 0, mode : active > < o(p('l0, 1), 1) : MO | mod : up(PROGRAM-COMMITTEE-MEMBER), s : up(PROGRAM-COMMITTEE-MEMBER, < o(p('l0, 1), 1) : PCMember | hidden-gas : 300, submission-form : null, name : pc-member1, paper : null, subreviewers : o(p('l0, 0), 1), done : mt > & none), p : p('l0, 1), gas : 300, hops : 0, mode : active >, guests : o(p('l0, 1), 0) . o(p('l0, 1), 1), forward : (0, (p('l0, 1), 0)) (1, (p('l0, 1), 0)) > < p('l1, 0) : P | cnt : 1, cf : < o(p('l1, 0), 0) : MO | mod : up(AUTHOR), s : up(AUTHOR, < o(p('l1, 0), 0) : Author | hidden-gas : 300, submission-form : null, name : author2, paper : p2 > & none), p : p('l1, 0), gas : 300, hops : 0, mode : active >, guests : o(p('l1, 0), 0), forward : (0, (p('l1, 0) ,0)) > < p('l1, 1) : P | cnt : 2, cf : < o(p('l1, 1), 0) : MO | mod : up(AUTHOR), s : up(AUTHOR, < o(p('l1, 1), 0) : Author | hidden-gas : 300, submission-form : null, name : author3, paper : p3 > & none), p : p('l1, 1), gas : 300, hops : 0, mode : active > < o(p('l1, 1), 1) : MO | mod : up(PROGRAM-COMMITTEE-MEMBER), s : up(PROGRAM-COMMITTEE-MEMBER, < o(p('l1, 1), 1) : PCMember | hidden-gas : 300, submission-form : null, name : pc-member2, paper : null, subreviewers : o(p('l2, 1), 1), done : mt > & none), p : p('l1, 1), gas : 300, hops : 0, mode : active >, guests : o(p('l1, 1), 0) . o(p('l1, 1), 1), forward : (0, (p('l1, 1), 0)) (1, (p('l1, 1), 0)) > < p('l2, 0) : P | cnt : 1, cf : < o(p('l2, 0), 0) : MO | mod : up(PROGR-CHAIR), s : up(PROGR-CHAIR, < o(p('l2, 0), 0) : ProgrChair | hidden-gas : 300, conference-chair : o(p('l0, 0), 0), committee-members : (o(p('l0, 1), 1) . o(p('l1, 1), 1) . o(p('l2, 0), 0)), number-of-reviewers : 3, submissions : mt, accepted : mt, proceedings : mt, submission-form : null, name : program-chair, paper : null, subreviewers : (o(p('l2, 2), 0) . o(p('l2, 1), 1)), done : mt > & none), p : p('l2, 0), gas : 300, hops : 0, mode : active >, guests : o(p('l2, 0), 0), forward : (0, (p('l2, 0) ,0)) > < p('l2, 1) : P | cnt : 2, cf : < o(p('l2, 1), 0) : MO | mod : up(AUTHOR), s : up(AUTHOR, < o(p('l2, 1), 0) : Author | hidden-gas : 300, submission-form : null, name : author4, paper : p4 > & none), p : p('l2, 1), gas : 300, hops : 0, mode : active > < o(p('l2, 1), 1) : MO | mod : up(REVIEWER), s : up(REVIEWER, < o(p('l2, 1), 1) : Reviewer | hidden-gas : 300, submission-form : null, name : reviewer2, paper : null, subreviewers : o(p('l2, 2), 0), done : mt > & none), p : p('l2, 1), gas : 300, hops : 0, mode : active >, guests : o(p('l2, 1), 0) . o(p('l2, 1), 1), forward : (0, (p('l2, 1) ,0)) (1, (p('l2, 1) ,0)) > < p('l2, 2) : P | cnt : 1, cf : < o(p('l2, 2), 0) : MO | mod : up(REVIEWER), s : up(REVIEWER, < o(p('l2, 2), 0) : Reviewer | hidden-gas : 300, submission-form : null, name : reviewer3, paper : null, subreviewers : mt, done : mt > & none), p : p('l2, 2), gas : 300, hops : 0, mode : active >, guests : o(p('l2, 2), 0), forward : (0, (p('l2, 1) ,0)) > . endom) ***( Execution of the above example Maude> (MO grew [28] [10] initial .) rewrites: 42756748 in 1010390ms cpu (1019800ms real) (42317 rewrites/second) Result Configuration : < 'l0 : R | hidden-gas : 10 , cnt : 2 > < 'l1 : R | hidden-gas : 10 , cnt : 2 > < 'l2 : R | hidden-gas : 10 , cnt : 3 > < p ( 'l0 , 0 ) : P | hidden-gas : 10 , cf : ( < o ( p ( 'l0 , 0 ) , 0 ) : MO | hidden-gas : 0 , mod : up ( CONF-CHAIR ) , s : up ( CONF-CHAIR , < o ( p ( 'l0 , 0 ) , 0 ) : ConfChair | hidden-gas : 44 , paper : null , program-chair : o ( p ( 'l2 , 0 ) , 0 ) , submission-form : null , name : conf-chair , done : mt , subreviewers : o ( p ( 'l0 , 0 ) , 1 ) , proceedings : ( final-version ( p1 ) . final-version ( p2 ) . final-version ( p4 ) ) , mailing-list : ( o ( p ( 'l0 , 1 ) , 0 ) . o ( p ( 'l1 , 0 ) , 0 ) . o ( p ( 'l1 , 1 ) , 0 ) . o ( p ( 'l2 , 1 ) , 0 ) ) > & none ) , mode : active , hops : 0 , gas : 43 , p : p ( 'l0 , 0 ) > < o ( p ( 'l0 , 0 ) , 1 ) : MO | hidden-gas : 0 , mod : up ( REVIEWER ) , s : up ( REVIEWER , < o ( p ( 'l0 , 0 ) , 1 ) : Reviewer | hidden-gas : 33 , paper : null , submission-form : null , name : reviewer1 , done : p2 , subreviewers : mt > & none ) , mode : active , hops : 0 , gas : 32 , p : p ( 'l0 , 0 ) > ) , forward : ( ( 0 , ( p ( 'l0 , 0 ) , 0 ) ) ( 1 , ( p ( 'l0 , 0 ) , 0 ) ) ) , guests : ( o ( p ( 'l0 , 0 ) , 0 ) . o ( p ( 'l0 , 0 ) , 1 ) ) , cnt : 6 > < p ( 'l0 , 1 ) : P | hidden-gas : 10 , cf : ( < o ( p ( 'l0 , 1 ) , 0 ) : MO | hidden-gas : 0 , mod : up ( AUTHOR ) , s : up ( AUTHOR , < o ( p ( 'l0 , 1 ) , 0 ) : Author | hidden-gas : 42 , paper : final-version ( p1 ) , submission-form : o ( p ( 'l0 , 0 ) , 2 ) , name : author1 > & none ) , mode : active , hops : 0 , gas : 41 , p : p ( 'l0 , 1 ) > < o ( p ( 'l0 , 1 ) , 1 ) : MO | hidden-gas : 0 , mod : up ( PROGRAM-COMMITTEE-MEMBER ) , s : up ( PROGRAM-COMMITTEE-MEMBER , < o ( p ( 'l0 , 1 ) , 1 ) : PCMember | hidden-gas : 45 , paper : null , submission-form : null , name : pc-member1 , done : ( p1 . p2 . p3 . p4 ) , subreviewers : o ( p ( 'l0 , 0 ) , 1 ) > & none ) , mode : active , hops : 0 , gas : 44 , p : p ( 'l0 , 1 ) > ) , forward : ( ( 0 , ( p ( 'l0 , 1 ) , 0 ) ) ( 1 , ( p ( 'l0 , 1 ) , 0 ) ) ) , guests : ( o ( p ( 'l0 , 1 ) , 0 ) . o ( p ( 'l0 , 1 ) , 1 ) ) , cnt : 3 > < p ( 'l1 , 0 ) : P | hidden-gas : 10 , cf : < o ( p ( 'l1 , 0 ) , 0 ) : MO | hidden-gas : 0 , mod : up ( AUTHOR ) , s : up ( AUTHOR , < o ( p ( 'l1 , 0 ) , 0 ) : Author | hidden-gas : 42 , paper : final-version ( p2 ) , submission-form : o ( p ( 'l0 , 0 ) , 3 ) , name : author2 > & none ) , mode : active , hops : 0 , gas : 41 , p : p ( 'l1 , 0 ) > , forward : ( 0 , ( p ( 'l1 , 0 ) , 0 ) ) , guests : o ( p ( 'l1 , 0 ) , 0 ) , cnt : 2 > < p ( 'l1 , 1 ) : P | hidden-gas : 10 , cf : ( < o ( p ( 'l1 , 1 ) , 0 ) : MO | hidden-gas : 0 , mod : up ( AUTHOR ) , s : up ( AUTHOR , < o ( p ( 'l1 , 1 ) , 0 ) : Author | hidden-gas : 40 , paper : rejected ( p3 ) , submission-form : o ( p ( 'l0 , 0 ) , 4 ) , name : author3 > & none ) , mode : active , hops : 0 , gas : 39 , p : p ( 'l1 , 1 ) > < o ( p ( 'l1 , 1 ) , 1 ) : MO | hidden-gas : 0 , mod : up ( PROGRAM-COMMITTEE-MEMBER ) , s : up ( PROGRAM-COMMITTEE-MEMBER , < o ( p ( 'l1 , 1 ) , 1 ) : PCMember | hidden-gas : 45 , paper : null , submission-form : null , name : pc-member2 , done : ( p1 . p2 . p3 . p4 ) , subreviewers : o ( p ( 'l2 , 1 ) , 1 ) > & none ) , mode : active , hops : 0 , gas : 44 , p : p ( 'l1 , 1 ) > ) , forward : ( ( 0 , ( p ( 'l1 , 1 ) , 0 ) ) ( 1 , ( p ( 'l1 , 1 ) , 0 ) ) ) , guests : ( o ( p ( 'l1 , 1 ) , 0 ) . o ( p ( 'l1 , 1 ) , 1 ) ) , cnt : 2 > < p ( 'l2 , 0 ) : P | hidden-gas : 10 , cf : < o ( p ( 'l2 , 0 ) , 0 ) : MO | hidden-gas : 0 , mod : up ( PROGR-CHAIR ) , s : up ( PROGR-CHAIR , < o ( p ( 'l2 , 0 ) , 0 ) : ProgrChair | hidden-gas : 97 , paper : null , submission-form : null , name : program-chair , done : ( p1 . p2 . p3 . p4 ) , subreviewers : ( o ( p ( 'l2 , 1 ) , 1 ) . o ( p ( 'l2 , 2 ) , 0 ) ) , proceedings : mt , accepted : mt , submissions : mt , committee-members : ( o ( p ( 'l0 , 1 ) , 1 ) . o ( p ( 'l1 , 1 ) , 1 ) . o ( p ( 'l2 , 0 ) , 0 ) ) , conference-chair : o ( p ( 'l0 , 0 ) , 0 ) , number-of-reviewers : 3 > & none ) , mode : active , hops : 0 , gas : 96 , p : p ( 'l2 , 0 ) > , forward : ( 0 , ( p ( 'l2 , 0 ) , 0 ) ) , guests : o ( p ( 'l2 , 0 ) , 0 ) , cnt : 17 > < p ( 'l2 , 1 ) : P | hidden-gas : 10 , cf : ( < o ( p ( 'l2 , 1 ) , 0 ) : MO | hidden-gas : 0 , mod : up ( AUTHOR ) , s : up ( AUTHOR , < o ( p ( 'l2 , 1 ) , 0 ) : Author | hidden-gas : 42 , paper : final-version ( p4 ) , submission-form : o ( p ( 'l0 , 0 ) , 5 ) , name : author4 > & none ) , mode : active , hops : 0 , gas : 41 , p : p ( 'l2 , 1 ) > < o ( p ( 'l2 , 1 ) , 1 ) : MO | hidden-gas : 0 , mod : up ( REVIEWER ) , s : up ( REVIEWER , < o ( p ( 'l2 , 1 ) , 1 ) : Reviewer | hidden-gas : 41 , paper : null , submission-form : null , name : reviewer2 , done : p2 , subreviewers : o ( p ( 'l2 , 2 ) , 0 ) > & none ) , mode : active , hops : 0 , gas : 40 , p : p ( 'l2 , 1 ) > ) , forward : ( ( 0 , ( p ( 'l2 , 1 ) , 0 ) ) ( 1 , ( p ( 'l2 , 1 ) , 0 ) ) ) , guests : ( o ( p ( 'l2 , 1 ) , 0 ) . o ( p ( 'l2 , 1 ) , 1 ) ) , cnt : 3 > < p ( 'l2 , 2 ) : P | hidden-gas : 10 , cf : < o ( p ( 'l2 , 2 ) , 0 ) : MO | hidden-gas : 0 , mod : up ( REVIEWER ) , s : up ( REVIEWER , < o ( p ( 'l2 , 2 ) , 0 ) : Reviewer | hidden-gas : 33 , paper : null , submission-form : null , name : reviewer3 , done : p2 , subreviewers : mt > & none ) , mode : active , hops : 0 , gas : 32 , p : p ( 'l2 , 2 ) > , forward : ( 0 , ( p ( 'l2 , 1 ) , 0 ) ) , guests : o ( p ( 'l2 , 2 ) , 0 ) , cnt : 1 > ) ***(% \end{verbatim} \normalsize %)