Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Simulation bugfixes

  • Loading branch information...
commit 8cbd00cc335154901463c18f8ac04b21fd878157 1 parent 8ddd3e5
@mwolf76 authored
View
4 src/algorithms/Makefile.am
@@ -17,8 +17,8 @@ INCLUDES = -I$(top_srcdir)/src/ -I$(top_srcdir)/src/dd \
AM_CPPFLAGS=@AM_CPPFLAGS@
AM_CXXFLAGS=@AM_CXXFLAGS@
-PKG_HH = base.hh prepare.hh
-PKG_CC = base.cc prepare.cc
+PKG_HH = base.hh init.hh
+PKG_CC = base.cc init.cc
PKG_SOURCES = $(PKG_H) $(PKG_CC)
View
14 src/algorithms/prepare.cc → src/algorithms/init.cc
@@ -1,6 +1,6 @@
/**
- * @file prepare.cc
- * @brief Prepare algorithm
+ * @file init.cc
+ * @brief Init algorithm
*
* Copyright (C) 2012 Marco Pensallorto < marco AT pensallorto DOT gmail DOT com >
*
@@ -19,16 +19,16 @@
* Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
*
**/
-#include <prepare.hh>
+#include <init.hh>
-Prepare::Prepare(IModel& model)
+Init::Init(IModel& model)
: Algorithm(model)
{}
-Prepare::~Prepare()
+Init::~Init()
{}
-void Prepare::process()
+void Init::process()
{
clock_t t0 = clock(), t1;
double secs;
@@ -40,7 +40,7 @@ void Prepare::process()
compile();
t1 = clock(); secs = (double) (t1 - t0) / (double) CLOCKS_PER_SEC;
- os () << "-- preparation completed, took " << secs
+ os () << "-- initialization completed, took " << secs
<< " seconds" << endl;
}
View
14 src/algorithms/prepare.hh → src/algorithms/init.hh
@@ -1,6 +1,6 @@
/**
- * @file Prepare Algorithm.hh
- * @brief SAT Prepare Algorithm
+ * @file Init Algorithm.hh
+ * @brief SAT Init Algorithm
*
* This module contains definitions and services that implement an
* optimized storage for expressions. Expressions are stored in a
@@ -24,16 +24,16 @@
*
**/
-#ifndef PREPARE_ALGORITHM_H
-#define PREPARE_ALGORITHM_H
+#ifndef INIT_ALGORITHM_H
+#define INIT_ALGORITHM_H
#include <base.hh>
-class Prepare : public Algorithm {
+class Init : public Algorithm {
public:
- Prepare(IModel& model);
- ~Prepare();
+ Init(IModel& model);
+ ~Init();
void process();
};
View
129 src/algorithms/sim/simulation.cc
@@ -26,13 +26,23 @@
#include <sim/simulation.hh>
Simulation::Simulation(IModel& model,
- Expr_ptr halt_cond,
+ Expr_ptr condition,
Expr_ptr resume_id,
ExprVector& constraints)
: Algorithm(model)
- , f_halt_cond(halt_cond)
+ , f_halt_cond( NULL )
+ , f_nsteps( NULL )
, f_constraints(constraints)
- {
+{
+ ExprMgr& em (ExprMgr::INSTANCE());
+ if (NULL != condition) {
+ if (em.is_constant( condition)) {
+ f_nsteps = condition;
+ }
+ else {
+ f_halt_cond = condition;
+ }
+ }
if (resume_id) {
Witness& w = WitnessMgr::INSTANCE().witness( resume_id );
set_witness(w);
@@ -42,9 +52,6 @@ Simulation::Simulation(IModel& model,
Simulation::~Simulation()
{}
-void Simulation::set_status(simulation_status_t status)
-{ f_status = status; }
-
void Simulation::process()
{
clock_t t0 = clock(), t1;
@@ -60,11 +67,9 @@ void Simulation::process()
ExprMgr& em = ExprMgr::INSTANCE();
WitnessMgr& wm = WitnessMgr::INSTANCE();
- bool halt = false; sigint_caught = 0;
+ sigint_caught = 0;
step_t k = 0;
- set_status( SIMULATION_SAT ); // optimic assumption
-
// if a witness is already there, we're resuming a previous
// simulation. Hence, no need for initial states.
if (! has_witness()) {
@@ -96,73 +101,71 @@ void Simulation::process()
witness().extend(*w);
}
- /* HALT condition can either be:
- 1. a boolean formula; (halts when true)
- 2. a non-negative integer constant; (number of steps to be executed)
- 3. NULL (no halt condition)
- */
+ /* halt simulation? */
if (sigint_caught) {
- halt = true;
+ f_status = SIMULATION_INTERRUPTED;
+ return;
}
- else if (NULL != f_halt_cond) {
- if ( em.is_constant( f_halt_cond)) {
- halt = (0 == f_halt_cond->value());
- f_halt_cond = em.make_const( f_halt_cond->value() -1);
- }
- else {
- halt = wm.eval ( witness(), em.make_main(), f_halt_cond, k);
+ else if (NULL != f_halt_cond && wm.eval ( witness(),
+ em.make_main(),
+ f_halt_cond, k)) {
+ f_status = SIMULATION_HALTED;
+ return;
+ }
+ else if (NULL != f_nsteps) {
+ if (0 == f_nsteps->value()) {
+ f_status = SIMULATION_DONE;
+ return;
}
+ f_nsteps = em.make_const( f_nsteps->value() -1);
}
- if (!halt) {
- do {
- t1 = clock(); secs = (double) (t1 - t0) / (double) CLOCKS_PER_SEC;
- os () << "-- completed step " << 1 + k
- << ", took " << secs << " seconds"
- << endl;
- t0 = t1; // resetting clock
+ while (1) {
+ t1 = clock(); secs = (double) (t1 - t0) / (double) CLOCKS_PER_SEC;
+ os () << "-- completed step " << 1 + k
+ << ", took " << secs << " seconds"
+ << endl;
+ t0 = t1; // resetting clock
- assert_fsm_trans(k ++);
- assert_fsm_invar(k);
+ // one more cup of coffe for the road
+ // TODO: SAT restart after a number of steps
+ assert_fsm_trans(k ++);
+ assert_fsm_invar(k);
- if (STATUS_SAT == engine().solve()) {
- Witness_ptr w = new SimulationWitness( model(), engine(), k);
- witness().extend(*w);
+ if (STATUS_SAT == engine().solve()) {
+ Witness_ptr w = new SimulationWitness( model(), engine(), k);
+ witness().extend(*w);
- if (sigint_caught) {
- halt = true;
- }
- if (NULL != f_halt_cond) {
- if ( em.is_constant( f_halt_cond)) {
- halt = (0 == f_halt_cond->value());
- f_halt_cond = em.make_const( f_halt_cond->value() -1);
- }
- else {
- halt = wm.eval ( witness(), em.make_main(), f_halt_cond, k);
- }
+ if (sigint_caught) {
+ f_status = SIMULATION_INTERRUPTED;
+ return;
+ }
+ else if (NULL != f_halt_cond && wm.eval ( witness(),
+ em.make_main(),
+ f_halt_cond, k)) {
+ f_status = SIMULATION_HALTED;
+ return;
+ }
+ else if (NULL != f_nsteps) {
+ if (0 == f_nsteps->value()) {
+ f_status = SIMULATION_DONE;
+ return;
}
+ f_nsteps = em.make_const( f_nsteps->value() -1);
}
- } while (STATUS_SAT == engine().status() && ! halt);
- }
- else {
- TRACE << "Inconsistency detected in transition relation at step " << k
- << ". Simulation aborted."
- << endl;
-
- set_status( SIMULATION_UNSAT );
+ }
+ else {
+ TRACE << "Inconsistency detected in transition relation at step " << k
+ << ". Simulation is deadlocked."
+ << endl;
+ f_status = SIMULATION_DEADLOCKED;
+ return;
+ }
}
}
else {
- TRACE << "Inconsistency detected in initial states. Simulation aborted."
+ TRACE << "Inconsistency detected in initial states. Simulation is deadlocked."
<< endl;
-
- set_status( SIMULATION_UNSAT );
+ f_status = SIMULATION_DEADLOCKED;
}
-
- if (halt) {
- TRACE << "Simulation reached HALT condition"
- << endl;
- }
-
- TRACE << "Done." << endl;
}
View
16 src/algorithms/sim/simulation.hh
@@ -28,15 +28,16 @@
#include <witness_mgr.hh>
typedef enum {
- SIMULATION_UNSAT,
- SIMULATION_SAT,
- SIMULATION_UNKNOWN,
+ SIMULATION_DONE,
+ SIMULATION_HALTED,
+ SIMULATION_DEADLOCKED,
+ SIMULATION_INTERRUPTED,
} simulation_status_t;
class Simulation : public Algorithm {
public:
- Simulation(IModel& model, Expr_ptr halt_cond,
+ Simulation(IModel& model, Expr_ptr condition,
Expr_ptr witness_id, ExprVector& constraints);
~Simulation();
@@ -46,15 +47,14 @@ public:
inline simulation_status_t status() const
{ return f_status; }
- const inline Expr_ptr halt_cond() const
- { return f_halt_cond; }
-
private:
+ /* None of 'em, one of 'em, not both. */
Expr_ptr f_halt_cond;
+ Expr_ptr f_nsteps;
+
ExprVector f_constraints;
simulation_status_t f_status;
- void set_status(simulation_status_t status);
};
class SimulationWitness : public Witness {
View
4 src/cmd/cmd.hh
@@ -52,8 +52,8 @@ public:
inline Command_ptr make_load_model(const char *filepath)
{ return new LoadModelCommand(f_interpreter, filepath); }
- inline Command_ptr make_prepare()
- { return new PrepareCommand(f_interpreter); }
+ inline Command_ptr make_init()
+ { return new InitCommand(f_interpreter); }
inline Command_ptr make_simulate(Expr_ptr halt_cond, Expr_ptr resume_id, ExprVector& constraints)
{ return new SimulateCommand(f_interpreter, halt_cond, resume_id, constraints); }
View
35 src/cmd/command.cc
@@ -83,19 +83,19 @@ Variant TimeCommand::operator()()
TimeCommand::~TimeCommand()
{}
-// -- Prepare -------------------------------------------------------------
-PrepareCommand::PrepareCommand(Interpreter& owner)
+// -- Init -------------------------------------------------------------
+InitCommand::InitCommand(Interpreter& owner)
: Command(owner)
- , f_prepare(* ModelMgr::INSTANCE().model())
+ , f_init(* ModelMgr::INSTANCE().model())
{}
-Variant PrepareCommand::operator()()
+Variant InitCommand::operator()()
{
- f_prepare.process();
+ f_init.process();
return Variant("Ok");
}
-PrepareCommand::~PrepareCommand()
+InitCommand::~InitCommand()
{}
// -- Check -------------------------------------------------------------
@@ -127,11 +127,28 @@ SimulateCommand::SimulateCommand(Interpreter& owner,
Variant SimulateCommand::operator()()
{
+ ostringstream tmp;
f_sim.process();
- ostringstream tmp;
- tmp << "Simulation halted, see witness '"
- << f_sim.witness().id() << "'";
+ switch (f_sim.status()) {
+ case SIMULATION_DONE:
+ tmp << "Simulation done, see witness '" << f_sim.witness().id() << "'"
+ << endl;
+ break;
+ case SIMULATION_HALTED:
+ tmp << "Simulation halted, see witness '" << f_sim.witness().id() << "'"
+ << endl;
+ break;
+ case SIMULATION_DEADLOCKED:
+ tmp << "Simulation deadlocked, see witness '" << f_sim.witness().id() << "'"
+ << endl;
+ break;
+ case SIMULATION_INTERRUPTED:
+ tmp << "Simulation interrupted, see witness '" << f_sim.witness().id() << "'"
+ << endl;
+ break;
+ default: assert( false ); /* unreachable */
+ } /* switch */
return Variant(tmp.str());
}
View
10 src/cmd/command.hh
@@ -30,7 +30,7 @@
#include <sat.hh>
/* algorithms */
-#include <prepare.hh>
+#include <init.hh>
#include <bmc/bmc.hh>
#include <sim/simulation.hh>
@@ -85,15 +85,15 @@ public:
Variant virtual operator()();
};
-class PrepareCommand : public Command {
+class InitCommand : public Command {
public:
- PrepareCommand(Interpreter& owner);
- virtual ~PrepareCommand();
+ InitCommand(Interpreter& owner);
+ virtual ~InitCommand();
Variant virtual operator()();
private:
- Prepare f_prepare;
+ Init f_init;
};
/* Performs a new simulation with given constraints and halting
View
14 src/parser/grammars/smv.g
@@ -158,7 +158,7 @@ commands returns [Command_ptr res]
| c=time_command
{ $res = c; }
- | c=prepare_command
+ | c=init_command
{ $res = c; }
| c=model_command
@@ -187,8 +187,8 @@ time_command returns [Command_ptr res]
: 'time' { $res = cm.make_time(); }
;
-prepare_command returns [Command_ptr res]
- : 'prepare' { $res = cm.make_prepare(); }
+init_command returns [Command_ptr res]
+ : 'init' { $res = cm.make_init(); }
;
model_command returns [Command_ptr res]
@@ -229,10 +229,10 @@ simulate_command returns [Command_ptr res]
) *
) ?
- ( 'halt'
- ( 'on' expr=toplevel_expression { halt_cond = expr; } )
- | ( 'after' expr=constant { halt_cond = expr; } )
-
+ ( 'halt' expr=toplevel_expression
+ { halt_cond = expr; }
+ | expr=constant
+ { halt_cond = expr; }
) ?
( 'resume' wid=identifier
Please sign in to comment.
Something went wrong with that request. Please try again.