/
IConfigurationConstants.java
147 lines (139 loc) · 4.56 KB
/
IConfigurationConstants.java
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
package org.lamport.tla.toolbox.tool.tlc.launch;
import tlc2.tool.fp.FPSet;
/**
* Constants for the configuration
* @author Simon Zambrovski
* @version $Id$
*/
public interface IConfigurationConstants
{
/**
* path to the root file of the spec (/bar/foo.tla)
*/
public static final String SPEC_ROOT_FILE = "specRootFile";
/**
* name of the spec (foo_spec)
*/
public static final String SPEC_NAME = "specName";
/**
* Name of the configuration (foo_mc_{i})
*/
public static final String MODEL_NAME = "configurationName";
/**
* Which profile to use for TLC configuration
*/
public static final String TLC_RESOURCES_PROFILE = "tlcResourcesProfile";
/**
* Number of workers to use during TLC launch
*/
public static final String LAUNCH_NUMBER_OF_WORKERS = "numberOfWorkers";
/**
* Launch distributed version of TLC
*/
public static final String LAUNCH_DISTRIBUTED = "distributedTLC";
/**
* Launch distributed version of TLC and send result to this address
*/
public static final String LAUNCH_DISTRIBUTED_RESULT_MAIL_ADDRESS = "result.mail.address";
/**
* Additional VM args for distributed version of TLC
*/
public static final String LAUNCH_JVM_ARGS = "distributedTLCVMArgs";
/**
* Additional VM args for distributed version of TLC
*/
public static final String LAUNCH_TLC_PARAMETERS = "TLCCmdLineParameters";
/**
* Distributed FPSets
*/
public static final String LAUNCH_DISTRIBUTED_FPSET_COUNT = "distributedFPSetCount";
/**
* Distributed Nodes count
*/
public static final String LAUNCH_DISTRIBUTED_NODES_COUNT = "distributedNodesCount";
/**
* Network interface under which TLC server process will listen (java.rmi.server.hostname)
*/
public static final String LAUNCH_DISTRIBUTED_INTERFACE = "distributedNetworkInterface";
/**
* Pre-flight script (primarily for distributed version of TLC)
*/
public static final String LAUNCH_DISTRIBUTED_SCRIPT = "distributedTLCScript";
/**
* How to run TLC (model-checking = true, simulation = false)
*/
public static final String LAUNCH_MC_MODE = "mcMode";
/**
* the VIEW to map from variables to values
*/
public static final String LAUNCH_VIEW = "view";
/**
* the POSTCONDITION to map from variables to values
*/
public static final String LAUNCH_POST_CONDITION = "postCondition";
/**
* MC depth first
*/
public static final String LAUNCH_DFID_MODE = "dfidMode";
/**
* the depth of DFID run
*/
public static final String LAUNCH_DFID_DEPTH = "dfidDepth";
/**
* the number of traces to generate by simulation.
*/
public static final String LAUNCH_SIMU_NUM_TRACES = "simuNumTraces";
/**
* the depth of simulation run
*/
public static final String LAUNCH_SIMU_DEPTH = "simuDepth";
/**
* the aril of simulation run
*/
public static final String LAUNCH_SIMU_ARIL = "simuAril";
/**
* the seed of simulation run
*/
public static final String LAUNCH_SIMU_SEED = "simuSeed";
/**
* the fp seed index "-fp"
*/
public static final String LAUNCH_FP_INDEX = "fpIndex";
/**
* Choose FP index randomly
*/
public static final String LAUNCH_FP_INDEX_RANDOM = "fpIndexRandom";
/**
* Defers verification of liveness properties upon the final stage of model
* checking (upon termination).
*/
public static final String LAUNCH_DEFER_LIVENESS = "deferLiveness";
/**
* Visualize state graph after model checking with GraphViz.
*/
public static final String LAUNCH_VISUALIZE_STATEGRAPH = "visualizeStateGraph";
/**
* Collect coverage statistics
*/
public static final String LAUNCH_COVERAGE = "collectCoverage";
/**
* Run from the checkpoint
*/
public static final String LAUNCH_RECOVER = "recover";
/**
* JVM maximum heap size
*/
public static final String LAUNCH_MAX_HEAP_SIZE = "maxHeapSize";
/**
* Amount of fp bits used for disk storage addressing
*/
public static final String LAUNCH_FPBITS = "fpBits";
/**
* The maximum size (upper bound) for a TLA set
*/
public static final String LAUNCH_MAXSETSIZE = "maxSetSize";
/**
* {@link FPSet} implementation to use during model checking
*/
public static final String LAUNCH_FPSET_IMPL = "fpSetImpl";
}