extern string $''$;

interface iprocess
{
  in void spawn(string model, string args);
  in void kill();
  in void stdin(string data);
  in void end();

  out void stdout(string data);
  out void stderr(string data);
  out void close();

  behaviour
  {
    enum State {Idle, Waiting, Running, Finishing};
    State state = State.Idle;

    bool pending = false;

    [state.Idle]
    {
      on spawn: state = State.Waiting;
      on kill: {}
      on stdin: illegal;
      on end: illegal;
    }
    [state.Waiting]
    {
      on spawn: illegal;
      on kill: state = State.Idle;
      on stdin: {state = State.Running; pending = true;}
      on end: illegal;
      on optional: {state = State.Idle; close;}
    }
    [state.Running]
    {
      on spawn: illegal;
      on kill: state = State.Idle;
      on stdin: pending = true;
      on end: state = State.Finishing;

      [pending]
      {
        on optional: stderr;
        on inevitable: stdout;
        on inevitable: {pending = false; stdout;}
      }
      [!pending]
      {
        on inevitable: {state = State.Idle; close;}
      }
    }
    [state.Finishing]
    {
      on spawn: illegal;
      on kill: state = State.Idle;
      on stdin: illegal;
      on end: illegal;

      [pending]
      {
        on optional: stderr;
        on inevitable: {pending = false; stdout;}
      }
      [!pending]
      {
        on inevitable: {state = State.Idle; close;}
      }
    }
  }
}

interface imodelchecker
{
  in void process(string data);

  out void error();
  out void pass(string data);
  out void fail(string data);

  behaviour
  {
    on process: {}
    on process: {error;}
    on process: {pass;}
    on process: {fail;}
    on process: {pass; fail;}
  }
}

interface irequest
{
  in void execute(string model, string args);
  in void cancel();

  out void error(string data);
  out void progress(string data);
  out void result(string data);

  behaviour
  {
    enum State {Idle, Running};
    State state = State.Idle;
    [state.Idle]
    {
      on execute: state = State.Running;
      on cancel: {}
    }
    [state.Running]
    {
      on execute: illegal;
      on cancel: state = State.Idle;
      on optional: {progress;}
      on optional: {state = State.Idle; error;}
      on optional: {state = State.Idle; progress; error;}
      on inevitable: {state = State.Idle; result;}
    }
  }
}

interface ififo
{
  enum Result {OK,NOK};
  in Result put(string data);
  in Result get(out string data);

  behaviour
  {
    on put: {reply(Result.OK);}
    on put: {reply(Result.NOK);}
    on get: {reply(Result.OK);}
    on get: {reply(Result.NOK);}
  }
}

component verify
{
  provides irequest port;

  requires iprocess parsing;
  requires iprocess generation;
  requires iprocess verification;
  requires iprocess simulation;
  requires ififo buffer;
  requires imodelchecker modelchecking;

  behaviour
  {
    enum State {Idle, Running};
    State state = State.Idle;

    bool p = false;
    bool g = false;
    bool v = false;
    bool s = false;

    string model_ = $''$;
    string args_ = $''$;
    string result_ = $''$;

    void start(string model, string args)
    {
      model_ = model;
      args_ = args;

      state = State.Running;
      parsing.spawn($''$,args); p = true;
      generation.spawn($''$,args); g = true;
      verification.spawn($''$,$''$); v = true;
      parsing.stdin(model);
      parsing.end();
    }
    void finish()
    {
      state = State.Idle;
      parsing.kill(); p = false;
      generation.kill(); g = false;
      verification.kill(); v = false;
      simulation.kill(); s = false;
    }
    void simulate(string data)
    {
      s = true;
      simulation.spawn(data,args_);
      simulation.stdin(model_);
      simulation.end();
    }
    void result()
    {
      port.result(result_);
      result_ = $''$;
    }
    void progress()
    {
      port.progress(result_);
      result_ = $''$;
    }
    [state.Idle]
    {
      on port.execute(model, args): start(model, args);
      on port.cancel(): {}

      on parsing.stderr, parsing.stdout, parsing.close: illegal;
      on generation.stderr, generation.stdout, generation.close: illegal;
      on verification.stderr, verification.stdout, verification.close: illegal;
      on simulation.stderr, simulation.stdout, simulation.close: illegal;
      on modelchecking.error, modelchecking.pass, modelchecking.fail: illegal;
    }
    [state.Running]
    {
      on port.execute: illegal;
      on port.cancel(): finish();

      on parsing.stderr(data): {finish(); port.error(data);}
      on parsing.stdout(data): generation.stdin(data);
      on parsing.close(): {p = false; generation.end();}

      on generation.stderr(data): {finish(); port.error(data);}
      on generation.stdout(data): if(v) {verification.stdin(data);}
      on generation.close(): {g = false; if(p || !v) {finish(); port.error($'{"type":"error","error":"generator error"}'$);} else {verification.end();}}

      on verification.stderr(data): {finish(); port.error(data);}
      on verification.stdout(data): {modelchecking.process(data);}
      on verification.close(): {
        v = false;
        if(!s) {
          string data; ififo.Result r = buffer.get(data);
          if(r.OK){port.progress(result_); simulate(data);}
          else {
            result();
            finish();
          }
        }
      }

      on modelchecking.error(): {finish(); port.error($'{"type":"error","error":"modelchecker error"}'$);}
      on modelchecking.pass(data): {port.progress(data);}
      on modelchecking.fail(data): {
        if(s){ififo.Result r = buffer.put(data); if(r.NOK) {finish(); port.error($'{"type":"error","error":"modelchecker error"}'$);}}
        else {simulate(data);}
      }

      on simulation.stderr(data): {finish(); port.error(data);}
      on simulation.stdout(data): {result_ = $this.result_ + data$;}
      on simulation.close(): {
        string data; ififo.Result r = buffer.get(data);
        s = false;
        if(r.OK){progress(); simulate(data);}
        else {
          if(v) {progress();}
          else {
            result();
            finish();
          }
        }
      }
    }
  }
}