SVA/LTL property instrumentation

kroening · kroening · commit 40f22febb8f6 · 2025-03-29T13:52:15.000-07:00
diff --git a/CHANGELOG b/CHANGELOG
@@ -10,6 +10,7 @@
 * SMV: LTL V operator, xnor operator
 * SMV: word types and operators
 * --smv-word-level outputs the model as word-level SMV
+* word-level BMC: LTL/SVA to Buechi with --buechi
 
 # EBMC 5.5
 
diff --git a/regression/ebmc/Buechi/FGp1.desc b/regression/ebmc/Buechi/FGp1.desc
@@ -0,0 +1,9 @@
+CORE
+FGp1.smv
+--buechi --bound 2
+^\[.*\] F G p: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc/Buechi/FGp1.smv b/regression/ebmc/Buechi/FGp1.smv
@@ -0,0 +1,9 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+-- should pass
+LTLSPEC F G p
diff --git a/regression/ebmc/Buechi/Fp1.desc b/regression/ebmc/Buechi/Fp1.desc
@@ -0,0 +1,9 @@
+CORE
+Fp1.smv
+--buechi --bound 2
+^\[.*\] F p: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc/Buechi/Fp1.smv b/regression/ebmc/Buechi/Fp1.smv
@@ -0,0 +1,9 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+-- should pass
+LTLSPEC F p
diff --git a/regression/ebmc/Buechi/GFp1.desc b/regression/ebmc/Buechi/GFp1.desc
@@ -0,0 +1,9 @@
+CORE
+GFp1.smv
+--buechi --bound 2
+^\[.*\] G F p: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc/Buechi/GFp1.smv b/regression/ebmc/Buechi/GFp1.smv
@@ -0,0 +1,9 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := !p;
+
+-- should pass
+LTLSPEC G F p
diff --git a/regression/ebmc/Buechi/Gp1.desc b/regression/ebmc/Buechi/Gp1.desc
@@ -0,0 +1,9 @@
+CORE
+Gp1.smv
+--buechi --bound 2
+^\[.*\] G p: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc/Buechi/Gp1.smv b/regression/ebmc/Buechi/Gp1.smv
@@ -0,0 +1,9 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := TRUE;
+       next(p) := TRUE;
+
+-- should pass
+LTLSPEC G p
diff --git a/regression/ebmc/Buechi/Xp1.desc b/regression/ebmc/Buechi/Xp1.desc
@@ -0,0 +1,9 @@
+CORE
+Xp1.smv
+--buechi --bound 2
+^\[.*\] X p: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc/Buechi/Xp1.smv b/regression/ebmc/Buechi/Xp1.smv
@@ -0,0 +1,9 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+-- should pass
+LTLSPEC X p
diff --git a/regression/ebmc/Buechi/and1.desc b/regression/ebmc/Buechi/and1.desc
@@ -0,0 +1,9 @@
+CORE
+and1.smv
+--buechi --bound 2
+^\[.*\] X p & X q: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc/Buechi/and1.smv b/regression/ebmc/Buechi/and1.smv
@@ -0,0 +1,15 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := FALSE;
+       next(q) := TRUE;
+
+-- should pass
+LTLSPEC X p & X q
+
diff --git a/regression/ebmc/Buechi/and2.desc b/regression/ebmc/Buechi/and2.desc
@@ -0,0 +1,9 @@
+CORE
+and2.smv
+--buechi --bound 2
+^\[.*\] X \(p & q\): PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc/Buechi/and2.smv b/regression/ebmc/Buechi/and2.smv
@@ -0,0 +1,15 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := FALSE;
+       next(q) := TRUE;
+
+-- should pass
+LTLSPEC X (p & q)
+
diff --git a/regression/ebmc/Buechi/iff1.desc b/regression/ebmc/Buechi/iff1.desc
@@ -0,0 +1,9 @@
+CORE
+iff1.smv
+--buechi --bound 2
+^\[.*\] X p <-> X q: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc/Buechi/iff1.smv b/regression/ebmc/Buechi/iff1.smv
@@ -0,0 +1,14 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := TRUE;
+       next(p) := FALSE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := TRUE;
+       next(q) := FALSE;
+
+-- should pass
+LTLSPEC X p <-> X q
diff --git a/regression/ebmc/Buechi/iff2.desc b/regression/ebmc/Buechi/iff2.desc
@@ -0,0 +1,9 @@
+CORE
+iff2.smv
+--buechi --bound 2
+^\[.*\] X \(p <-> q\): PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc/Buechi/iff2.smv b/regression/ebmc/Buechi/iff2.smv
@@ -0,0 +1,14 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := TRUE;
+       next(p) := FALSE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := TRUE;
+       next(q) := FALSE;
+
+-- should pass
+LTLSPEC X (p <-> q)
diff --git a/regression/ebmc/Buechi/implies1.desc b/regression/ebmc/Buechi/implies1.desc
@@ -0,0 +1,9 @@
+CORE
+implies1.smv
+--buechi --bound 2
+^\[.*\] X p -> X q: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc/Buechi/implies1.smv b/regression/ebmc/Buechi/implies1.smv
@@ -0,0 +1,14 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := TRUE;
+       next(p) := FALSE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := TRUE;
+       next(q) := FALSE;
+
+-- should pass
+LTLSPEC X p -> X q
diff --git a/regression/ebmc/Buechi/implies2.desc b/regression/ebmc/Buechi/implies2.desc
@@ -0,0 +1,9 @@
+CORE
+implies2.smv
+--buechi --bound 2
+^\[.*\] X \(p -> q\): PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc/Buechi/implies2.smv b/regression/ebmc/Buechi/implies2.smv
@@ -0,0 +1,14 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := TRUE;
+       next(p) := FALSE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := TRUE;
+       next(q) := FALSE;
+
+-- should pass
+LTLSPEC X (p -> q)
diff --git a/regression/ebmc/Buechi/or1.desc b/regression/ebmc/Buechi/or1.desc
@@ -0,0 +1,9 @@
+CORE
+or1.smv
+--buechi --bound 2
+^\[.*\] X p \| X q: PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc/Buechi/or1.smv b/regression/ebmc/Buechi/or1.smv
@@ -0,0 +1,14 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := TRUE;
+       next(q) := FALSE;
+
+-- should pass
+LTLSPEC X p | X q
diff --git a/regression/ebmc/Buechi/or2.desc b/regression/ebmc/Buechi/or2.desc
@@ -0,0 +1,9 @@
+CORE
+or2.smv
+--buechi --bound 2
+^\[.*\] X \(p \| q\): PROVED up to bound 2$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc/Buechi/or2.smv b/regression/ebmc/Buechi/or2.smv
@@ -0,0 +1,14 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := TRUE;
+       next(q) := FALSE;
+
+-- should pass
+LTLSPEC X (p | q)
diff --git a/src/ebmc/Makefile b/src/ebmc/Makefile
@@ -17,6 +17,7 @@ SRC = \
       ebmc_properties.cpp \
       ebmc_solver_factory.cpp \
       instrument_past.cpp \
+      instrument_buechi.cpp \
       k_induction.cpp \
       liveness_to_safety.cpp \
       live_signal.cpp \
diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "ebmc_base.h"
 #include "ebmc_error.h"
 #include "ebmc_version.h"
+#include "instrument_buechi.h"
 #include "liveness_to_safety.h"
 #include "netlist.h"
 #include "neural_liveness.h"
@@ -237,6 +238,10 @@ int ebmc_parse_optionst::doit()
       return 0;
     }
 
+    // LTL/SVA to Buechi?
+    if(cmdline.isset("buechi"))
+      instrument_buechi(transition_system, properties, ui_message_handler);
+
     // possibly apply liveness-to-safety
     if(cmdline.isset("liveness-to-safety"))
       liveness_to_safety(transition_system, properties);
@@ -371,6 +376,7 @@ void ebmc_parse_optionst::help()
     " {y--show-properties}           \t list the properties in the model\n"
     " {y--property} {uid}            \t check the property with given ID\n"
     " {y--liveness-to-safety}        \t translate liveness properties to safety properties\n"
+    " {y--buechi}                    \t translate LTL/SVA properties to Buechi acceptance\n"
     "\n"
     "Methods:\n"
     " {y--k-induction}               \t do k-induction with k=bound\n"
diff --git a/src/ebmc/ebmc_parse_options.h b/src/ebmc/ebmc_parse_options.h
@@ -49,7 +49,7 @@ class ebmc_parse_optionst:public parse_options_baset
         "(random-traces)(trace-steps):(random-seed):(traces):"
         "(random-trace)(random-waveform)"
         "(bmc-with-assumptions)"
-        "(liveness-to-safety)"
+        "(liveness-to-safety)(buechi)"
         "I:D:(preprocess)(systemverilog)(vl2smv-extensions)"
         "(warn-implicit-nets)",
         argc,
diff --git a/src/ebmc/instrument_buechi.cpp b/src/ebmc/instrument_buechi.cpp
diff --git a/src/ebmc/instrument_buechi.h b/src/ebmc/instrument_buechi.h
diff --git a/src/temporal-logic/Makefile b/src/temporal-logic/Makefile
diff --git a/src/temporal-logic/hoa.cpp b/src/temporal-logic/hoa.cpp
diff --git a/src/temporal-logic/hoa.h b/src/temporal-logic/hoa.h
diff --git a/src/temporal-logic/ltl_sva_to_string.cpp b/src/temporal-logic/ltl_sva_to_string.cpp
diff --git a/src/temporal-logic/ltl_sva_to_string.h b/src/temporal-logic/ltl_sva_to_string.h
diff --git a/src/temporal-logic/ltl_to_buechi.cpp b/src/temporal-logic/ltl_to_buechi.cpp
diff --git a/src/temporal-logic/ltl_to_buechi.h b/src/temporal-logic/ltl_to_buechi.h
diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp
diff --git a/src/temporal-logic/temporal_logic.h b/src/temporal-logic/temporal_logic.h
diff --git a/unit/Makefile b/unit/Makefile
diff --git a/unit/temporal-logic/ltl_sva_to_string.cpp b/unit/temporal-logic/ltl_sva_to_string.cpp
