← Back to branch summary

~verifytapn/verifytapn/1.0

« back to all changes in this revision

Viewing changes to src/Core/VerificationOptions.cpp

  • Committer: Lasse Jacobsen
  • Date: 2010-12-08 15:08:52 UTC
  • Revision ID: lassejac@lassejac-laptop-20101208150852-23199n367rkamcuh
- added switch for DFS or BFS search
- added bubble sort for symmetry reduction

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Core/VerificationOptions.cpp
23
23
                }
24
24
        }
25
25
 
 
26
        std::string SearchTypeEnumToString(SearchType s){
 
27
                switch(s){
 
28
                case DEPTHFIRST:
 
29
                        return "Depth-First Search";
 
30
                default:
 
31
                        return "Breadth-First Search";
 
32
                }
 
33
        }
 
34
 
 
35
        SearchType intToSearchTypeEnum(int i) {
 
36
                switch(i){
 
37
                case 1:
 
38
                        return DEPTHFIRST;
 
39
                default:
 
40
                        return BREADTHFIRST;
 
41
                }
 
42
        }
 
43
 
26
44
        VerificationOptions VerificationOptions::ParseVerificationOptions(int argc, char* argv[])
27
45
        {
28
46
                std::string workingdir = boost::filesystem::initial_path().string();
32
50
                desc.add_options()
33
51
                                ("help,h", "Produce help message")
34
52
                                ("k-bound,k", boost::program_options::value<int>(), "Specify the bound of the TAPN model")
 
53
                                ("search-type,o", boost::program_options::value<int>()->default_value(0), "Specify the desired search strategy. \n - 0: BFS\n - 1: DFS" )
35
54
                                ("trace,t", boost::program_options::value<int>()->default_value(0), "Specify the desired trace option. \n - 0: none\n - 1: Some")
36
55
                                ("global-max-constant,g", "Use a global max constant for extrapolation (as opposed to local constants)")
37
56
                                ("infinity-places,i", "Use the infinity place optimization")
53
72
                        exit(0);
54
73
                }
55
74
 
 
75
                SearchType search = intToSearchTypeEnum(vm["search-type"].as<int>());
 
76
                std::cout << "Using " << SearchTypeEnumToString(search) << "\n";
 
77
 
56
78
                if(vm.count("k-bound")) {
57
79
                        std::cout << "k-bound is: " << vm["k-bound"].as<int>() << "\n";
58
80
                }
64
86
                Trace trace = intToEnum(vm["trace"].as<int>());
65
87
                std::cout << "Generating " << enumToString(trace) << " trace \n";
66
88
 
 
89
 
 
90
 
67
91
                bool symmetry = true;
68
92
                if(vm.count("symmetry")) {
69
93
                        std::cout << "Symmetry Reduction is ON\n";
120
144
                        exit(0);
121
145
                }
122
146
 
123
 
                return VerificationOptions(vm["model-file"].as<std::string>(), vm["query-file"].as<std::string>(), vm["k-bound"].as<int>(), symmetry, trace, infPlaces, globalConstants, workingdir);
 
147
                return VerificationOptions(vm["model-file"].as<std::string>(), vm["query-file"].as<std::string>(), search, vm["k-bound"].as<int>(), symmetry, trace, infPlaces, globalConstants, workingdir);
124
148
        }
125
149
}