From 8147a2afb3ef20eeecc410c3144bbfd5d0509555 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 21 Apr 2024 13:22:37 -0700 Subject: [PATCH] BMC for F phi This adds support for properties of the type F phi and AF p to the BMC engine. --- .../ebmc/smv/bmc_unsupported_property1.desc | 2 +- .../ebmc/smv/bmc_unsupported_property1.smv | 2 +- .../ebmc/smv/bmc_unsupported_property2.desc | 2 +- .../ebmc/smv/bmc_unsupported_property2.smv | 2 +- regression/ebmc/smv/smv_ltlspec4.desc | 13 +++++++ regression/ebmc/smv/smv_ltlspec4.smv | 10 ++++++ src/temporal-logic/normalize_property.cpp | 10 ++++++ src/temporal-logic/normalize_property.h | 2 ++ src/trans-word-level/property.cpp | 35 +++++++++++++++++++ 9 files changed, 74 insertions(+), 4 deletions(-) create mode 100644 regression/ebmc/smv/smv_ltlspec4.desc create mode 100644 regression/ebmc/smv/smv_ltlspec4.smv diff --git a/regression/ebmc/smv/bmc_unsupported_property1.desc b/regression/ebmc/smv/bmc_unsupported_property1.desc index 7a750aa85..b18e1ed1a 100644 --- a/regression/ebmc/smv/bmc_unsupported_property1.desc +++ b/regression/ebmc/smv/bmc_unsupported_property1.desc @@ -3,7 +3,7 @@ bmc_unsupported_property1.smv ^EXIT=10$ ^SIGNAL=0$ -^\[main::spec1\] !G main::var::x = FALSE: FAILURE: property not supported by BMC engine$ +^\[main::spec1\] EG main::var::x = FALSE: FAILURE: property not supported by BMC engine$ ^\[main::spec2\] G main::var::x = FALSE: REFUTED$ -- ^warning: ignoring diff --git a/regression/ebmc/smv/bmc_unsupported_property1.smv b/regression/ebmc/smv/bmc_unsupported_property1.smv index 03ed490fe..b640b7440 100644 --- a/regression/ebmc/smv/bmc_unsupported_property1.smv +++ b/regression/ebmc/smv/bmc_unsupported_property1.smv @@ -4,5 +4,5 @@ VAR x : boolean; ASSIGN init(x) := 1; -LTLSPEC !G x=0 +SPEC EG x=0 LTLSPEC G x=0 diff --git a/regression/ebmc/smv/bmc_unsupported_property2.desc b/regression/ebmc/smv/bmc_unsupported_property2.desc index 83e3c7eb3..fcb52b210 100644 --- a/regression/ebmc/smv/bmc_unsupported_property2.desc +++ b/regression/ebmc/smv/bmc_unsupported_property2.desc @@ -3,7 +3,7 @@ bmc_unsupported_property2.smv ^EXIT=10$ ^SIGNAL=0$ -^\[main::spec1\] !G main::var::x = FALSE: FAILURE: property not supported by BMC engine$ +^\[main::spec1\] EG main::var::x = FALSE: FAILURE: property not supported by BMC engine$ ^\[main::spec2\] G main::var::x = TRUE: PROVED up to bound 1$ -- ^warning: ignoring diff --git a/regression/ebmc/smv/bmc_unsupported_property2.smv b/regression/ebmc/smv/bmc_unsupported_property2.smv index 638a4c008..2a7b155f1 100644 --- a/regression/ebmc/smv/bmc_unsupported_property2.smv +++ b/regression/ebmc/smv/bmc_unsupported_property2.smv @@ -5,5 +5,5 @@ VAR x : boolean; ASSIGN init(x) := 1; ASSIGN next(x) := x; -LTLSPEC !G x=0 -- unsupported +SPEC EG x=0 -- unsupported LTLSPEC G x=1 -- should pass diff --git a/regression/ebmc/smv/smv_ltlspec4.desc b/regression/ebmc/smv/smv_ltlspec4.desc new file mode 100644 index 000000000..93b6fff8a --- /dev/null +++ b/regression/ebmc/smv/smv_ltlspec4.desc @@ -0,0 +1,13 @@ +CORE broken-smt-backend +smv_ltlspec4.smv +--bound 10 --numbered-trace +^EXIT=10$ +^SIGNAL=0$ +^\[main::spec1\] F main::var::x = 0: REFUTED$ +^main::var::x@0 = 1$ +^main::var::x@1 = 2$ +^main::var::x@2 = 2$ +^\[main::spec2\] F main::var::x = 2: PROVED up to bound 10$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc/smv/smv_ltlspec4.smv b/regression/ebmc/smv/smv_ltlspec4.smv new file mode 100644 index 000000000..6b93e1a35 --- /dev/null +++ b/regression/ebmc/smv/smv_ltlspec4.smv @@ -0,0 +1,10 @@ +MODULE main + +VAR x : 0..2; + +ASSIGN + init(x) := 1; + next(x) := 2; + +LTLSPEC F x=0 -- fails +LTLSPEC F x=2 -- holds diff --git a/src/temporal-logic/normalize_property.cpp b/src/temporal-logic/normalize_property.cpp index b5fc35ce3..1843cd322 100644 --- a/src/temporal-logic/normalize_property.cpp +++ b/src/temporal-logic/normalize_property.cpp @@ -36,6 +36,16 @@ exprt normalize_pre_not(not_exprt expr) { return to_not_expr(op).op(); } + else if(op.id() == ID_G) + { + // ¬Gφ --> F¬φ + return F_exprt{not_exprt{to_G_expr(op).op()}}; + } + else if(op.id() == ID_F) + { + // ¬Fφ --> G¬φ + return G_exprt{not_exprt{to_F_expr(op).op()}}; + } return std::move(expr); } diff --git a/src/temporal-logic/normalize_property.h b/src/temporal-logic/normalize_property.h index b0c37269d..5764c640b 100644 --- a/src/temporal-logic/normalize_property.h +++ b/src/temporal-logic/normalize_property.h @@ -16,6 +16,8 @@ Author: Daniel Kroening, dkr@amazon.com /// ¬(a ∨ b) --> ¬a ∧ ¬b /// ¬(a ∧ b) --> ¬a ∨ ¬b /// ¬¬φ --> φ +/// ¬Gφ --> F¬φ +/// ¬Fφ --> G¬φ exprt normalize_property(exprt); #endif diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp index 6061b10cd..e9c7c356e 100644 --- a/src/trans-word-level/property.cpp +++ b/src/trans-word-level/property.cpp @@ -54,6 +54,10 @@ bool bmc_supports_property(const exprt &expr) return true; else if(expr.id() == ID_G) return true; + else if(expr.id() == ID_AF) + return true; + else if(expr.id() == ID_F) + return true; else if(expr.id() == ID_X) return bmc_supports_property(to_X_expr(expr).op()); else if(expr.id() == ID_sva_always) @@ -117,6 +121,37 @@ static void property_obligations_rec( property_obligations_rec(phi, solver, c, no_timeframes, ns, obligations); } } + else if( + property_expr.id() == ID_AF || property_expr.id() == ID_F || + property_expr.id() == ID_sva_s_eventually) + { + const auto &phi = to_unary_expr(property_expr).op(); + + // Counterexamples to Fφ must have a loop. + // We consider l-k loops with l