

***(%
\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

%)
