task3.ispl

---Environment agent
Agent Environment

    Obsvars:
        reached: BOOLEAN;
    k: 2..3;
    END Obsvars

    Vars:
        state: {idle, detected, initiated, completed};
    END Vars

    Actions = {NONE, task_detected_, task_initiated_, task_completed_};

    Protocol:
        state = idle: {task_detected_};
        state = detected: {task_initiated_};
        state = completed: {task_completed_};
    END Protocol

    Evolution:
        reached = TRUE IF
            ((k = 2) AND
                ((Robot1.Action=received_confirm) OR (Robot2.Action=received_confirm) OR (Robot3.Action=received_confirm))) OR
            ((k = 3) AND
                ((Robot1.Action=received_confirm) AND (Robot2.Action=received_confirm)) OR
        ((Robot1.Action=received_confirm) AND (Robot3.Action=received_confirm)) OR
        ((Robot2.Action=received_confirm) AND (Robot3.Action=received_confirm)));

        state = detected IF ((state = idle) AND ((Robot1.Action = task_detected) OR (Robot2.Action = task_detected) OR (Robot3.Action = task_detected)))
            AND (Action=task_detected_);

        state = initiated IF (state = detected) AND (reached=TRUE) AND (Action=task_initiated_);

        state = completed IF (Action=task_completed_) AND
      (((k = 2) AND (
        ((Robot1.Action=task_completed) AND (Robot2.Action=task_completed)) OR
        ((Robot1.Action=task_completed) AND (Robot3.Action=task_completed)) OR
        ((Robot2.Action=task_completed) AND (Robot3.Action=task_completed))
      )) OR ((k = 3) AND
        ((Robot1.Action=task_completed) AND (Robot2.Action=task_completed) AND (Robot3.Action=task_completed))
      ));
    END Evolution
END Agent


---Robot1
Agent Robot1

    Vars:
        state: {idle, busy, ready, promised};
    END Vars

    Actions = {task_detected, send_confirm, send_request, send_willing, received_request, received_willing, received_engaged, received_confirm, received_not_required, task_completed};

    Protocol:
        state = idle: {task_detected, received_request};
        state = ready: {send_request, send_confirm, received_willing, received_engaged};
        state = busy: {task_completed};
        state = promised: {received_confirm, received_not_required, send_willing};
    END Protocol

    Evolution:
        state = idle IF ((state = idle) AND (Action = task_detected) AND ((Robot2.Action = task_detected) OR (Robot3.Action = task_detected))) OR
                ((state = busy) AND (Action = task_completed) AND (
            ((Environment.k = 2) AND ((Robot2.Action = task_completed) OR (Robot3.Action = task_completed))) OR
            ((Environment.k = 3) AND ((Robot2.Action = task_completed) AND (Robot3.Action = task_completed))))) OR
                ((state= promised) AND (Action=received_not_required));

        state = ready IF ((state = idle) AND (Action = task_detected) AND (
            ((Environment.k = 2) AND ((Robot2.Action = received_request) OR (Robot3.Action = received_request))) OR
            ((Environment.k = 3) AND ((Robot2.Action = received_request) AND (Robot3.Action = received_request))))) OR
                ((state=ready) AND ((Action = received_willing) OR (Action = received_engaged)));

        state = busy IF ((state = ready) AND (Action = send_confirm)) OR
                ((state = promised) AND (Action=received_confirm));

        state = promised IF ((state = idle) AND (Action=received_request) AND (Robot2.Action=send_request)) OR
               ((state = promised) AND (Action=send_willing) AND (Robot2.Action=received_willing)) OR
         ((state = idle) AND (Action=received_request) AND (Robot3.Action=send_request)) OR
               ((state = promised) AND (Action=send_willing) AND (Robot3.Action=received_willing));
   END Evolution
END Agent


---Robot2
Agent Robot2

    Vars:
        state: {idle, busy, ready, promised};
    END Vars

    Actions = {task_detected, send_confirm, send_request, send_willing, received_request, received_willing, received_engaged, received_confirm, received_not_required, task_completed};

    Protocol:
        state = idle: {task_detected, received_request};
        state = ready: {send_request, send_confirm, received_willing, received_engaged};
        state = busy: {task_completed};
        state = promised: {received_confirm, received_not_required, send_willing};
    END Protocol

    Evolution:
        state = idle IF ((state = idle) AND (Action = task_detected) AND ((Robot1.Action = task_detected) OR (Robot3.Action = task_detected))) OR
                ((state = busy) AND (Action = task_completed) AND (
            ((Environment.k = 2) AND ((Robot1.Action = task_completed) OR (Robot3.Action = task_completed))) OR
            ((Environment.k = 3) AND ((Robot1.Action = task_completed) AND (Robot3.Action = task_completed))))) OR
                ((state= promised) AND (Action=received_not_required));

        state = ready IF ((state = idle) AND (Action = task_detected) AND (
            ((Environment.k = 2) AND ((Robot1.Action = received_request) OR (Robot3.Action = received_request))) OR
            ((Environment.k = 3) AND ((Robot1.Action = received_request) AND (Robot3.Action = received_request))))) OR
                ((state=ready) AND ((Action = received_willing) OR (Action = received_engaged)));

        state = busy IF ((state = ready) AND (Action = send_confirm)) OR
                ((state = promised) AND (Action=received_confirm));

        state = promised IF ((state = idle) AND (Action=received_request) AND (Robot1.Action=send_request)) OR
               ((state = promised) AND (Action=send_willing) AND (Robot1.Action=received_willing)) OR
         ((state = idle) AND (Action=received_request) AND (Robot3.Action=send_request)) OR
               ((state = promised) AND (Action=send_willing) AND (Robot3.Action=received_willing));
   END Evolution
END Agent


---Robot3
Agent Robot3

    Vars:
        state: {idle, busy, ready, promised};
    END Vars

    Actions = {task_detected, send_confirm, send_request, send_willing, received_request, received_willing, received_engaged, received_confirm, received_not_required, task_completed};

    Protocol:
        state = idle: {task_detected, received_request};
        state = ready: {send_request, send_confirm, received_willing, received_engaged};
        state = busy: {task_completed};
        state = promised: {received_confirm, received_not_required, send_willing};
    END Protocol

    Evolution:
        state = idle IF ((state = idle) AND (Action = task_detected) AND ((Robot1.Action = task_detected) OR (Robot2.Action = task_detected))) OR
                ((state = busy) AND (Action = task_completed) AND (
            ((Environment.k = 2) AND ((Robot1.Action = task_completed) OR (Robot2.Action = task_completed))) OR
            ((Environment.k = 3) AND ((Robot1.Action = task_completed) AND (Robot2.Action = task_completed))))) OR
                ((state= promised) AND (Action=received_not_required));

        state = ready IF ((state = idle) AND (Action = task_detected) AND (
            ((Environment.k = 2) AND ((Robot1.Action = received_request) OR (Robot2.Action = received_request))) OR
            ((Environment.k = 3) AND ((Robot1.Action = received_request) AND (Robot2.Action = received_request))))) OR
                ((state=ready) AND ((Action = received_willing) OR (Action = received_engaged)));

        state = busy IF ((state = ready) AND (Action = send_confirm)) OR
                ((state = promised) AND (Action=received_confirm));

        state = promised IF ((state = idle) AND (Action=received_request) AND (Robot1.Action=send_request)) OR
               ((state = promised) AND (Action=send_willing) AND (Robot1.Action=received_willing)) OR
         ((state = idle) AND (Action=received_request) AND (Robot2.Action=send_request)) OR
               ((state = promised) AND (Action=send_willing) AND (Robot2.Action=received_willing));
   END Evolution
END Agent


Evaluation
      ready_var IF ( (Robot1.state=ready) OR (Robot2.state=ready) OR (Robot3.state=ready) );

        bad_condition IF (
                 ((Robot1.state=promised) AND (Robot2.state=idle) AND (Robot3.state=idle)) OR
                 ((Robot1.state=idle) AND (Robot2.state=promised) AND (Robot3.state=idle)) OR
                 ((Robot1.state=idle) AND (Robot2.state=idle) AND (Robot3.state=promised)));
END Evaluation


InitStates
    (Robot1.state = idle) AND
    (Robot2.state = idle) AND
    (Robot3.state = idle) AND
    (Environment.reached=FALSE) AND (Environment.state=idle);
END InitStates


Fairness
  ready_var;
END Fairness


Formulae
    AG(!bad_condition);
END Formulae