#include <systemc>

// Files to be included by the user's request


// Monitor parameters:
//	 LTL forumula: G p


// The SPIN version of the automaton: 

//never {
//accept_init: /* <p:1>, SCC 1 */
//  if
//  :: (p) -> goto accept_S2
//  fi;
//accept_S2: /* T, SCC 2 */
//  if
//  :: (p) -> goto accept_S2
//  fi;
//}
//


class test_monitor0 : public sc_core::mon_prototype {
public: 
  /* The constructor */
  /// <param name="obs">This is a pointer to the observer object that is driving this monitor.
  /// We need it when we integrate this monitor object with SystemC. Later, the observer will be sending
  /// the monitor notifications when a new input needs to be processed. </param>
  test_monitor0(mon_observer* obs) : sc_core::mon_prototype() {

    /// Here we initialize the set of reachable states.
    next_state = new bool[3];

    /// The initial state is the only one reachable at the beginning...
    next_state[0] = 1;

    /// ... everybody else is unreachable
    for (int i = 1; i < 3; i++) {
      next_state[i] = 0;
    }

    // In a moment we will swap current_state and next_state
    current_state = new bool[3];
    for (int i = 0; i < 3; i++) {
      current_state[i] = 0;
    }

    /// Local variable, we need it later for some function calls
    observer = obs;

    /// Status is undetermined, neither FAIL nor PASS. We have not seen enough of the
    /// trace to make a decision if this property holds or not
    status = MON_UNDETERMINED;

    /// Here we tell the observer when to call us to process input. This way the monitor
    /// doesn't process every single burp of the SystemC program, but instead it only
    /// processes the ones that are relevant to the property we are monitoring. 
    observer->register_monitor(this, MON_INIT_PHASE_BEGIN);
    observer->register_monitor(this, MON_INIT_PHASE_BEGIN);
    observer->register_monitor(this, MON_INIT_PHASE_END);
    observer->register_monitor(this, MON_INIT_UPDATE_PHASE_BEGIN);
    observer->register_monitor(this, MON_INIT_UPDATE_PHASE_END);
    observer->register_monitor(this, MON_INIT_DELTA_NOTIFY_PHASE_BEGIN);
    observer->register_monitor(this, MON_INIT_DELTA_NOTIFY_PHASE_END);
    observer->register_monitor(this, MON_DELTA_CYCLE_BEGIN);
    observer->register_monitor(this, MON_DELTA_CYCLE_END);
    observer->register_monitor(this, MON_EVALUATION_PHASE_BEGIN);
    observer->register_monitor(this, MON_EVALUATION_PHASE_END);
    observer->register_monitor(this, MON_UPDATE_PHASE_BEGIN);
    observer->register_monitor(this, MON_UPDATE_PHASE_END);
    observer->register_monitor(this, MON_DELTA_NOTIFY_PHASE_BEGIN);
    observer->register_monitor(this, MON_DELTA_NOTIFY_PHASE_END);
    observer->register_monitor(this, MON_TIMED_NOTIFY_PHASE_BEGIN);
    observer->register_monitor(this, MON_TIMED_NOTIFY_PHASE_END);
    observer->register_monitor(this, MON_METHOD_SUSPEND);
    observer->register_monitor(this, MON_THREAD_SUSPEND);
  } // Constructor

  /**
   * Simulating a step of the monitor.
   */
  /// This function is called from the callbacks (see below). The observer, which lives in the
  /// SystemC kernel, calls the monitor's callbacks when the observer observes something relevant to
  /// this monitor's property. We just told the observer what is relevant, so the observer just
  /// follows the register_monitor() instructions we submitted above. 
  void step() {
    if (status == MON_UNDETERMINED) {

      /// If the property either FAILs or PASSes, we avoid doing the work below, since once the
      /// property FAILs it remains FAILed. Same for PASSed properties.

      /// Here we do the swap of current_state and next_state
      delete[] current_state;
      current_state = next_state;

      /// Next state is currently empty (no reachable states in the next step). This is about to change
      /// as we process the transitions that are enabled by the state of the SystemC model at this instance.
      next_state = new bool[3];
      for (int i = 0; i < 3; i++) {
        next_state[i] = 0;
      }

      
      /// One by one, we process each state that is currently reachable
      for (int i = 0; i < 3; i++) {
        if (current_state[i]) {
	  /// This state currently reachable, so lets see what other states are reachable from here....
#ifdef MONITOR_DEBUG
	  /// Status update for those curious engineers who are tracing the execution
	  /// of the monitor
          std::cout << "Current microstate: " << i << std::endl;
#endif

	  /// Depending on what is the current_state[] and the value of the monitored variable ($p$),
	  /// we may make some state reachable in next_state[].
          switch ( i ) {
            case 0: /* <p:1>, SCC 1 */
              if((p)  )
                next_state[2] = 1;
              break;
            case 2: /* T, SCC 2 */
              if((p)  )
                next_state[2] = 1;
              break;
            default:
	      /// This is unreachable, but it is better to be safe, and warn the user
	      /// in case something got messed up upstream.
              std::cerr << "Reached unknown state in test_monitor0" << std::endl;
              std::cerr << "The state is " << i << std::endl;
              exit(99);
          } // switch
        } // if (...)
      } // for(...)

      // Check if we are stuck... unless we already satisfied the property
      bool not_stuck = (status == MON_PASS);
      for (int i = 0; i < 3; i++) {
        not_stuck = not_stuck || next_state[i];
      }

      if (! not_stuck) {
        property_failed();
      }
    } // if (status == MON_UNDETERMINED)
#ifdef MONITOR_DEBUG
    else {
      std::cout << "test_monitor0: property has already been determined to "
		<< std::string((status == MON_PASS)? "hold" : "fail") << std::endl;
    }
#endif
  } // step()


  /// Callback functions for the observer to call while running with the SystemC code.
  /// This is what drives the monitor forward.
  virtual void callback_init_phase_begin() {
    step();
  }

  virtual void callback_init_phase_end() {
    step();
  }

  virtual void callback_init_update_phase_begin() {
    step();
  }

  virtual void callback_init_update_phase_end() {
    step();
  }

  virtual void callback_init_delta_notify_phase_begin() {
    step();
  }

  virtual void callback_init_delta_notify_phase_end() {
    step();
  }

  virtual void callback_delta_cycle_begin() {
    step();
  }

  virtual void callback_delta_cycle_end() {
    step();
  }

  virtual void callback_evaluation_phase_begin() {
    step();
  }

  virtual void callback_evaluation_phase_end() {
    step();
  }

  virtual void callback_update_phase_begin() {
    step();
  }

  virtual void callback_update_phase_end() {
    step();
  }

  virtual void callback_delta_notify_phase_begin() {
    step();
  }

  virtual void callback_delta_notify_phase_end() {
    step();
  }

  virtual void callback_timed_notify_phase_begin() {
    step();
  }

  virtual void callback_timed_notify_phase_end() {
    step();
  }

  virtual void callback_method_suspend() {
    step();
  }

  virtual void callback_thread_suspend() {
    step();
  }

  /// In case the monitor fails, we make sure that step() will not do any expensive computations
  /// by setting the status to FAIL
  void property_failed() {
    std::cout << "The property " << to_string() << "FAILED" << std::endl;
    SC_REPORT_WARNING("Property failed", "Monitor for property G p @ DEFAULT_CLOCK has reached an error state");
    status = MON_FAIL;
  }

  /// Same for the cases when the property is satisified and does not need to be evaluated further.
  void property_satisfied() {
#ifdef MONITOR_DEBUG
    std::cout << "The property " << to_string() << "HOLDS" << std::endl;
#endif
    status = MON_PASS;
  }

  /// Some public utility function for interacting with this monitor from the outside.
  const char* to_string() const {
    return "G p @ DEFAULT_CLOCK";
  }

  const mon_status_t get_status() const {
    return status;
  }

private: 
  bool* current_state;
  bool* next_state;
  mon_observer* observer;
  mon_status_t status;
}; // class


/// End of monitor, the rest is the definition of the object that will sit in SystemC's kernel and
/// drive all monitors from there. Each monitor is passed a reference to this object. The local_observer
/// is instantiated by the SystemC code during elaboration.



/**
 * This object is derived from mon_observer defined in the SystemC
 * modified kernel. Thus, we can pass it as an argument to the classes
 * implementing the monitors.
 */
class local_observer : public mon_observer {

 public:

  // The constructor
  local_observer(unsigned int verbosity, int num_monitors) : mon_observer(verbosity) {

    /// Instantiate all monitors (in this case, there is only one monitor)
    test_monitor0* test_monitor0_inst;
    for (int i=0; i<num_monitors; i++) {
      test_monitor0_inst = new test_monitor0(this);
      mons.push_back(test_monitor0_inst);
    } //for loop

  } // constructor


  /**
   * Report the status of each monitor. Output to @os
   */
  void report_status(std::ostream& os) {
    mon_status_t status = MON_FAIL;
    os << "Monitor Status Report" << std::endl;

    for (vect_mon_t::const_iterator it = mons.begin();
         it != mons.end();
         it++)
      {
        status = (*it)->get_status();
        os << "Monitor \t" << (*it)->to_string() << std::endl;
        os << "Status: \t" << ((status == MON_FAIL)? "FAILED" : (status == MON_PASS) ? "HOLDS" : "UNDETERMINED (DID NOT FAIL)") << std::endl << std::endl;

      }
  } // report_status
}; // class local_observer