← Back to branch summary

~verifydtapn-contributers/verifydtapn/d3.4

« back to all changes in this revision

Viewing changes to src/DiscreteVerification/DiscreteVerification.hpp

  • Committer: Jiri Srba
  • Date: 2020-09-09 17:52:56 UTC
  • mfrom: (338.1.41 cmake)
  • Revision ID: srba@cs.aau.dk-20200909175256-6y90y7whhki3t4u2
merged in lp:~verifydtapn-contributers/verifydtapn/cmake that uses cmake, adds AF games, code cleanup 

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/DiscreteVerification/DiscreteVerification.hpp
1
 
/*
2
 
 * DiscreteVerification.hpp
3
 
 *
4
 
 *  Created on: 23 Feb 2012
5
 
 *      Author: jakob
6
 
 */
7
 
 
8
 
#ifndef DISCRETEVERIFICATION_HPP_
9
 
#define DISCRETEVERIFICATION_HPP_
10
 
 
11
 
#include <iostream>
12
 
#include "../Core/TAPN/TAPN.hpp"
13
 
#include "../Core/QueryParser/AST.hpp"
14
 
#include "../Core/VerificationOptions.hpp"
15
 
#include "DataStructures/NonStrictMarking.hpp"
16
 
#include "../../lib/rapidxml-1.13/rapidxml.hpp"
17
 
#include "../../lib/rapidxml-1.13/rapidxml_print.hpp"
18
 
#include "SearchStrategies/SearchStrategy.hpp"
19
 
#include "../Core/TAPNParser/util.hpp"
20
 
#include <stack>
21
 
#include "VerificationTypes/Verification.hpp"
22
 
#include "VerificationTypes/LivenessSearch.hpp"
23
 
#include "VerificationTypes/ReachabilitySearch.hpp"
24
 
#include "VerificationTypes/TimeDartReachabilitySearch.hpp"
25
 
#include "VerificationTypes/TimeDartLiveness.hpp"
26
 
#include "VerificationTypes/WorkflowSoundness.hpp"
27
 
#include "VerificationTypes/WorkflowStrongSoundness.hpp"
28
 
#include "SearchStrategies/SearchFactory.h"
29
 
 
30
 
 
31
 
namespace VerifyTAPN {
32
 
 
33
 
namespace DiscreteVerification {
34
 
 
35
 
class DiscreteVerification {
36
 
public:
37
 
        DiscreteVerification();
38
 
        virtual ~DiscreteVerification();
39
 
        static int run(TAPN::TimedArcPetriNet& tapn, std::vector<int> initialPlacement, AST::Query* query, VerificationOptions& options);
40
 
private:
41
 
        static void printHumanTrace(bool result, NonStrictMarking* m, std::stack<NonStrictMarking*>& stack, AST::Quantifier query);
42
 
        static void printXMLTrace(bool result, NonStrictMarking* m, std::stack<NonStrictMarking*>& stack, AST::Quantifier query);
43
 
        static rapidxml::xml_node<>* createTransitionNode(NonStrictMarking* old, NonStrictMarking* current, rapidxml::xml_document<>& doc);
44
 
        static rapidxml::xml_node<>* createTokenNode(rapidxml::xml_document<>& doc, const TAPN::TimedPlace& place, const Token& token);
45
 
        static void createTransitionSubNodes(NonStrictMarking* old, NonStrictMarking* current, rapidxml::xml_document<>& doc, rapidxml::xml_node<>* transitionNode, const TAPN::TimedPlace& place, const TAPN::TimeInterval& interval, const int weight);
46
 
        static void generateTraceStack(NonStrictMarking* m, std::stack<NonStrictMarking*>* stack, std::stack<NonStrictMarking*>* liveness = NULL);
47
 
};
48
 
 
49
 
}
50
 
 
51
 
}
52
 
 
53
 
#endif /* DISCRETEVERIFICATION_HPP_ */