/* ============================================================================
 * D Y N I B E X - Example of a Signal Temporal Logic (STL) formula verification
 * ============================================================================
 * Copyright   : ENSTA
 * License     : This program can be distributed under the terms of the GNU LGPL.
 *               See the file COPYING.LESSER.
 *
 * Author(s)   : Joris Tillet
 * Created     : Feb 06, 2025
 * Sponsored   : This research benefited from the support of the CIEDS within the
 * STARTS Project.
 * ---------------------------------------------------------------------------- */

#include <map>
#include <list>
#include <iostream>
#include <stdexcept>

#include <ibex.h>

using namespace ibex;


int main(){

  const int n = 1;
  Variable y(n);

  // DYNAMICAL SYSTEM
  IntervalVector yinit(n);
  yinit[0] = Interval(-1.0,0.5);

  Function ydot = Function(y, Interval(1));
  ivp_ode problem = ivp_ode(ydot, 0.0, yinit);

  // SIMULATION
  simulation simu = simulation(&problem, 10, KUTTA3, 1e-8);

  std::cout << "Start simulation" << std::endl;
  simu.run_simulation();
  std::cout << "End simulation" << std::endl;


  // CHECK SATISFIABILITY OF PROPERTY
  float rho = 5.0;
  IntervalVector cstr1(n);
  cstr1[0] = Interval(NEG_INFINITY, rho);
  IntervalVector cstr2(n);
  cstr2[0] = Interval(rho, POS_INFINITY);
  BoolInterval result = until(simu, Interval(4.5,6), cstr1, cstr2);

  std::cout << "Result: " << result << std::endl;
//   //For an export in order to plot
//   simu.export2d_yn("export_2d.txt",0,1);
//   simu.generate_python_plot("python_plot.py",0,1);

  return 0;
}