~verifydtapn-contributers/verifydtapn/trunk

« back to all changes in this revision

Viewing changes to src/DiscreteVerification/DiscreteVerification.cpp

  • Committer: Jiri Srba
  • Date: 2015-08-31 12:39:10 UTC
  • mfrom: (324.3.24 PTrieWorkflow)
  • Revision ID: srba@cs.aau.dk-20150831123910-qwr9g6pq7zntajhe
merged in a big branch implementing PTrie for workflow analysis

Show diffs side-by-side

added added

removed removed

Lines of Context:
53
53
                                        exit(1);
54
54
                                }
55
55
 
56
 
                if (options.getMemoryOptimization() != VerificationOptions::NO_MEMORY_OPTIMIZATION) {
57
 
                                        cout << "Workflow analysis currently does not support any memory optimizations (i.e. no PTries)." << endl;
58
 
                                        exit(1);
59
 
                                }
60
 
                WaitingList<NonStrictMarking*>* strategy = getWaitingList<NonStrictMarking* > (query, options);
61
56
                if(options.getWorkflowMode() == VerificationOptions::WORKFLOW_SOUNDNESS){
62
 
                        WorkflowSoundness* verifier = new WorkflowSoundness(tapn, *initialMarking, query, options, strategy);
 
57
                        WorkflowSoundness* verifier;
 
58
                        if(options.getMemoryOptimization() == VerificationOptions::NO_MEMORY_OPTIMIZATION)
 
59
                        {
 
60
                            verifier = new WorkflowSoundness(tapn, *initialMarking, query, options, 
 
61
                                    getWaitingList<NonStrictMarking* > (query, options));
 
62
                        }
 
63
                        else
 
64
                        {
 
65
                            verifier = new WorkflowSoundnessPTrie(tapn, *initialMarking, query, options, 
 
66
                                    getWaitingList<ptriepointer_t<MetaData*> > (query, options));
 
67
                        }
63
68
 
64
 
                                        if(verifier->getModelType() == verifier->NOTTAWFN){
65
 
                                                std::cerr << "Model is not a TAWFN!" << std::endl;
66
 
                                                return -1;
67
 
                                        }else if(verifier->getModelType() == verifier->ETAWFN){
68
 
                                                std::cout << "Model is a ETAWFN" << std::endl << std::endl;
69
 
                                        }else if(verifier->getModelType() == verifier->MTAWFN){
70
 
                                                std::cout << "Model is a MTAWFN" << std::endl << std::endl;
71
 
                                        }
72
 
                                        VerifyAndPrint(
73
 
                                                        tapn,
74
 
                                                        *verifier,
75
 
                                                        options,
76
 
                                                        query);
77
 
                                        verifier->printExecutionTime(cout);
78
 
                                        verifier->printMessages(cout);
 
69
                            if(verifier->getModelType() == verifier->NOTTAWFN){
 
70
                                    std::cerr << "Model is not a TAWFN!" << std::endl;
 
71
                                    return -1;
 
72
                            }else if(verifier->getModelType() == verifier->ETAWFN){
 
73
                                    std::cout << "Model is a ETAWFN" << std::endl << std::endl;
 
74
                            }else if(verifier->getModelType() == verifier->MTAWFN){
 
75
                                    std::cout << "Model is a MTAWFN" << std::endl << std::endl;
 
76
                            }
 
77
                            VerifyAndPrint(
 
78
                                            tapn,
 
79
                                            *verifier,
 
80
                                            options,
 
81
                                            query);
 
82
                            verifier->printExecutionTime(cout);
 
83
                            verifier->printMessages(cout);
 
84
#ifdef CLEANUP
 
85
                            delete verifier;
 
86
#endif
79
87
                }
80
88
                else{
81
89
                        // Assumes correct structure of net!
82
 
                        WorkflowStrongSoundnessReachability* verifier = new WorkflowStrongSoundnessReachability(tapn, *initialMarking, query, options, strategy);
 
90
                        WorkflowStrongSoundnessReachability* verifier;
 
91
                        if(options.getMemoryOptimization() == VerificationOptions::NO_MEMORY_OPTIMIZATION)
 
92
                        {
 
93
                            verifier = new  WorkflowStrongSoundnessReachability(tapn, *initialMarking, query, options, 
 
94
                                    getWaitingList<NonStrictMarking* > (query, options));
 
95
                        }
 
96
                        else
 
97
                        {
 
98
                            verifier = new  WorkflowStrongSoundnessPTrie(tapn, *initialMarking, query, options, 
 
99
                                    getWaitingList<ptriepointer_t<MetaData*> > (query, options));
 
100
                        }
83
101
                        VerifyAndPrint(
84
102
                                                        tapn,
85
103
                                                        *verifier,
86
104
                                                        options,
87
105
                                                        query);
88
106
                                        verifier->printExecutionTime(cout);
 
107
#ifdef CLEANUP
 
108
                        delete verifier;
 
109
#endif
89
110
                }
90
111
 
91
 
                delete strategy;
 
112
                
92
113
                return 0;
93
114
            }
94
115