(codethorn) merge with dev branch

CODETHORN-70
SNSerHello · Oct 11, 2022 · 1268584 · 1268584
2 parents 5d7f037 + b779ec9
commit 1268584
Show file tree

Hide file tree

Showing 18 changed files with 42 additions and 16 deletions.
diff --git a/tools/CodeThorn/src/CodeThornCommandLineOptions.C b/tools/CodeThorn/src/CodeThornCommandLineOptions.C
@@ -1,4 +1,7 @@
 #include "sage3basic.h"
+// required for checking of: HAVE_SPOT
+#include "rose_config.h"
+
 #include "CodeThornException.h"
 #include "CodeThornCommandLineOptions.h"
 #include "CppStdUtilities.h"
@@ -7,9 +10,6 @@
 #include <sstream>
 #include <iostream>
 
-// required for checking of: HAVE_SPOT, HAVE_Z3
-#include "rose_config.h"
-
 #include "Rose/Diagnostics.h"
 using namespace Sawyer::Message;
 using namespace std;

diff --git a/tools/CodeThorn/src/LTLThornLib.C b/tools/CodeThorn/src/LTLThornLib.C
@@ -1,4 +1,5 @@
 #include "sage3basic.h"
+#include "rose_config.h"
 
 #include <string> // std::string, std::stoi
 #include <regex>

diff --git a/tools/CodeThorn/src/PropertyValueTable.C b/tools/CodeThorn/src/PropertyValueTable.C
@@ -1,3 +1,5 @@
+#include "sage3basic.h"
+
 #include "PropertyValueTable.h"
 #include "CodeThornException.h"
 #include "Miscellaneous2.h"

diff --git a/tools/CodeThorn/src/Thorn1CommandLineOptions.C b/tools/CodeThorn/src/Thorn1CommandLineOptions.C
@@ -1,4 +1,7 @@
 #include "sage3basic.h"
+// required for checking of: HAVE_SPOT, HAVE_Z3
+#include "rose_config.h"
+
 #include "CodeThornException.h"
 #include "CodeThornCommandLineOptions.h"
 #include "CppStdUtilities.h"
@@ -7,9 +10,6 @@
 #include <sstream>
 #include <iostream>
 
-// required for checking of: HAVE_SPOT, HAVE_Z3
-#include "rose_config.h"
-
 #include "Rose/Diagnostics.h"
 using namespace Sawyer::Message;
 using namespace std;

diff --git a/tools/CodeThorn/src/ltlthorn-lib/CounterexampleAnalyzer.C b/tools/CodeThorn/src/ltlthorn-lib/CounterexampleAnalyzer.C
@@ -1,4 +1,6 @@
 // Author: Marc Jasper, 2014, 2015.
+#include "sage3basic.h"
+#include "rose_config.h"
 
 #ifdef HAVE_SPOT
 

diff --git a/tools/CodeThorn/src/ltlthorn-lib/CounterexampleAnalyzer.h b/tools/CodeThorn/src/ltlthorn-lib/CounterexampleAnalyzer.h
@@ -27,9 +27,9 @@ namespace CodeThorn {
  enum IoType {IO_TYPE_UNKNOWN,IO_TYPE_INPUT,IO_TYPE_OUTPUT,IO_TYPE_ERROR};
 
  typedef std::pair<int, IoType> CeIoVal;
- typedef std::pair<list<CeIoVal> , std::list<CeIoVal> > PrefixAndCycle;
+ typedef std::pair<std::list<CeIoVal> , std::list<CeIoVal> > PrefixAndCycle;
  typedef std::list<std::unordered_set<EStatePtr> > StateSets;
- typedef std::unordered_map<EStatePtr, list<int> > InputsAtEState;
+ typedef std::unordered_map<EStatePtr, std::list<int> > InputsAtEState;
 
  /*! 
  * \author Marc Jasper
@@ -63,7 +63,7 @@ namespace CodeThorn {
  public:
  // initializing the CounterexampleAnalyzer, using "analyzer" to trace paths of the original program
  CounterexampleAnalyzer(IOAnalyzer* analyzer);
- CounterexampleAnalyzer(IOAnalyzer* analyzer, stringstream* csvOutput);
+ CounterexampleAnalyzer(IOAnalyzer* analyzer, std::stringstream* csvOutput);
  // Check whether or not the "counterexample" is spurious. 
  // If "returnSpuriousLabel" is set to true: In the case of a spurious counterexample, the result includes a label that should not 
  // be reachable according to the original program but is reachable in the counterexample
@@ -108,29 +108,29 @@ namespace CodeThorn {
  // marks index in "v" as true iff the entry in "erroneousBranches" that corresponds to "eState" containts (index+1) in its mapping.
 
  //std::vector<bool> setErrorBranches(vector<bool> v, EStatePtr eState, InputsAtEState erroneousBranches);
- std::vector<bool> setErrorBranches(vector<bool> v, EStatePtr eState);
- std::list<pair<EStatePtr, int> > removeTraceLeadingToErrorState(EStatePtr errorState, TransitionGraph* stg);
+ std::vector<bool> setErrorBranches(std::vector<bool> v, EStatePtr eState);
+ std::list<std::pair<EStatePtr, int> > removeTraceLeadingToErrorState(EStatePtr errorState, TransitionGraph* stg);
 
  // Adds all output states in the prefix to "startAndOuputStatesPrefix" and returns the set.
  EStatePtrSet addAllPrefixOutputStates(EStatePtrSet& startAndOuputStatesPrefix, TransitionGraph* model);
  // identify states needed to disconnect the concrete prefix and the over-approximated part in the initial abstract model
- pair<EStatePtrSet, EStatePtrSet> getConcreteOutputAndAbstractInput(TransitionGraph* model);
+ std::pair<EStatePtrSet, EStatePtrSet> getConcreteOutputAndAbstractInput(TransitionGraph* model);
  // sort the |<input_alphabet>| abstract input states according to their input value and insert them into the vector "v". 
- vector<EStatePtr> sortAbstractInputStates(vector<EStatePtr> v, EStatePtrSet abstractInputStates);
+ std::vector<EStatePtr> sortAbstractInputStates(std::vector<EStatePtr> v, EStatePtrSet abstractInputStates);
  // deprecated: now implemented as function of EState ("isRersTopified(...)");
  bool isPrefixState(EStatePtr state);
  // prints #transitions, details about states and #counterexamples analyzed
  void printStgSizeAndCeCount(TransitionGraph* model, int counterexampleCount, int property);
 
  //for debugging purposes
  std::string ceIoValToString(CeIoVal& ioVal);
- std::string ioErrTraceToString(list<pair<int, IoType> > trace);
+ std::string ioErrTraceToString(std::list<std::pair<int, IoType> > trace);
  void writeDotGraphToDisk(std::string filename, Visualizer& visualizer);
 
  CodeThorn::VariableId globalVarIdByName(std::string);
 
  IOAnalyzer* _analyzer;
- stringstream* _csvOutput;
+ std::stringstream* _csvOutput;
  int _maxCounterexamples;
  InputsAtEState _erroneousBranches;
  };

diff --git a/tools/CodeThorn/src/ltlthorn-lib/ParProAutomata.C b/tools/CodeThorn/src/ltlthorn-lib/ParProAutomata.C
@@ -1,4 +1,6 @@
 #include "sage3basic.h"
+#include "rose_config.h"
+
 #include "CodeThornCommandLineOptions.h"
 #include "ParProAutomata.h"
 #include "DotGraphCfgFrontend.h"

diff --git a/tools/CodeThorn/src/ltlthorn-lib/ParProExplorer.C b/tools/CodeThorn/src/ltlthorn-lib/ParProExplorer.C
@@ -1,14 +1,19 @@
 // Author: Marc Jasper, 2016.
 
+#include "sage3basic.h"
+#include "rose_config.h"
+
 #include "ParProExplorer.h"
 #include "LtsminConnection.h"
 #include "ParProAutomataGenerator.h"
 
-
 using namespace CodeThorn;
 using namespace std;
 
 #ifdef HAVE_SPOT
+
+#include "SpotState.h" // requires HAVE_SPOT to be defined
+
 /*! 
  * \author Marc Jasper
  * \date 2016.

diff --git a/tools/CodeThorn/src/ltlthorn-lib/ParProSpotState.C b/tools/CodeThorn/src/ltlthorn-lib/ParProSpotState.C
@@ -1,4 +1,5 @@
 #include "sage3basic.h"
+#include "rose_config.h"
 #ifdef HAVE_SPOT
 
 #include "ParProSpotState.h"

diff --git a/tools/CodeThorn/src/ltlthorn-lib/ParProSpotSuccIter.C b/tools/CodeThorn/src/ltlthorn-lib/ParProSpotSuccIter.C
@@ -1,4 +1,5 @@
 #include "sage3basic.h"
+#include "rose_config.h"
 #ifdef HAVE_SPOT
 
 #include "ParProSpotSuccIter.h"

diff --git a/tools/CodeThorn/src/ltlthorn-lib/ParProSpotTgba.C b/tools/CodeThorn/src/ltlthorn-lib/ParProSpotTgba.C
@@ -1,4 +1,5 @@
 #include "sage3basic.h"
+#include "rose_config.h"
 #ifdef HAVE_SPOT
 
 #include "ParProSpotTgba.h"

diff --git a/tools/CodeThorn/src/ltlthorn-lib/SpotConnection.C b/tools/CodeThorn/src/ltlthorn-lib/SpotConnection.C
@@ -1,5 +1,7 @@
 #include "sage3basic.h"
+#include "rose_config.h"
 #include "SpotConnection.h"
+
 using namespace std;
 using namespace CodeThorn;
 

diff --git a/tools/CodeThorn/src/ltlthorn-lib/SpotMiscellaneous.C b/tools/CodeThorn/src/ltlthorn-lib/SpotMiscellaneous.C
@@ -1,4 +1,5 @@
 #include "sage3basic.h"
+#include "rose_config.h"
 #ifdef HAVE_SPOT
 
 #include "SpotMiscellaneous.h"

diff --git a/tools/CodeThorn/src/ltlthorn-lib/SpotRenameVisitor.C b/tools/CodeThorn/src/ltlthorn-lib/SpotRenameVisitor.C
@@ -1,4 +1,5 @@
 #include "sage3basic.h"
+#include "rose_config.h"
 #ifdef HAVE_SPOT
 
 #include "SpotRenameVisitor.h"

diff --git a/tools/CodeThorn/src/ltlthorn-lib/SpotState.C b/tools/CodeThorn/src/ltlthorn-lib/SpotState.C
@@ -1,4 +1,5 @@
 #include "sage3basic.h"
+#include "rose_config.h"
 #ifdef HAVE_SPOT
 
 #include "SpotState.h"

diff --git a/tools/CodeThorn/src/ltlthorn-lib/SpotState.h b/tools/CodeThorn/src/ltlthorn-lib/SpotState.h
@@ -1,3 +1,4 @@
+
 #ifdef HAVE_SPOT
 
 #ifndef SPOT_STATE_H

diff --git a/tools/CodeThorn/src/ltlthorn-lib/SpotSuccIter.C b/tools/CodeThorn/src/ltlthorn-lib/SpotSuccIter.C
@@ -1,4 +1,7 @@
 #include "sage3basic.h"
+// required for checking of: HAVE_SPOT
+#include "rose_config.h"
+
 #ifdef HAVE_SPOT
 
 #include <list>

diff --git a/tools/CodeThorn/src/ltlthorn-lib/SpotTgba.C b/tools/CodeThorn/src/ltlthorn-lib/SpotTgba.C
@@ -1,4 +1,6 @@
 #include "sage3basic.h"
+// required for checking of: HAVE_SPOT
+#include "rose_config.h"
 #ifdef HAVE_SPOT
 
 #include "SpotTgba.h"