-
Notifications
You must be signed in to change notification settings - Fork 0
/
example.ini
131 lines (118 loc) · 5.45 KB
/
example.ini
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
; examples.ini
; Sample tlcwrapper.py configuration file
[options] ; TLC cmd arguments
; "target" specifies the top module TLA+ file
target: path/to/top_module.tla
; "model name" creates a directory "path/to/model_name" + "_timestamp" + "_seq", copies all tla files to it
model name: model_name
; default options are as follows (optional)
; "workers" worker numbers, default is 1. (use "auto" to automatically select the number of threads)
workers: 1
; SHOW_IN_TABLE to show in the summary table, must be used consecutively after the option
workers: SHOW_IN_TABLE
; "dfs depth" sets model checking search mode to dfs (default is bfs), and sets the search depth
dfs depth: 100
; "simulation depth" enables simulation mode and sets the search depth
simulation depth: 100
; "simulation traces" generates n*worker traces (default is infinite), also enables simulation mode
simulation traces: 0
; "simulation dump traces" saves traces, also enables simulation mode
simulation dump traces: false/true
; "simulation seed" sets seed for random simulation (can be used to reproduce an experiment), also enables simulation mode
simulation seed: 0
; "check deadlock" whether or not to check deadlock, default is false
check deadlock: false/true
; "checkpoint minute" interval between check point, default is 30
checkpoint minute: 30
; "recover" recover from the checkpoint with the specified id (i.e. path, recommended to use absolute path), default is not set
recover: /path/to/yyyy-MM-dd-HH-mm-ss.SSS
; "clean up" clean up the states directory (only when not recovering), default is false
clean up: true/false
; "gzip" controls if gzip is applied to value input/output (checkpoint) streams, default is false (true saves ~88% disk spaces)
gzip: false/true
; "dump states" saves states to "MC_states.dump" or "MC_states.dot". value range: "true", "dot", or "false" (default)
dump states: false/true/dot/dot,colorize,actionlabels,stuttering
; "coverage minute" sets tlc computing coverage every n minutes, default is disabled
coverage minute: 1
; "system memory" physical memory to use (MB)
system memory: 4000
; "memory ratio" physical memory ratio to use (0..1) (overrides "system memory")
memory ratio: 0.4
; "community modules" whether or not to use community modules, default is false
community modules: false/true
; "generate spec TE" generating a trace exploration (TE) spec, default is false
generate spec TE: false/true
; "dump trace" formats the TLA+ error trace as TLA and JSON, default is false
dump trace: false/true
; "stop after" TLC stops after n seconds
stop after: 600
; "liveness check" checks liveness properties at different times of model checking
liveness check: default/final/seqfinal
; "diff trace" when printing trace, show only the differences between successive states
diff trace: false/true
; "distributed mode" run an ad hoc TLC distributed server, the value should be hostname/ip (not true)
distributed mode: false/true/hostname/ip
; distributed worker types: "distributed TLC and fingerprint" is recommended
distributed TLC workers: user1@host1 [memory] [thread count]
user2@host2 [memory] [thread count]
distributed fingerprint server: user2@host2
distributed TLC and fingerprint: user3@host3
; "other TLC options" other TLC options, each argument is split by line, and starts with space
other TLC options: field
split by
line
; "other Java options" other Java options, each argument is split by line, and starts with space
other Java options: field
split by
line
[init state] ; (optional) replace Init with a specific state in the trace file
; trace file or MC.out (with counterexample traces) to provide a state
trace file: path/to/trace_file
; the number of state to be selected, 0 to select the last state
state: 0
; python callback handlers to select a specific state
python init file: path/to/python_file
[behavior] ; what is the behavior spec
; one or none: (init & next) OR (temporal formula)
#init: Init
#next: Next
temporal formula: Spec
[invariants] ; (for safety) formulas true in every reachable state
; format: "NAME: formula"
TypeOK: TypeOK
TCConsistent: TCConsistent
; Warning: multi line removes any leading spaces
multi_line_inv: /\ multi
/\ line
/\ inv
[properties] ; (for liveness) temporal formulas true for every possible behavior
; format is the same as [invariants]
TCSpec: TCSpec
[state constraint] ; A state constraint is a formula restrict the possible states by a state predicate
; format is the same as [invariants]
StateConstraint: StateConstraint
[action constraint] ; An action constraint is a formula restrict the possible transactions
; format is the same as [invariants]
ActionConstraint: ActionConstraint
[additional definitions]; definitions required for the model checkings
Additional: abc == 1
[constants] ; specify the values of declared constants
; continuous same options will be combined by Cartesian product (to support batch mode)
Char: [model value]<symmetrical>{a, b}
Char: [model value]<symmetrical>{a, b, c}
Client: [model value]{c1, c2}
Client: [model value]{c1, c2, c3}
Server: [model value]
InitState: <<>>
InitState: SHOW_IN_TABLE
Msg: Msg
[override] ; direct TLC to use alternate definitions for operators
; the same as [constants] (but without "set of model values")
Nop: [model value]
Int: -10..10
Int: -1000..1000
[const expr] ; evaluate constant expression
; only one option "expr", you cannot define other names
expr: GCD(1,1)
[alias]
alias: Alias