sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

added more interfaces to AbstractModelChecker.

main
gereon 13 years ago
parent
4389f6ba5b
commit
5bb71a28e9
16 changed files with 28 additions and 25 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/formula/AbstractFormula.h
  2. 2
      src/formula/AbstractPathFormula.h
  3. 2
      src/formula/AbstractStateFormula.h
  4. 2
      src/formula/And.h
  5. 2
      src/formula/Ap.h
  6. 2
      src/formula/BoundedEventually.h
  7. 3
      src/formula/BoundedNaryUntil.h
  8. 3
      src/formula/BoundedUntil.h
  9. 2
      src/formula/Eventually.h
  10. 9
      src/formula/Formulas.h
  11. 1
      src/formula/Globally.h
  12. 2
      src/formula/Not.h
  13. 2
      src/formula/PathBoundOperator.h
  14. 13
      src/modelchecker/AbstractModelChecker.h
  15. 3
      src/modelchecker/DtmcPrctlModelChecker.h
  16. 3
      src/modelchecker/ForwardDeclarations.h

2
src/formula/AbstractFormula.h
View File

@ -14,7 +14,7 @@ namespace storm { namespace formula {
template <class T> class AbstractFormula; template <class T> class AbstractFormula;
}} }}
#include "src/modelchecker/AbstractModelChecker.h"
#include "src/modelchecker/ForwardDeclarations.h"
#include "src/formula/AbstractFormulaChecker.h" #include "src/formula/AbstractFormulaChecker.h"
namespace storm { namespace storm {

2
src/formula/AbstractPathFormula.h
View File

@ -13,7 +13,7 @@ template <class T> class AbstractPathFormula;
}} }}
#include "src/formula/AbstractFormula.h" #include "src/formula/AbstractFormula.h"
#include "src/modelchecker/AbstractModelChecker.h"
#include "src/modelchecker/ForwardDeclarations.h"
#include <vector> #include <vector>
#include <iostream> #include <iostream>

2
src/formula/AbstractStateFormula.h
View File

@ -14,7 +14,7 @@ template <class T> class AbstractStateFormula;
#include "src/formula/AbstractFormula.h" #include "src/formula/AbstractFormula.h"
#include "src/storage/BitVector.h" #include "src/storage/BitVector.h"
#include "src/modelchecker/AbstractModelChecker.h"
#include "src/modelchecker/ForwardDeclarations.h"
namespace storm { namespace storm {
namespace formula { namespace formula {

2
src/formula/And.h
View File

@ -10,7 +10,7 @@
#include "src/formula/AbstractStateFormula.h" #include "src/formula/AbstractStateFormula.h"
#include "src/formula/AbstractFormulaChecker.h" #include "src/formula/AbstractFormulaChecker.h"
#include "src/modelchecker/AbstractModelChecker.h"
#include "src/modelchecker/ForwardDeclarations.h"
#include <string> #include <string>
namespace storm { namespace storm {

2
src/formula/Ap.h
View File

@ -10,7 +10,7 @@
#include "src/formula/AbstractStateFormula.h" #include "src/formula/AbstractStateFormula.h"
#include "src/formula/AbstractFormulaChecker.h" #include "src/formula/AbstractFormulaChecker.h"
#include "src/modelchecker/AbstractModelChecker.h"
#include "src/modelchecker/ForwardDeclarations.h"
namespace storm { namespace storm {
namespace formula { namespace formula {

2
src/formula/BoundedEventually.h
View File

@ -13,7 +13,7 @@
#include "src/formula/AbstractFormulaChecker.h" #include "src/formula/AbstractFormulaChecker.h"
#include "boost/integer/integer_mask.hpp" #include "boost/integer/integer_mask.hpp"
#include <string> #include <string>
#include "src/modelchecker/AbstractModelChecker.h"
#include "src/modelchecker/ForwardDeclarations.h"
namespace storm { namespace storm {

3
src/formula/BoundedNaryUntil.h
View File

@ -10,13 +10,12 @@
#include "src/formula/AbstractPathFormula.h" #include "src/formula/AbstractPathFormula.h"
#include "src/formula/AbstractStateFormula.h" #include "src/formula/AbstractStateFormula.h"
#include "src/modelchecker/AbstractModelChecker.h"
#include "boost/integer/integer_mask.hpp" #include "boost/integer/integer_mask.hpp"
#include <string> #include <string>
#include <vector> #include <vector>
#include <tuple> #include <tuple>
#include <sstream> #include <sstream>
#include "src/formula/AbstractFormulaChecker.h"
#include "src/modelchecker/ForwardDeclarations.h"
namespace storm { namespace storm {
namespace formula { namespace formula {

3
src/formula/BoundedUntil.h
View File

@ -10,10 +10,9 @@
#include "src/formula/AbstractPathFormula.h" #include "src/formula/AbstractPathFormula.h"
#include "src/formula/AbstractStateFormula.h" #include "src/formula/AbstractStateFormula.h"
#include "src/modelchecker/AbstractModelChecker.h"
#include "boost/integer/integer_mask.hpp" #include "boost/integer/integer_mask.hpp"
#include <string> #include <string>
#include "src/formula/AbstractFormulaChecker.h"
#include "src/modelchecker/ForwardDeclarations.h"
namespace storm { namespace storm {
namespace formula { namespace formula {

2
src/formula/Eventually.h
View File

@ -10,7 +10,7 @@
#include "src/formula/AbstractPathFormula.h" #include "src/formula/AbstractPathFormula.h"
#include "src/formula/AbstractStateFormula.h" #include "src/formula/AbstractStateFormula.h"
#include "src/modelchecker/AbstractModelChecker.h"
#include "src/modelchecker/ForwardDeclarations.h"
namespace storm { namespace storm {

9
src/formula/Formulas.h
View File

@ -10,11 +10,6 @@
#include "modelchecker/ForwardDeclarations.h" #include "modelchecker/ForwardDeclarations.h"
#include "AbstractFormula.h"
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
#include "And.h" #include "And.h"
#include "Ap.h" #include "Ap.h"
#include "BoundedUntil.h" #include "BoundedUntil.h"
@ -36,6 +31,10 @@
#include "RewardNoBoundOperator.h" #include "RewardNoBoundOperator.h"
#include "SteadyStateOperator.h" #include "SteadyStateOperator.h"
#include "AbstractFormula.h"
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
#include "modelchecker/DtmcPrctlModelChecker.h" #include "modelchecker/DtmcPrctlModelChecker.h"
#endif /* STORM_FORMULA_FORMULAS_H_ */ #endif /* STORM_FORMULA_FORMULAS_H_ */

1
src/formula/Globally.h
View File

@ -11,6 +11,7 @@
#include "AbstractPathFormula.h" #include "AbstractPathFormula.h"
#include "AbstractStateFormula.h" #include "AbstractStateFormula.h"
#include "src/formula/AbstractFormulaChecker.h" #include "src/formula/AbstractFormulaChecker.h"
#include "src/modelchecker/ForwardDeclarations.h"
namespace storm { namespace storm {

2
src/formula/Not.h
View File

@ -10,7 +10,7 @@
#include "AbstractStateFormula.h" #include "AbstractStateFormula.h"
#include "src/formula/AbstractFormulaChecker.h" #include "src/formula/AbstractFormulaChecker.h"
#include "src/modelchecker/AbstractModelChecker.h"
#include "src/modelchecker/ForwardDeclarations.h"
namespace storm { namespace storm {

2
src/formula/PathBoundOperator.h
View File

@ -11,7 +11,7 @@
#include "src/formula/AbstractStateFormula.h" #include "src/formula/AbstractStateFormula.h"
#include "src/formula/AbstractPathFormula.h" #include "src/formula/AbstractPathFormula.h"
#include "src/formula/AbstractFormulaChecker.h" #include "src/formula/AbstractFormulaChecker.h"
#include "src/modelchecker/AbstractModelChecker.h"
#include "src/modelchecker/ForwardDeclarations.h"
#include "src/utility/ConstTemplates.h" #include "src/utility/ConstTemplates.h"
namespace storm { namespace storm {

13
src/modelchecker/AbstractModelChecker.h
View File

@ -12,9 +12,7 @@ namespace storm { namespace modelChecker {
template <class Type> class AbstractModelChecker; template <class Type> class AbstractModelChecker;
}} }}
//#include "src/formula/Formulas.h"
#include "src/formula/Or.h"
#include "src/formula/Ap.h"
#include "src/formula/Formulas.h"
#include "src/storage/BitVector.h" #include "src/storage/BitVector.h"
#include <iostream> #include <iostream>
@ -33,8 +31,13 @@ namespace modelChecker {
*/ */
template<class Type> template<class Type>
class AbstractModelChecker : class AbstractModelChecker :
public virtual storm::formula::IOrModelChecker<Type>,
public virtual storm::formula::IApModelChecker<Type>
public virtual storm::formula::IApModelChecker<Type>,
public virtual storm::formula::IAndModelChecker<Type>,
public virtual storm::formula::IEventuallyModelChecker<Type>,
public virtual storm::formula::IGloballyModelChecker<Type>,
public virtual storm::formula::INextModelChecker<Type>,
public virtual storm::formula::INotModelChecker<Type>,
public virtual storm::formula::IOrModelChecker<Type>
{ {
public: public:

3
src/modelchecker/DtmcPrctlModelChecker.h
View File

@ -41,8 +41,7 @@ template<class Type>
class DtmcPrctlModelChecker : class DtmcPrctlModelChecker :
public virtual AbstractModelChecker<Type>, public virtual AbstractModelChecker<Type>,
public virtual storm::formula::INoBoundOperatorModelChecker<Type>, public virtual storm::formula::INoBoundOperatorModelChecker<Type>,
public virtual storm::formula::IReachabilityRewardModelChecker<Type>,
public virtual storm::formula::IEventuallyModelChecker<Type>
public virtual storm::formula::IReachabilityRewardModelChecker<Type>
{ {
public: public:
/*! /*!

3
src/modelchecker/ForwardDeclarations.h
View File

@ -13,6 +13,9 @@ namespace storm {
namespace modelChecker { namespace modelChecker {
template <class Type>
class AbstractModelChecker;
template <class Type> template <class Type>
class DtmcPrctlModelChecker; class DtmcPrctlModelChecker;

Write Preview
Loading…
Cancel
Save