/*************************************************************************
 *
 *
 * Copyright 2022 Ole Richter - University of Groningen
 * Copyright 2022 Michele Mastella - University of Groningen
 *
 *  This program is free software; you can redistribute it and/or
 *  modify it under the terms of the GNU General Public License
 *  as published by the Free Software Foundation; either version 2
 *  of the License, or (at your option) any later version.
 *
 *  This program is distributed in the hope that it will be useful,
 *  but WITHOUT ANY WARRANTY; without even the implied warranty of
 *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 *  GNU General Public License for more details.
 *
 *  You should have received a copy of the GNU General Public License
 *  along with this program; if not, write to the Free Software
 *  Foundation, Inc., 51 Franklin Street, Fifth Floor,
 *  Boston, MA  02110-1301, USA.
 *
 **************************************************************************
 */


namespace sim{
  namespace test_bench_lib {

function finit (int verbose) : int;
function fsource_next(int id; int sim_step) : int;
function fsource_get(int id; int bit_width) : int;
function fcheck_next(int id; int sim_step) : int;
function fcheck_in_order(int id; int data) : int;
function fcheck_out_of_order(int id; int data) : int;
function fdump_to_file(int id; int sim_step; int data) : int;
function fcontrol_next(int dontcare) : int;
function fcontrol_get(int dontcare) : int;
function fcontrol_wait(int dontcare) : int;


export template<pint BIT_WIDTH;pint ID; pint VERBOSE>
defproc channel_source(chan!(int<BIT_WIDTH>) out; chan?(int) sim_step; chan!(int<1>) done)
{
  int current_step, t,data;
  chp {
   *[ sim_step?current_step; t := 1;
    *[ t = 1 -> t := fsource_next(ID,current_step);
      [ t = 1 -> data := fsource_get(ID,BIT_WIDTH); out!data ; 
      [   VERBOSE >= 1 -> log("send ", data, " on source ", ID) 
      []  else -> skip
      ]      
      [] else -> done!1
      ]
    ]
   ]
  }
}

export template<pint BIT_WIDTH;pint ID>
defproc channel_checker_in_order(chan?(int<BIT_WIDTH>) in; chan?(int) sim_step; chan!(int<1>) done)
{
  int current_step, t, check, data;
  chp {
   *[ sim_step?current_step; t := 1;
    *[ t = 1 -> t := fcheck_next(ID,current_step);
      [ t = 1 -> in?data; check := fcheck_in_order(ID,data); 
        [check = 1 -> log("[success] got ",data, " on check ", ID)
        [] else ->  log("[failure] got wrong ",data, " on check ", ID, " see log")
        ]
      [] else -> done!1
      ]
    ]
   ]
  }
}

export template<pint BIT_WIDTH;pint ID>
defproc channel_checker_out_of_order(chan?(int<BIT_WIDTH>) in; chan?(int) sim_step; chan!(int<1>) done)
{
  int current_step, t, check, data;
  chp {
   *[ sim_step?current_step; t := 1;
    *[ t = 1 -> t := fcheck_next(ID,current_step);
      [ t = 1 -> in?data; check := fcheck_out_of_order(ID,data); 
        [check = 1 -> log("[success] got ",data, " on check ", ID)
        [] else ->  log("[failure] got wrong ",data, " on check ", ID, " see log")
        ]
      [] else -> done!1
      ]
    ]
   ]
  }
}

export template<pint BIT_WIDTH;pint ID>
defproc channel_dump(chan?(int<BIT_WIDTH>) in; chan?(int) sim_step)
{
  int current_step, t,in_tmp;
  chp {

   *[ [| #sim_step -> sim_step?current_step
      [] #in -> in?in_tmp; log("Dumping a spike"); t:=fdump_to_file(ID,current_step,in_tmp);log("Dumped a spike") //here should be non-deterministic but it doesn't work
      |];
      log("Waiting for next. sim_step: " ,#sim_step,", in: ",#in)
    ]
  }
}

defproc channel_dump_dummy(chan?(int) sim_step)
{
  chp {
    *[ sim_step? ]
  }
}

defproc channel_source_dummy(chan?(int) sim_step; chan!(int<1>) done)
{
  chp {
    *[ sim_step?;done!1 ]
  }
}

defproc channel_checker_dummy(chan?(int) sim_step; chan!(int<1>) done)
{
  chp {
    *[ sim_step?;done!1 ]
  }
}

export template<pint NUMBER_SOURCE,NUMBER_CHECKER,NUMBER_DUMP;pbool HALT_ON_FALIURE>
defproc control(chan(int) sim_step_source[NUMBER_SOURCE+1]; chan(int) sim_step_checker[NUMBER_CHECKER+1]; chan(int) sim_step_dump[NUMBER_DUMP+1]; chan?(int<1>) done_source[NUMBER_SOURCE+1]; chan?(int<1>) done_checker[NUMBER_CHECKER+1])
{
  int current_step, wait;
  int<1> t, success, failure_free;

  //This is a workaround to permit to have 0 instances of a type.
  channel_checker_dummy dummy1(.sim_step=sim_step_checker[NUMBER_CHECKER],.done=done_checker[NUMBER_CHECKER]);
  channel_source_dummy dummy2(.sim_step=sim_step_source[NUMBER_SOURCE],.done=done_source[NUMBER_SOURCE]);
    channel_dump_dummy dummy3(.sim_step=sim_step_dump[NUMBER_DUMP]);
    
  chp {
    log("I entered control");

    t:=finit(1);
    failure_free:=1;
    *[ t = 1 -> current_step := fcontrol_get(0);
        log("I entered the t loop at current step:",current_step);
      [ current_step = 0 -> skip // reset here
      [] else ->
        (,j:0..NUMBER_SOURCE: sim_step_source[j]!current_step),
        (,j:0..NUMBER_CHECKER: sim_step_checker[j]!current_step),
        (,j:0..NUMBER_DUMP: sim_step_dump[j]!current_step); 
        (;j:0..NUMBER_SOURCE: done_source[j]?success; failure_free := failure_free & success);
        (;j:0..NUMBER_CHECKER: done_checker[j]?success; failure_free := failure_free & success)
      ];
      wait := fcontrol_wait(0);
      [ wait > 0 -> skip // exec cycle
      [] else -> skip
      ];
      [ HALT_ON_FALIURE & 0=failure_free -> t := 0; log("stopped testbech because of failure")
      [] else -> t:=fcontrol_next(0);
        log("I finished the t loop at current step:",current_step)
      ]
    ];
    log("I finished the program")
  }
}
}
}