Skip to content
Browse files

Added traces to simulation, very inefficient

  • Loading branch information...
1 parent ccf6a3e commit 17f276bc4c8a4155797ca8879cfee78e9c92d2ce @mwolf76 committed Dec 31, 2012
Showing with 13 additions and 12 deletions.
  1. +1 −1 src/algorithms/sim/Makefile.am
  2. +7 −10 src/algorithms/sim/simulation.cc
  3. +5 −1 src/algorithms/sim/simulation.hh
View
2 src/algorithms/sim/Makefile.am
@@ -18,7 +18,7 @@ AM_CPPFLAGS=@AM_CPPFLAGS@
AM_CXXFLAGS=@AM_CXXFLAGS@
PKG_HH = simulation.hh
-PKG_CC = simulation.cc
+PKG_CC = simulation.cc witness.cc
PKG_SOURCES = $(PKG_H) $(PKG_CC)
View
17 src/algorithms/sim/simulation.cc
@@ -33,7 +33,7 @@ Simulation::Simulation(IModel& model, int resume,
, f_nsteps(nsteps)
, f_constraints(constraints)
{
- /* internal structures are empty */
+ /* internal structures are empty */
assert( 0 == f_init_adds.size() );
assert( 0 == f_trans_adds.size() );
@@ -70,9 +70,6 @@ Simulation::Simulation(IModel& model, int resume,
Simulation::~Simulation()
{}
-simulation_status_t Simulation::status() const
-{ return f_status; }
-
void Simulation::set_status(simulation_status_t status)
{ f_status = status; }
@@ -89,7 +86,12 @@ void Simulation::process()
do {
assert_fsm_trans(k); ++ k;
TRACE << "Simulating step " << k << endl;
- } while (STATUS_SAT == engine().solve() && ! leave);
+
+ if (STATUS_SAT == engine().solve()) {
+ ostringstream oss; oss << "Simulation";
+ SimulationWitness witness(model(), engine(), k);
+ }
+ } while (STATUS_SAT == engine().status() && ! leave);
if (STATUS_SAT == engine().status()) {
@@ -98,11 +100,6 @@ void Simulation::process()
set_status( SIMULATION_SAT );
- // /* CEX extraction */
- // ostringstream oss; oss << "CEX for '" << f_property << "'";
- // Witness& witness = * new SimulationWitness(f_property, model(),
- // engine(), k, false);
-
// TODO: register
}
View
6 src/algorithms/sim/simulation.hh
@@ -46,7 +46,11 @@ public:
void process();
- simulation_status_t status() const;
+ inline simulation_status_t status() const
+ { return f_status; }
+
+ inline IModel& model()
+ { return f_model; }
private:
IModel& f_model;

0 comments on commit 17f276b

Please sign in to comment.
Something went wrong with that request. Please try again.