diff --git a/regression/ebmc/BDD/AF1.desc b/regression/ebmc/BDD/AF1.desc new file mode 100644 index 000000000..fee19fe3e --- /dev/null +++ b/regression/ebmc/BDD/AF1.desc @@ -0,0 +1,10 @@ +CORE +AF1.smv +--bdd +^\[main::spec1\] AF some_var = TRUE: REFUTED$ +^\[main::spec2\] AF some_var = FALSE: PROVED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/BDD/AF1.smv b/regression/ebmc/BDD/AF1.smv new file mode 100644 index 000000000..d138a099e --- /dev/null +++ b/regression/ebmc/BDD/AF1.smv @@ -0,0 +1,11 @@ +MODULE main + +VAR some_var : boolean; + +INVAR some_var = 0 + +-- should fail +SPEC AF some_var = 1 + +-- should pass +SPEC AF some_var = 0 diff --git a/regression/ebmc/BDD/AF2.desc b/regression/ebmc/BDD/AF2.desc new file mode 100644 index 000000000..9a274ca3c --- /dev/null +++ b/regression/ebmc/BDD/AF2.desc @@ -0,0 +1,10 @@ +CORE +AF2.smv +--bdd +^\[main::spec1\] AF some_var = TRUE: REFUTED$ +^\[main::spec2\] AF some_var = FALSE: PROVED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/BDD/AF2.smv b/regression/ebmc/BDD/AF2.smv new file mode 100644 index 000000000..4e7d6f91d --- /dev/null +++ b/regression/ebmc/BDD/AF2.smv @@ -0,0 +1,11 @@ +MODULE main + +VAR some_var : boolean; + +ASSIGN next(some_var) := 0; + +-- should fail +SPEC AF some_var = 1 + +-- should pass +SPEC AF some_var = 0 diff --git a/regression/ebmc/BDD/AG1.desc b/regression/ebmc/BDD/AG1.desc new file mode 100644 index 000000000..0ab3b01ee --- /dev/null +++ b/regression/ebmc/BDD/AG1.desc @@ -0,0 +1,10 @@ +CORE +AG1.smv +--bdd +^\[main::spec1\] AG some_var = TRUE: REFUTED$ +^\[main::spec2\] AG some_var = FALSE: PROVED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/BDD/AG1.smv b/regression/ebmc/BDD/AG1.smv new file mode 100644 index 000000000..3160bb014 --- /dev/null +++ b/regression/ebmc/BDD/AG1.smv @@ -0,0 +1,11 @@ +MODULE main + +VAR some_var : boolean; + +INVAR some_var = 0 + +-- should fail +SPEC AG some_var = 1 + +-- should pass +SPEC AG some_var = 0 diff --git a/regression/ebmc/BDD/AG2.desc b/regression/ebmc/BDD/AG2.desc new file mode 100644 index 000000000..aed42a6e6 --- /dev/null +++ b/regression/ebmc/BDD/AG2.desc @@ -0,0 +1,10 @@ +CORE +AG2.smv +--bdd +^\[main::spec1\] AG some_var = TRUE: REFUTED$ +^\[main::spec2\] AG some_var = FALSE: REFUTED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/BDD/AG2.smv b/regression/ebmc/BDD/AG2.smv new file mode 100644 index 000000000..c4ba3af4e --- /dev/null +++ b/regression/ebmc/BDD/AG2.smv @@ -0,0 +1,11 @@ +MODULE main + +VAR some_var : boolean; + +ASSIGN next(some_var) := 0; + +-- should fail +SPEC AG some_var = 1 + +-- should fail +SPEC AG some_var = 0 diff --git a/regression/ebmc/BDD/AU1.desc b/regression/ebmc/BDD/AU1.desc new file mode 100644 index 000000000..2510d97e7 --- /dev/null +++ b/regression/ebmc/BDD/AU1.desc @@ -0,0 +1,8 @@ +KNOWNBUG +AU1.smv +--bdd +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/BDD/AU1.smv b/regression/ebmc/BDD/AU1.smv new file mode 100644 index 000000000..cf723c0f8 --- /dev/null +++ b/regression/ebmc/BDD/AU1.smv @@ -0,0 +1,16 @@ +MODULE main + +VAR x : 0..10; + +-- 1, 2, 3, ..., 10 +ASSIGN init(x) := 1; +ASSIGN next(x) := case + x = 10 : 10; + 1 : x + 1; + esac; + +-- should fail, since x=0 is not reachable +SPEC A x>=1 U x=0 + +-- should pass +SPEC A x>=1 U x=10 diff --git a/regression/ebmc/BDD/AX1.desc b/regression/ebmc/BDD/AX1.desc new file mode 100644 index 000000000..abc4ce68d --- /dev/null +++ b/regression/ebmc/BDD/AX1.desc @@ -0,0 +1,10 @@ +CORE +AX1.smv +--bdd +^\[main::spec1\] AX some_var = TRUE: REFUTED$ +^\[main::spec2\] AX some_var = FALSE: PROVED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/BDD/AX1.smv b/regression/ebmc/BDD/AX1.smv new file mode 100644 index 000000000..be19b5ce5 --- /dev/null +++ b/regression/ebmc/BDD/AX1.smv @@ -0,0 +1,11 @@ +MODULE main + +VAR some_var : boolean; + +INVAR some_var = 0 + +-- should fail +SPEC AX some_var = 1 + +-- should pass +SPEC AX some_var = 0 diff --git a/regression/ebmc/BDD/EF1.desc b/regression/ebmc/BDD/EF1.desc new file mode 100644 index 000000000..8da7b9529 --- /dev/null +++ b/regression/ebmc/BDD/EF1.desc @@ -0,0 +1,10 @@ +CORE +EF1.smv +--bdd +^\[main::spec1\] EF some_var = TRUE: REFUTED$ +^\[main::spec2\] EF some_var = FALSE: PROVED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/BDD/EF1.smv b/regression/ebmc/BDD/EF1.smv new file mode 100644 index 000000000..a956b5e63 --- /dev/null +++ b/regression/ebmc/BDD/EF1.smv @@ -0,0 +1,11 @@ +MODULE main + +VAR some_var : boolean; + +INVAR some_var = 0 + +-- should fail +SPEC EF some_var = 1 + +-- should pass +SPEC EF some_var = 0 diff --git a/regression/ebmc/BDD/EF2.desc b/regression/ebmc/BDD/EF2.desc new file mode 100644 index 000000000..ce03ac682 --- /dev/null +++ b/regression/ebmc/BDD/EF2.desc @@ -0,0 +1,10 @@ +CORE +EF2.smv +--bdd +^\[main::spec1\] EF some_var = TRUE: REFUTED$ +^\[main::spec2\] EF some_var = FALSE: PROVED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/BDD/EF2.smv b/regression/ebmc/BDD/EF2.smv new file mode 100644 index 000000000..5938e5add --- /dev/null +++ b/regression/ebmc/BDD/EF2.smv @@ -0,0 +1,11 @@ +MODULE main + +VAR some_var : boolean; + +ASSIGN next(some_var) := 0; + +-- should fail +SPEC EF some_var = 1 + +-- should pass +SPEC EF some_var = 0 diff --git a/regression/ebmc/BDD/EG1.desc b/regression/ebmc/BDD/EG1.desc new file mode 100644 index 000000000..d76c69604 --- /dev/null +++ b/regression/ebmc/BDD/EG1.desc @@ -0,0 +1,10 @@ +CORE +EG1.smv +--bdd +^\[main::spec1\] EG some_var = TRUE: REFUTED$ +^\[main::spec2\] EG some_var = FALSE: PROVED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/BDD/EG1.smv b/regression/ebmc/BDD/EG1.smv new file mode 100644 index 000000000..1e98ca846 --- /dev/null +++ b/regression/ebmc/BDD/EG1.smv @@ -0,0 +1,11 @@ +MODULE main + +VAR some_var : boolean; + +INVAR some_var = 0 + +-- should fail +SPEC EG some_var = 1 + +-- should pass +SPEC EG some_var = 0 diff --git a/regression/ebmc/BDD/EG2.desc b/regression/ebmc/BDD/EG2.desc new file mode 100644 index 000000000..98d5e6970 --- /dev/null +++ b/regression/ebmc/BDD/EG2.desc @@ -0,0 +1,10 @@ +CORE +EG2.smv +--bdd +^\[main::spec1\] EG some_var = TRUE: REFUTED$ +^\[main::spec2\] EG some_var = FALSE: REFUTED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/BDD/EG2.smv b/regression/ebmc/BDD/EG2.smv new file mode 100644 index 000000000..b243473f3 --- /dev/null +++ b/regression/ebmc/BDD/EG2.smv @@ -0,0 +1,11 @@ +MODULE main + +VAR some_var : boolean; + +ASSIGN next(some_var) := 0; + +-- should fail +SPEC EG some_var = 1 + +-- should fail +SPEC EG some_var = 0 diff --git a/regression/ebmc/BDD/EX1.desc b/regression/ebmc/BDD/EX1.desc new file mode 100644 index 000000000..4bd9972a8 --- /dev/null +++ b/regression/ebmc/BDD/EX1.desc @@ -0,0 +1,10 @@ +CORE +EX1.smv +--bdd +^\[main::spec1\] EX some_var = TRUE: REFUTED$ +^\[main::spec2\] EX some_var = FALSE: PROVED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/BDD/EX1.smv b/regression/ebmc/BDD/EX1.smv new file mode 100644 index 000000000..1fedef77c --- /dev/null +++ b/regression/ebmc/BDD/EX1.smv @@ -0,0 +1,11 @@ +MODULE main + +VAR some_var : boolean; + +INVAR some_var = 0 + +-- should fail +SPEC EX some_var = 1 + +-- should pass +SPEC EX some_var = 0 diff --git a/regression/ebmc/BDD/EX2.desc b/regression/ebmc/BDD/EX2.desc new file mode 100644 index 000000000..df449e386 --- /dev/null +++ b/regression/ebmc/BDD/EX2.desc @@ -0,0 +1,10 @@ +CORE +EX2.smv +--bdd +^\[main::spec1\] EX some_var = TRUE: REFUTED$ +^\[main::spec2\] EX some_var = FALSE: PROVED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/BDD/EX2.smv b/regression/ebmc/BDD/EX2.smv new file mode 100644 index 000000000..0cd118ffe --- /dev/null +++ b/regression/ebmc/BDD/EX2.smv @@ -0,0 +1,11 @@ +MODULE main + +VAR some_var : boolean; + +ASSIGN next(some_var) := 0; + +-- should fail +SPEC EX some_var = 1 + +-- should pass +SPEC EX some_var = 0 diff --git a/regression/ebmc/BDD/GF1.desc b/regression/ebmc/BDD/GF1.desc index 80ae71845..fe80c7b5f 100644 --- a/regression/ebmc/BDD/GF1.desc +++ b/regression/ebmc/BDD/GF1.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE GF1.smv --bdd ^\[main::spec1\] G F some_var: REFUTED$ diff --git a/regression/ebmc/BDD/just_p.desc b/regression/ebmc/BDD/just_p.desc new file mode 100644 index 000000000..670e73cd4 --- /dev/null +++ b/regression/ebmc/BDD/just_p.desc @@ -0,0 +1,10 @@ +CORE +just_p.smv +--bdd +^\[main::spec1\] some_var = TRUE: REFUTED$ +^\[main::spec2\] some_var = FALSE: PROVED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/BDD/just_p.smv b/regression/ebmc/BDD/just_p.smv new file mode 100644 index 000000000..b0f925913 --- /dev/null +++ b/regression/ebmc/BDD/just_p.smv @@ -0,0 +1,11 @@ +MODULE main + +VAR some_var : boolean; + +ASSIGN init(some_var) := 0; + +-- should fail +SPEC some_var = 1 + +-- should pass +SPEC some_var = 0 diff --git a/regression/ebmc/smv/smv_ltlspec2.desc b/regression/ebmc/smv/smv_ltlspec2.desc index 47298d4cc..d0880d8e1 100644 --- a/regression/ebmc/smv/smv_ltlspec2.desc +++ b/regression/ebmc/smv/smv_ltlspec2.desc @@ -1,10 +1,9 @@ -KNOWNBUG +CORE smv_ltlspec2.smv --bdd ^EXIT=0$ ^SIGNAL=0$ -^\[smv::main::spec1\] G F x = 3: PROVED$ +^\[main::spec1\] G F x = 3: PROVED$ -- ^warning: ignoring -- -The BDD engine returns REFUTED. diff --git a/src/ebmc/bdd_engine.cpp b/src/ebmc/bdd_engine.cpp index 6aeee5026..73a08f36e 100644 --- a/src/ebmc/bdd_engine.cpp +++ b/src/ebmc/bdd_engine.cpp @@ -112,10 +112,9 @@ class bdd_enginet return result; } - void get_atomic_propositions(const exprt &); + void get_atomic_propositions(const exprt &); void check_property(propertyt &); - BDD property2BDD(const exprt &); - + BDD current_to_next(const BDD &) const; BDD next_to_current(const BDD &) const; BDD project_next(const BDD &) const; @@ -125,9 +124,35 @@ class bdd_enginet propertyt &, unsigned number_of_timeframes); - void AGp(propertyt &); - void AGAFp(propertyt &); - void just_p(propertyt &); + void check_AGp(propertyt &); + void check_CTL(propertyt &); + BDD CTL(const exprt &); + BDD EX(BDD); + BDD AX(BDD f) + { + return !EX(!f); + } + BDD EF(BDD); + BDD AF(BDD f) + { + return !EG(!f); + } + BDD EG(BDD); + BDD AG(BDD f) + { + return !EF(!f); + } + BDD EU(BDD, BDD); + BDD AU(BDD, BDD); + BDD ER(BDD f1, BDD f2) + { + return !AU(!f1, !f2); + } + BDD AR(BDD f1, BDD f2) + { + return !EU(!f1, !f2); + } + BDD fixedpoint(std::function, BDD); }; /*******************************************************************\ @@ -184,7 +209,7 @@ int bdd_enginet::operator()() for(const auto & a : atomic_propositions) { std::cout << '`' << format(a.first) << "' -> " - << a.second.bdd.node_number(); + << a.second.bdd.node_number() << '\n'; } std::cout << '\n'; @@ -437,37 +462,42 @@ void bdd_enginet::check_property(propertyt &property) !has_temporal_operator(to_unary_expr(expr).op()); }; - // special treatment for AG AFp and G F p - auto is_always_eventually = [](const exprt &expr) { - return expr.id() == ID_sva_always && - to_unary_expr(expr).op().id() == ID_sva_s_eventually && - !has_temporal_operator(to_unary_expr(to_unary_expr(expr).op()).op()); - }; + // Our engine knows CTL only. + // We map selected path properties to CTL. - auto is_AG_AFp = [](const exprt &expr) { - return expr.id() == ID_AG && to_AG_expr(expr).op().id() == ID_AF && - !has_temporal_operator(to_AF_expr(to_AG_expr(expr).op()).op()); - }; + if( + property.normalized_expr.id() == ID_G && + to_G_expr(property.normalized_expr).op().id() == ID_F && + !has_temporal_operator( + to_F_expr(to_G_expr(property.normalized_expr).op()).op())) + { + // G F p --> AG AF p + auto p = to_F_expr(to_G_expr(property.normalized_expr).op()).op(); + property.normalized_expr = AG_exprt{AF_exprt{p}}; + } - auto is_GFp = [](const exprt &expr) { - return expr.id() == ID_G && to_G_expr(expr).op().id() == ID_F && - !has_temporal_operator(to_F_expr(to_G_expr(expr).op()).op()); - }; + if( + property.normalized_expr.id() == ID_sva_always && + to_sva_always_expr(property.normalized_expr).op().id() == + ID_sva_s_eventually && + !has_temporal_operator(to_sva_s_eventually_expr( + to_sva_always_expr(property.normalized_expr).op()) + .op())) + { + // always s_eventually p --> AG AF p + auto p = to_sva_s_eventually_expr( + to_sva_always_expr(property.normalized_expr).op()) + .op(); + property.normalized_expr = AG_exprt{AF_exprt{p}}; + } if(is_AGp(property.normalized_expr)) { - AGp(property); + check_AGp(property); } - else if( - is_AG_AFp(property.normalized_expr) || - is_always_eventually(property.normalized_expr) || - is_GFp(property.normalized_expr)) + else if(is_CTL(property.normalized_expr)) { - AGAFp(property); - } - else if(!has_temporal_operator(property.normalized_expr)) - { - just_p(property); + check_CTL(property); } else property.failure("property not supported by BDD engine"); @@ -475,7 +505,7 @@ void bdd_enginet::check_property(propertyt &property) /*******************************************************************\ -Function: bdd_enginet::AGp +Function: bdd_enginet::check_AGp Inputs: @@ -485,10 +515,10 @@ Function: bdd_enginet::AGp \*******************************************************************/ -void bdd_enginet::AGp(propertyt &property) +void bdd_enginet::check_AGp(propertyt &property) { const exprt &sub_expr = to_unary_expr(property.normalized_expr).op(); - BDD p = property2BDD(sub_expr); + BDD p = CTL(sub_expr); // Start with !p, and go backwards until saturation or we hit an // initial state. @@ -556,7 +586,7 @@ void bdd_enginet::AGp(propertyt &property) /*******************************************************************\ -Function: bdd_enginet::AGAFp +Function: bdd_enginet::check_CTL Inputs: @@ -566,67 +596,23 @@ Function: bdd_enginet::AGAFp \*******************************************************************/ -void bdd_enginet::AGAFp(propertyt &property) +void bdd_enginet::check_CTL(propertyt &property) { - const exprt &sub_expr = - to_unary_expr(to_unary_expr(property.normalized_expr).op()).op(); - BDD p = property2BDD(sub_expr); + // For a CTL formula f, calculate the set of states that satisfy + // !f, and then check if that contains any initial state. + BDD not_f = !CTL(property.normalized_expr); - // Start with p, and go backwards until saturation. - // AG AFp holds iff this includes all initial states. + BDD intersection = not_f; - BDD good_states = p; - unsigned iteration = 0; + for(const auto &i : initial_BDDs) + intersection = intersection & i; for(const auto &c : constraints_BDDs) - good_states = good_states & c; - - std::size_t peak_bdd_nodes = 0; - - while(true) - { - iteration++; - message.statistics() << "Iteration " << iteration << messaget::eom; - - // make the states be expressed in terms of 'next' variables - BDD good_states_next = current_to_next(good_states); - - // now conjoin with transition relation - BDD conjunction = good_states_next; - - for(const auto &t : transition_BDDs) - conjunction = conjunction & t; - - for(const auto &c : constraints_BDDs) - conjunction = conjunction & c; - - // now project away 'next' variables - BDD pre_image = project_next(conjunction); - - // compute union - BDD set_union = good_states | pre_image; - - // have we saturated? - if((set_union == good_states).is_true()) - { - message.progress() << "Fixedpoint reached" << messaget::eom; - break; - } - - good_states = set_union; - - peak_bdd_nodes = std::max(peak_bdd_nodes, mgr.number_of_nodes()); - } - - // Does 'good_states' include all initial states? - BDD union_with_initial = good_states; - - for(const auto &i : initial_BDDs) - union_with_initial = union_with_initial | i; + intersection = intersection & c; - if((union_with_initial == good_states).is_true()) + if(intersection.is_false()) { - // proved + // intersection empty, proved property.proved(); message.status() << "Property proved" << messaget::eom; } @@ -640,57 +626,17 @@ void bdd_enginet::AGAFp(propertyt &property) /*******************************************************************\ -Function: bdd_enginet::just_p +Function: bdd_enginet::CTL - Inputs: + Inputs: a CTL expression - Outputs: - - Purpose: - -\*******************************************************************/ - -void bdd_enginet::just_p(propertyt &property) -{ - // We check whether the BDD for the negation of the property - // contains an initial state. - exprt negation = negate_property(property.normalized_expr); - BDD states = property2BDD(negation); - - // do we have an initial state? - BDD intersection = states; - - for(const auto &i : initial_BDDs) - intersection = intersection & i; - - for(const auto &c : constraints_BDDs) - intersection = intersection & c; - - if(!intersection.is_false()) - { - property.refuted(); - message.status() << "Property refuted" << messaget::eom; - } - else - { - property.proved(); - message.status() << "Property proved" << messaget::eom; - } -} - -/*******************************************************************\ - -Function: bdd_enginet::property2BDD - - Inputs: a property expression - - Outputs: a BDD for a set of states + Outputs: a BDD for the set of states that satisfies the expression Purpose: compute states that satisfy a particular property \*******************************************************************/ -bdd_enginet::BDD bdd_enginet::property2BDD(const exprt &expr) +bdd_enginet::BDD bdd_enginet::CTL(const exprt &expr) { if(expr.is_true()) return mgr.True(); @@ -698,128 +644,69 @@ bdd_enginet::BDD bdd_enginet::property2BDD(const exprt &expr) return mgr.False(); else if(expr.id()==ID_not) { - return !property2BDD(to_not_expr(expr).op()); + return !CTL(to_not_expr(expr).op()); } - else if(expr.id()==ID_implies || - expr.id()==ID_sva_overlapped_implication) + else if(expr.id() == ID_implies) { - return (!property2BDD(to_binary_expr(expr).lhs())) | - property2BDD(to_binary_expr(expr).rhs()); + return (!CTL(to_binary_expr(expr).lhs())) | CTL(to_binary_expr(expr).rhs()); } else if(expr.id()==ID_and) { BDD result=mgr.True(); for(const auto & op : expr.operands()) - result = result & property2BDD(op); + result = result & CTL(op); return result; } else if(expr.id()==ID_or) { BDD result=mgr.False(); for(const auto & op : expr.operands()) - result = result | property2BDD(op); + result = result | CTL(op); return result; } - else if(expr.id()==ID_sva_non_overlapped_implication) + else if(expr.id() == ID_EX) { - // use sva_nexttime for this - unary_predicate_exprt tmp(ID_sva_nexttime, to_binary_expr(expr).rhs()); - return (!property2BDD(to_binary_expr(expr).lhs())) | property2BDD(tmp); + return EX(CTL(to_EX_expr(expr).op())); } - else if(expr.id()==ID_sva_nexttime) + else if(expr.id() == ID_EF) { - // recursive call - const exprt &sub_expr = to_sva_nexttime_expr(expr).op(); - BDD p=property2BDD(sub_expr); - - // make 'p' be expressed in terms of 'next' variables - BDD p_next=current_to_next(p); - - // now conjoin with transition relation - BDD conjunction=p_next; - - for(const auto &t : transition_BDDs) - conjunction = conjunction & t; - - for(const auto &c : constraints_BDDs) - conjunction = conjunction & c; - - // now project away 'next' variables - BDD pre_image=project_next(conjunction); - - return pre_image; + return EF(CTL(to_EF_expr(expr).op())); } - else if(expr.id() == ID_F || expr.id() == ID_sva_s_eventually) + else if(expr.id() == ID_EG) { - // recursive call - const exprt &sub_expr = to_sva_s_eventually_expr(expr).op(); - BDD p=property2BDD(sub_expr); - BDD states=p; - - while(true) - { - // make 'states' be expressed in terms of 'next' variables - BDD states_next=current_to_next(p); - - // now conjoin with transition relation - BDD conjunction=states_next; - - for(const auto &t : transition_BDDs) - conjunction = conjunction & t; - - for(const auto &c : constraints_BDDs) - conjunction = conjunction & c; - - // now project away 'next' variables - BDD pre_image=project_next(conjunction); - - // compute intersection - BDD set_intersection=states & pre_image; - - // have we saturated? - if((set_intersection==states).is_true()) - break; - - states=set_intersection; - } - - return states; + return EG(CTL(to_EG_expr(expr).op())); } - else if(expr.id() == ID_AG || expr.id() == ID_G || expr.id() == ID_sva_always) + else if(expr.id() == ID_AX) { - // recursive call - const exprt &sub_expr = to_unary_expr(expr).op(); - BDD p=property2BDD(sub_expr); - BDD states=p; - - while(true) - { - // make 'states' be expressed in terms of 'next' variables - BDD states_next=current_to_next(p); - - // now conjoin with transition relation - BDD conjunction=states_next; - - for(const auto &t : transition_BDDs) - conjunction = conjunction & t; - - for(const auto &c : constraints_BDDs) - conjunction = conjunction & c; - - // now project away 'next' variables - BDD pre_image=project_next(conjunction); - - // compute union - BDD set_union=states | pre_image; - - // have we saturated? - if((set_union==states).is_true()) - break; - - states=set_union; - } - - return states; + return AX(CTL(to_AX_expr(expr).op())); + } + else if(expr.id() == ID_AF) + { + return AF(CTL(to_AF_expr(expr).op())); + } + else if(expr.id() == ID_AG) + { + return AG(CTL(to_AG_expr(expr).op())); + } + else if(expr.id() == ID_EU) + { + auto &EU_expr = to_EU_expr(expr); + return EU(CTL(EU_expr.lhs()), CTL(EU_expr.rhs())); + } + else if(expr.id() == ID_AU) + { + auto &AU_expr = to_AU_expr(expr); + return AU(CTL(AU_expr.lhs()), CTL(AU_expr.rhs())); + } + else if(expr.id() == ID_ER) + { + auto &ER_expr = to_ER_expr(expr); + return ER(CTL(ER_expr.lhs()), CTL(ER_expr.rhs())); + } + else if(expr.id() == ID_AR) + { + auto &AR_expr = to_AR_expr(expr); + return AR(CTL(AR_expr.lhs()), CTL(AR_expr.rhs())); } else { @@ -837,6 +724,150 @@ bdd_enginet::BDD bdd_enginet::property2BDD(const exprt &expr) /*******************************************************************\ +Function: bdd_enginet::EX + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +bdd_enginet::BDD bdd_enginet::EX(BDD f) +{ + for(const auto &c : constraints_BDDs) + f = f & c; + + // make 'f' be expressed in terms of 'next' variables + BDD p_next = current_to_next(f); + + // now conjoin with transition relation + BDD conjunction = p_next; + + for(const auto &t : transition_BDDs) + conjunction = conjunction & t; + + for(const auto &c : constraints_BDDs) + conjunction = conjunction & c; + + // now project away 'next' variables + BDD pre_image = project_next(conjunction); + + return pre_image; +} + +/*******************************************************************\ + +Function: bdd_enginet::fixedpoint + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +bdd_enginet::BDD bdd_enginet::fixedpoint(std::function tau, BDD x) +{ + // Apply tau(x) until saturation. + while(true) + { + BDD image = tau(x); + + // fixpoint? + if((image == x).is_true()) + return x; // done + + x = image; + } +} + +/*******************************************************************\ + +Function: bdd_enginet::EG + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +bdd_enginet::BDD bdd_enginet::EG(BDD f) +{ + // EG f = f ∧ EX EG f + // Iterate x ∧ EX x until saturation. + auto tau = [this](BDD x) { return x & EX(x); }; + + return fixedpoint(tau, f); +} + +/*******************************************************************\ + +Function: bdd_enginet::EF + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +bdd_enginet::BDD bdd_enginet::EF(BDD f) +{ + // EF f ↔ f ∨ EX EF f + // Iterate x ∨ EX x until saturation. + auto tau = [this](BDD x) { return x | EX(x); }; + + return fixedpoint(tau, f); +} + +/*******************************************************************\ + +Function: bdd_enginet::EU + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +bdd_enginet::BDD bdd_enginet::EU(BDD f1, BDD f2) +{ + // Iterate x ∨ f2 ∨ (f1 ∧ EX x) until saturation + auto tau = [this, f1, f2](BDD x) { return x | f2 | (f1 & EX(x)); }; + + return fixedpoint(tau, mgr.False()); +} + +/*******************************************************************\ + +Function: bdd_enginet::AU + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +bdd_enginet::BDD bdd_enginet::AU(BDD f1, BDD f2) +{ + // Iterate x ∨ f2 ∨ (f1 ∧ AX x) until saturation + auto tau = [this, f1, f2](BDD x) { return x | f2 | (f1 & AX(x)); }; + + return fixedpoint(tau, mgr.False()); +} + +/*******************************************************************\ + Function: bdd_enginet::get_atomic_propositions Inputs: @@ -851,13 +882,8 @@ void bdd_enginet::get_atomic_propositions(const exprt &expr) { if( expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_not || - expr.id() == ID_implies || expr.id() == ID_AG || expr.id() == ID_G || - expr.id() == ID_AF || expr.id() == ID_F || expr.id() == ID_sva_always || - expr.id() == ID_sva_overlapped_implication || - expr.id() == ID_sva_non_overlapped_implication || - expr.id() == ID_sva_nexttime || expr.id() == ID_sva_s_eventually || - expr.id() == ID_sva_until || expr.id() == ID_sva_s_until || - expr.id() == ID_sva_until_with || expr.id() == ID_sva_s_until_with) + expr.id() == ID_implies || is_temporal_operator(expr) || + expr.id() == ID_sva_overlapped_implication) { for(const auto & op : expr.operands()) get_atomic_propositions(op); diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index ae4e7619b..7d4790865 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -1,9 +1,13 @@ IREP_ID_ONE(AG) IREP_ID_ONE(AF) IREP_ID_ONE(AX) +IREP_ID_ONE(AU) +IREP_ID_ONE(AR) IREP_ID_ONE(EG) IREP_ID_ONE(EF) IREP_ID_ONE(EX) +IREP_ID_ONE(EU) +IREP_ID_ONE(ER) IREP_ID_ONE(U) IREP_ID_ONE(R) IREP_ID_ONE(A) diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index f6e1d320d..325a4c25d 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -951,6 +951,13 @@ void smv_typecheckt::typecheck( typecheck(to_unary_expr(expr).op(), expr.type(), mode); } + else if(expr.id() == ID_U || expr.id() == ID_R) + { + auto &binary_expr = to_binary_expr(expr); + expr.type() = bool_typet(); + typecheck(binary_expr.lhs(), expr.type(), mode); + typecheck(binary_expr.rhs(), expr.type(), mode); + } else if(expr.id()==ID_typecast) { } diff --git a/src/temporal-logic/temporal_expr.h b/src/temporal-logic/temporal_expr.h index d22c1ae99..dbafca953 100644 --- a/src/temporal-logic/temporal_expr.h +++ b/src/temporal-logic/temporal_expr.h @@ -166,6 +166,52 @@ static inline U_exprt &to_U_expr(exprt &expr) return static_cast(expr); } +class EU_exprt : public binary_predicate_exprt +{ +public: + explicit EU_exprt(exprt op0, exprt op1) + : binary_predicate_exprt(std::move(op0), ID_EU, std::move(op1)) + { + } +}; + +static inline const EU_exprt &to_EU_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_EU); + EU_exprt::check(expr); + return static_cast(expr); +} + +static inline EU_exprt &to_EU_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_EU); + EU_exprt::check(expr); + return static_cast(expr); +} + +class AU_exprt : public binary_predicate_exprt +{ +public: + explicit AU_exprt(exprt op0, exprt op1) + : binary_predicate_exprt(std::move(op0), ID_AU, std::move(op1)) + { + } +}; + +static inline const AU_exprt &to_AU_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_AU); + AU_exprt::check(expr); + return static_cast(expr); +} + +static inline AU_exprt &to_AU_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_AU); + AU_exprt::check(expr); + return static_cast(expr); +} + class R_exprt : public binary_predicate_exprt { public: @@ -189,6 +235,52 @@ static inline R_exprt &to_R_expr(exprt &expr) return static_cast(expr); } +class ER_exprt : public binary_predicate_exprt +{ +public: + explicit ER_exprt(exprt op0, exprt op1) + : binary_predicate_exprt(std::move(op0), ID_ER, std::move(op1)) + { + } +}; + +static inline const ER_exprt &to_ER_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_ER); + R_exprt::check(expr); + return static_cast(expr); +} + +static inline ER_exprt &to_ER_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_ER); + R_exprt::check(expr); + return static_cast(expr); +} + +class AR_exprt : public binary_predicate_exprt +{ +public: + explicit AR_exprt(exprt op0, exprt op1) + : binary_predicate_exprt(std::move(op0), ID_AR, std::move(op1)) + { + } +}; + +static inline const AR_exprt &to_AR_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_AR); + R_exprt::check(expr); + return static_cast(expr); +} + +static inline AR_exprt &to_AR_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_AR); + R_exprt::check(expr); + return static_cast(expr); +} + class E_exprt : public binary_predicate_exprt { public: @@ -235,6 +327,50 @@ static inline A_exprt &to_A_expr(exprt &expr) return static_cast(expr); } +class AX_exprt : public unary_predicate_exprt +{ +public: + explicit AX_exprt(exprt op) : unary_predicate_exprt(ID_AX, std::move(op)) + { + } +}; + +static inline const AX_exprt &to_AX_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_AX); + AX_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); +} + +static inline AX_exprt &to_AX_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_AX); + AX_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); +} + +class EX_exprt : public unary_predicate_exprt +{ +public: + explicit EX_exprt(exprt op) : unary_predicate_exprt(ID_EX, std::move(op)) + { + } +}; + +static inline const EX_exprt &to_EX_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_EX); + EX_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); +} + +static inline EX_exprt &to_EX_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_EX); + EX_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); +} + class X_exprt : public unary_predicate_exprt { public: diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp index dc77e7aa5..a45a195df 100644 --- a/src/temporal-logic/temporal_logic.cpp +++ b/src/temporal-logic/temporal_logic.cpp @@ -8,15 +8,12 @@ Author: Daniel Kroening, kroening@kroening.com #include "temporal_logic.h" -#include +#include bool is_temporal_operator(const exprt &expr) { - return expr.id() == ID_AG || expr.id() == ID_EG || expr.id() == ID_AF || - expr.id() == ID_EF || expr.id() == ID_AX || expr.id() == ID_EX || - expr.id() == ID_A || expr.id() == ID_E || expr.id() == ID_U || - expr.id() == ID_R || expr.id() == ID_G || expr.id() == ID_F || - expr.id() == ID_X || expr.id() == ID_sva_always || + return is_CTL_operator(expr) || is_LTL_operator(expr) || expr.id() == ID_A || + expr.id() == ID_E || expr.id() == ID_sva_always || expr.id() == ID_sva_always || expr.id() == ID_sva_ranged_always || expr.id() == ID_sva_nexttime || expr.id() == ID_sva_s_nexttime || expr.id() == ID_sva_non_overlapped_implication || @@ -28,18 +25,42 @@ bool is_temporal_operator(const exprt &expr) bool has_temporal_operator(const exprt &expr) { - for(auto subexpr_it = expr.depth_cbegin(), subexpr_end = expr.depth_cend(); - subexpr_it != subexpr_end; - subexpr_it++) - { - if(is_temporal_operator(*subexpr_it)) - return true; - } - - return false; + return has_subexpr(expr, is_temporal_operator); } bool is_exists_path(const exprt &expr) { return expr.id() == ID_sva_cover; } + +bool is_CTL_operator(const exprt &expr) +{ + auto id = expr.id(); + return id == ID_AG || id == ID_EG || id == ID_AF || id == ID_EF || + id == ID_AX || id == ID_EX || id == ID_AU || id == ID_EU || + id == ID_AR || id == ID_ER; +} + +bool is_CTL(const exprt &expr) +{ + auto non_CTL_operator = [](const exprt &expr) { + return is_temporal_operator(expr) && !is_CTL_operator(expr); + }; + + return !has_subexpr(expr, non_CTL_operator); +} + +bool is_LTL_operator(const exprt &expr) +{ + auto id = expr.id(); + return id == ID_G || id == ID_F || id == ID_X || id == ID_U || id == ID_R; +} + +bool is_LTL(const exprt &expr) +{ + auto non_LTL_operator = [](const exprt &expr) { + return is_temporal_operator(expr) && !is_LTL_operator(expr); + }; + + return !has_subexpr(expr, non_LTL_operator); +} diff --git a/src/temporal-logic/temporal_logic.h b/src/temporal-logic/temporal_logic.h index 54392d43a..f12773ece 100644 --- a/src/temporal-logic/temporal_logic.h +++ b/src/temporal-logic/temporal_logic.h @@ -22,4 +22,18 @@ bool is_temporal_operator(const exprt &); /// property. bool is_exists_path(const exprt &); +/// Returns true iff the given expression is a CTL formula +bool is_CTL(const exprt &); + +/// Returns true iff the given expression has a CTL operator +/// as its root +bool is_CTL_operator(const exprt &); + +/// Returns true iff the given expression is an LTL formula +bool is_LTL(const exprt &); + +/// Returns true iff the given expression has an LTL operator +/// as its root +bool is_LTL_operator(const exprt &); + #endif diff --git a/src/trans-netlist/trans_to_netlist.cpp b/src/trans-netlist/trans_to_netlist.cpp index 74dc3ab3c..e7d88e0b9 100644 --- a/src/trans-netlist/trans_to_netlist.cpp +++ b/src/trans-netlist/trans_to_netlist.cpp @@ -345,6 +345,7 @@ void convert_trans_to_netlistt::operator()(const irep_idt &module) if(!has_temporal_operator(phi)) { + // G p dest.properties.emplace(id, netlistt::Gpt{convert(phi)}); } else if( @@ -362,7 +363,17 @@ void convert_trans_to_netlistt::operator()(const irep_idt &module) PRECONDITION(false); }; - dest.properties.emplace(id, netlistt::GFpt{convert(get_psi(phi))}); + auto psi = get_psi(phi); + + if(!has_temporal_operator(psi)) + { + // G F p + dest.properties.emplace(id, netlistt::GFpt{convert(psi)}); + } + else + { + // unsupported + } } else {