___     __     ____ ____     ___ _____ 
   / \ \   / /__  / ___/ ___|   / _ \___ / 
  / _ \ \ / / _ \| |   \___ \  | | | ||_ \ 
 / ___ \ V / (_) | |___ ___) | | |_| |__) |
/_/   \_\_/ \___/ \____|____/   \___/____/ 
                                           

AVOCS'03
Model Checking Competition
Southampton, 2nd of April 2003

Rules of the Competition
========================
1. Have Fun
2. Don't cheat
3. Goto 1




Question 1) COUNTDOWN

You are given a sequence of numbers. You can combine 2 of these numbers
by applying either a multiplication, addition, or subtraction operation.
Doing so will remove the two numbers from the sequence and add the result
of the operation to the sequence.
Your goal is to reach a given target number by applying the above
operations.

For example, given  the initial list of numbers [ 1, 4, 10,23] 
and a goal number of 41 you can:

       multiply(4,10)
               ---giving-->  [1, 40,23]
       add(1,40)
               ---giving--> [41,23]
               
and you have reached the goal.


Tasks
 1. Write a generic model/specification/program for the task.
 
 2. Try to solve it for an initial list [11,9,8,7,6,5] and
     the goal 1234. (There is a solution.)

 3. Try to find a solution for the initial list
    [23,19,13,11,9,8,7,6,5] and the goal 123456.
    Or prove that there is no solution.
    
 4. [Bonus] If your model checker supports timing or probabilities, or both,
    can you find out more details about the solutions you have found
    in task 2? E.g., assume time for multiplication = 10 ms, time
    for addition = 4 ms, time for subtraction = 5 ms, assume every number
    can be chose with equal probability and every operation with equal
    probability.





Question 2) RING PROTOCOL

    |------------|                     |------------|
    |  Component |                     |  Component | 
    |------------|                     |------------|
    |          ID|                     |          ID|
/-> |   in-buffer|        /--------->  |   in-buffer|       /--------> ...
|   |  out-buffer|  -----/             |  out-buffer|  ----/
|   --------------                     --------------
|                                                                                 |
\---------------------------------------------------------------------------------/

A series of components are organised in a ring topology.
A component has an identifier and has two buffers: an in-buffer and an out-buffer.
The buffers can either be empty or contain a message.
A message is a pair composed of an identifier and a bit.

Behaviour of the components:
 - if the in-buffer is empty and the out-buffer of the previous component in
   the chain is non-empty then the contents of the out-buffer can be
   transferred into the component's in-buffer. The out-buffer of the other
   component becomes empty.
 - if the in-buffer is non-empty and contains a message to the component then
   it can read the message, after which the in-buffer becomes empty.
 - if the in-buffer is non-empty and contains a message for another component
   (id different from identifier of component) then it can copy the in-buffer
   into its own out-buffer, provided the out-buffer is empty.
 - if both the in-buffer and out-buffer are empty the component can put a
   message into its out-buffer.
   
Tasks
 1. Assuming components only send messages to themselves, can the system deadlock?
    The initial configuration is a ring of 3 components with all buffers empty.
    If too easy, try with 5 or 10 or more components. If too difficult assume all messages
    bits are 0.
 
 2. Assuming there is one component that can
    send any message (i.e., even identifiers that don't exist), can the system deadlock?
    Can the system reach a state where it is impossible to send or receive any new messages?
    
    Again, if too easy, try with 5 or 10 or more components.
    If too difficult assume all messages bits are 0.
   
3. [Bonus] For timed & probability model checkers: can you determine interesting
   timing and/or probability information about the system.
   
   [Bonus] For infinite state model checkers: Prove the properties from task 2 for any
   number of components.
   
   
   Have Fun,
   Michael Leuschel