Skip to content
Browse files

Revamping algorithms

  • Loading branch information...
1 parent d5e4740 commit 15960649dbb144ea17717ecc6cf6cde3a53281fe @mwolf76 committed Dec 18, 2012
View
79 src/algorithms/base.cc
@@ -24,21 +24,17 @@
**/
#include <base.hh>
-Algorithm::Algorithm(IModel& model)
+Algorithm::Algorithm()
: f_mm(ModelMgr::INSTANCE())
, f_em(ExprMgr::INSTANCE())
, f_tm(TypeMgr::INSTANCE())
- , f_model(model)
, f_engine(* new SAT())
{
set_param("alg_name", "test");
DEBUG << "Creating Base algoritm instance "
<< get_param("alg_name")
<< " @" << this
<< endl;
-
- /* pre-compilation */
- prepare();
}
Algorithm::~Algorithm()
@@ -64,76 +60,3 @@ Variant& Algorithm::get_param(const string key)
else return NilValue;
}
-
-void Algorithm::prepare()
-{
- /* internal structures are empty */
- assert( 0 == f_init_adds.size() );
- assert( 0 == f_trans_adds.size() );
-
- const Modules& modules = f_model.modules();
- for (Modules::const_iterator m = modules.begin();
- m != modules.end(); ++ m) {
-
- Module& module = dynamic_cast <Module&> (*m->second);
-
- /* INIT */
- const ExprVector init = module.init();
- for (ExprVector::const_iterator init_eye = init.begin();
- init_eye != init.end(); ++ init_eye) {
-
- Expr_ptr ctx = module.expr();
- Expr_ptr body = (*init_eye);
-
- f_init_adds.push_back(f_compiler.process(ctx, body));
- }
-
- /* TRANS */
- const ExprVector trans = module.trans();
- for (ExprVector::const_iterator trans_eye = trans.begin();
- trans_eye != trans.end(); ++ trans_eye) {
-
- Expr_ptr ctx = module.expr();
- Expr_ptr body = (*trans_eye);
-
- f_trans_adds.push_back(f_compiler.process(ctx, body));
- }
- }
-}
-
-void Algorithm::assert_fsm_init(step_t time, group_t group, color_t color)
-{
- clock_t t0 = clock();
- unsigned n = f_init_adds.size();
- TRACE << "CNFizing INITs @" << time
- << "... (" << n << " formulas)"
- << endl;
-
- ADDVector::iterator i;
- for (i = f_init_adds.begin(); f_init_adds.end() != i; ++ i) {
- f_engine.push( *i, time, group, color);
- }
-
- clock_t elapsed = clock() - t0;
- double secs = (double) elapsed / (double) CLOCKS_PER_SEC;
- TRACE << "Done. (took " << secs << " seconds)" << endl;
-}
-
-void Algorithm::assert_fsm_trans(step_t time, group_t group, color_t color)
-{
- clock_t t0 = clock();
- unsigned n = f_trans_adds.size();
-
- TRACE << "CNFizing TRANSes @" << time
- << "... (" << n << " formulas)"
- << endl;
-
- ADDVector::iterator i;
- for (i = f_trans_adds.begin(); f_trans_adds.end() != i; ++ i) {
- f_engine.push( *i, time, group, color);
- }
-
- clock_t elapsed = clock() - t0;
- double secs = (double) elapsed / (double) CLOCKS_PER_SEC;
- TRACE << "Done. (took " << secs << " seconds)" << endl;
-}
View
30 src/algorithms/base.hh
@@ -55,27 +55,20 @@ using Minisat::STATUS_UNSAT;
class Algorithm {
public:
- Algorithm(IModel& model);
+ Algorithm();
virtual ~Algorithm();
// actual algorithm
virtual void process() =0;
- IModel& model() const
- { return f_model; }
-
- // alg abstract param iface (key -> value map)
+ // algorithm abstract param interface (key -> value map)
void set_param(string key, Variant value);
Variant& get_param(const string key);
-protected:
- void assert_fsm_init (step_t time,
- group_t group = MAINGROUP,
- color_t color = BACKGROUND);
+ inline Compiler& compiler()
+ { return f_compiler; }
- void assert_fsm_trans(step_t time,
- group_t group = MAINGROUP,
- color_t color = BACKGROUND);
+protected:
inline ModelMgr& mm()
{ return f_mm; }
@@ -86,28 +79,15 @@ protected:
inline TypeMgr& tm()
{ return f_tm; }
- inline IModel& model()
- { return f_model; }
-
inline SAT& engine()
{ return f_engine; }
- inline Compiler& compiler()
- { return f_compiler; }
-
private:
// managers
ModelMgr& f_mm;
ExprMgr& f_em;
TypeMgr& f_tm;
- IModel& f_model;
- ADDVector f_init_adds;
- ADDVector f_trans_adds;
-
- // services
- void prepare();
-
/* Model Compiler */
Compiler f_compiler;
View
3 src/algorithms/bmc/bmc.cc
@@ -27,7 +27,8 @@
BMC::BMC(IModel& model, Expr_ptr property)
: MCAlgorithm(model, property)
-{}
+{
+}
BMC::~BMC()
{}
View
13 src/algorithms/kind/kind.cc
@@ -29,15 +29,7 @@ using namespace Minisat;
KInduction::KInduction(IModel& model, Expr_ptr property)
: MCAlgorithm(model, property)
{
- prepare();
-}
-
-KInduction::~KInduction()
-{}
-
-void KInduction::prepare()
-{
- const Modules& modules = model().modules();
+ const Modules& modules = f_model.modules();
for (Modules::const_iterator m = modules.begin();
m != modules.end(); ++ m) {
@@ -75,6 +67,9 @@ void KInduction::assert_fsm_not_init(step_t time, group_t group, color_t color)
TRACE << "Done. (took " << secs << " seconds)" << endl;
}
+KInduction::~KInduction()
+{}
+
void KInduction::process()
{
step_t k; // to infinity...
View
4 src/algorithms/kind/kind.hh
@@ -47,10 +47,6 @@ protected:
void assert_fsm_not_init (step_t time,
group_t group = MAINGROUP,
color_t color = BACKGROUND);
-
-private:
- void prepare();
-
};
#endif
View
105 src/algorithms/mc.cc
@@ -27,7 +27,8 @@
using namespace Minisat;
MCAlgorithm::MCAlgorithm(IModel& model, Expr_ptr property)
- : Algorithm(model)
+ : Algorithm()
+ , f_model(model)
, f_property(property)
, f_witness(NULL)
{
@@ -37,8 +38,45 @@ MCAlgorithm::MCAlgorithm(IModel& model, Expr_ptr property)
<< " @" << this
<< endl;
- /* pre-compilation */
- prepare();
+ /* internal structures are empty */
+ assert( 0 == f_init_adds.size() );
+ assert( 0 == f_trans_adds.size() );
+
+ const Modules& modules = f_model.modules();
+ for (Modules::const_iterator m = modules.begin();
+ m != modules.end(); ++ m) {
+
+ Module& module = dynamic_cast <Module&> (*m->second);
+
+ /* INIT */
+ const ExprVector init = module.init();
+ for (ExprVector::const_iterator init_eye = init.begin();
+ init_eye != init.end(); ++ init_eye) {
+
+ Expr_ptr ctx = module.expr();
+ Expr_ptr body = (*init_eye);
+
+ f_init_adds.push_back(compiler().process(ctx, body));
+ }
+
+ /* TRANS */
+ const ExprVector trans = module.trans();
+ for (ExprVector::const_iterator trans_eye = trans.begin();
+ trans_eye != trans.end(); ++ trans_eye) {
+
+ Expr_ptr ctx = module.expr();
+ Expr_ptr body = (*trans_eye);
+
+ f_trans_adds.push_back(compiler().process(ctx, body));
+ }
+ }
+
+ /* Invariant */
+ f_invariant_add = compiler().process( em().make_main(), f_property);
+
+ /* Violation (negation of Invarion) */
+ f_violation_add = compiler().process( em().make_main(),
+ em().make_not( f_property));
}
MCAlgorithm::~MCAlgorithm()
@@ -64,16 +102,6 @@ Witness& MCAlgorithm::get_witness() const
void MCAlgorithm::set_status(mc_status_t status)
{ f_status = status; }
-void MCAlgorithm::prepare()
-{
- /* Invariant */
- f_invariant_add = compiler().process( em().make_main(), f_property);
-
- /* Violation (negation of Invarion) */
- f_violation_add = compiler().process( em().make_main(),
- em().make_not( f_property));
-}
-
void MCAlgorithm::assert_violation(step_t time, group_t group, color_t color)
{
// TODO: macro to wrap code to be benchmarked (cool!)
@@ -87,3 +115,54 @@ void MCAlgorithm::assert_violation(step_t time, group_t group, color_t color)
double secs = (double) elapsed / (double) CLOCKS_PER_SEC;
TRACE << "Done. (took " << secs << " seconds)" << endl;
}
+
+void MCAlgorithm::assert_fsm_init(step_t time, group_t group, color_t color)
+{
+ clock_t t0 = clock();
+ unsigned n = f_init_adds.size();
+ TRACE << "CNFizing INITs @" << time
+ << "... (" << n << " formulas)"
+ << endl;
+
+ ADDVector::iterator i;
+ for (i = f_init_adds.begin(); f_init_adds.end() != i; ++ i) {
+ engine().push( *i, time, group, color);
+ }
+
+ clock_t elapsed = clock() - t0;
+ double secs = (double) elapsed / (double) CLOCKS_PER_SEC;
+ TRACE << "Done. (took " << secs << " seconds)" << endl;
+}
+
+void MCAlgorithm::assert_fsm_trans(step_t time, group_t group, color_t color)
+{
+ clock_t t0 = clock();
+ unsigned n = f_trans_adds.size();
+
+ TRACE << "CNFizing TRANSes @" << time
+ << "... (" << n << " formulas)"
+ << endl;
+
+ ADDVector::iterator i;
+ for (i = f_trans_adds.begin(); f_trans_adds.end() != i; ++ i) {
+ engine().push( *i, time, group, color);
+ }
+
+ clock_t elapsed = clock() - t0;
+ double secs = (double) elapsed / (double) CLOCKS_PER_SEC;
+ TRACE << "Done. (took " << secs << " seconds)" << endl;
+}
+
+SlaveAlgorithm::SlaveAlgorithm(MCAlgorithm& master)
+ : Algorithm()
+ , f_master(master)
+{
+}
+
+SlaveAlgorithm::~SlaveAlgorithm()
+{
+ DEBUG << "Destroying MC algoritm instance"
+ << get_param("alg_name")
+ << " @" << this
+ << endl;
+}
View
52 src/algorithms/mc.hh
@@ -43,41 +43,71 @@ public:
mc_status_t status() const;
bool has_witness() const;
-
Witness& get_witness() const;
+ inline Expr_ptr property()
+ { return f_property; }
+
+ inline IModel& model()
+ { return f_model; }
+
protected:
- inline ADD& invariant()
- { return f_invariant_add; }
+ IModel& f_model;
+ Expr_ptr f_property;
- inline ADD& violation()
- { return f_violation_add; }
+ void assert_fsm_init (step_t time,
+ group_t group = MAINGROUP,
+ color_t color = BACKGROUND);
- inline Expr_ptr property()
- { return f_property; }
+ void assert_fsm_trans(step_t time,
+ group_t group = MAINGROUP,
+ color_t color = BACKGROUND);
void assert_violation(step_t time,
group_t group = MAINGROUP,
color_t color = BACKGROUND);
+ inline ADD& invariant()
+ { return f_invariant_add; }
+
void assert_invariant(step_t time,
group_t group = MAINGROUP,
color_t color = BACKGROUND);
+ inline ADD& violation()
+ { return f_violation_add; }
+
void set_status(mc_status_t status);
private:
- // services
- void prepare();
-
ADD f_invariant_add;
ADD f_violation_add;
- Expr_ptr f_property;
+ ADDVector f_init_adds;
+ ADDVector f_trans_adds;
// ctx witness
Witness_ptr f_witness;
mc_status_t f_status;
};
+class SlaveAlgorithm : public Algorithm {
+public:
+ SlaveAlgorithm(MCAlgorithm& master);
+ virtual ~SlaveAlgorithm();
+
+protected:
+ void assert_violation(step_t time,
+ group_t group = MAINGROUP,
+ color_t color = BACKGROUND);
+
+ void assert_invariant(step_t time,
+ group_t group = MAINGROUP,
+ color_t color = BACKGROUND);
+
+private:
+ MCAlgorithm& f_master;
+};
+
+
#endif
View
75 src/algorithms/sim/simulation.cc
@@ -27,11 +27,45 @@
Simulation::Simulation(IModel& model, int resume,
int nsteps, ExprVector& constraints)
- : Algorithm(model)
+ : Algorithm()
+ , f_model(model)
, f_resume(resume)
, f_nsteps(nsteps)
, f_constraints(constraints)
-{}
+{
+ /* internal structures are empty */
+ assert( 0 == f_init_adds.size() );
+ assert( 0 == f_trans_adds.size() );
+
+ const Modules& modules = f_model.modules();
+ for (Modules::const_iterator m = modules.begin();
+ m != modules.end(); ++ m) {
+
+ Module& module = dynamic_cast <Module&> (*m->second);
+
+ /* INIT */
+ const ExprVector init = module.init();
+ for (ExprVector::const_iterator init_eye = init.begin();
+ init_eye != init.end(); ++ init_eye) {
+
+ Expr_ptr ctx = module.expr();
+ Expr_ptr body = (*init_eye);
+
+ f_init_adds.push_back(compiler().process(ctx, body));
+ }
+
+ /* TRANS */
+ const ExprVector trans = module.trans();
+ for (ExprVector::const_iterator trans_eye = trans.begin();
+ trans_eye != trans.end(); ++ trans_eye) {
+
+ Expr_ptr ctx = module.expr();
+ Expr_ptr body = (*trans_eye);
+
+ f_trans_adds.push_back(compiler().process(ctx, body));
+ }
+ }
+}
Simulation::~Simulation()
{}
@@ -90,3 +124,40 @@ void Simulation::process()
TRACE << "Done." << endl;
}
+
+void Simulation::assert_fsm_init(step_t time, group_t group, color_t color)
+{
+ clock_t t0 = clock();
+ unsigned n = f_init_adds.size();
+ TRACE << "CNFizing INITs @" << time
+ << "... (" << n << " formulas)"
+ << endl;
+
+ ADDVector::iterator i;
+ for (i = f_init_adds.begin(); f_init_adds.end() != i; ++ i) {
+ engine().push( *i, time, group, color);
+ }
+
+ clock_t elapsed = clock() - t0;
+ double secs = (double) elapsed / (double) CLOCKS_PER_SEC;
+ TRACE << "Done. (took " << secs << " seconds)" << endl;
+}
+
+void Simulation::assert_fsm_trans(step_t time, group_t group, color_t color)
+{
+ clock_t t0 = clock();
+ unsigned n = f_trans_adds.size();
+
+ TRACE << "CNFizing TRANSes @" << time
+ << "... (" << n << " formulas)"
+ << endl;
+
+ ADDVector::iterator i;
+ for (i = f_trans_adds.begin(); f_trans_adds.end() != i; ++ i) {
+ engine().push( *i, time, group, color);
+ }
+
+ clock_t elapsed = clock() - t0;
+ double secs = (double) elapsed / (double) CLOCKS_PER_SEC;
+ TRACE << "Done. (took " << secs << " seconds)" << endl;
+}
View
14 src/algorithms/sim/simulation.hh
@@ -49,12 +49,26 @@ public:
simulation_status_t status() const;
private:
+ IModel& f_model;
+
int f_resume;
int f_nsteps;
ExprVector f_constraints;
simulation_status_t f_status;
void set_status(simulation_status_t status);
+
+ ADDVector f_init_adds;
+ ADDVector f_trans_adds;
+
+ void assert_fsm_init (step_t time,
+ group_t group = MAINGROUP,
+ color_t color = BACKGROUND);
+
+ void assert_fsm_trans(step_t time,
+ group_t group = MAINGROUP,
+ color_t color = BACKGROUND);
+
};
class SimulationWitness : public Witness {

0 comments on commit 1596064

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