-
Notifications
You must be signed in to change notification settings - Fork 1
/
enumerate.go
260 lines (206 loc) · 6.9 KB
/
enumerate.go
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
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
// Here we define the TM enumeration algorithm
package bbchallenge
import (
"fmt"
"io"
"runtime"
"sync"
"time"
)
type SimulationBackend byte
const (
SIMULATION_GO SimulationBackend = iota
SIMULATION_C
)
// Package parameters
var TimeStart time.Time = time.Now()
var UndecidedTimeLog io.Writer // Logging UNDECIDED_TIME machines
var UndecidedSpaceLog io.Writer // Logging UNDECIDED_SPACE machines
var BBRecordLog io.Writer // Logging BB and BB_space record holders
var Verbose bool
var LogFreq int64 = 30000000000 // 30 sec in ns
var ActivateFiltering bool = true
var SimulationLimitTime int = BB5
var SimulationLimitSpace int = BB5_SPACE
var SlowDownInit int = 2 // How many recursion will be done on the stack before calling go routines
// At the root of the TM tree are always 12 machines (independently of nbStates)
// Only 8 of them are interesting. We authorize the user to cut the computation
// of the entire tree in 1, 2, 4, or 8 pieces. Useful when you have several computers!
var TaskDivisor int = 1 // Can be either 1, 2, 4 or 8
var TaskDivisorMe int = 0 // Wich task to I do
// Package outputs
var mutexMetrics sync.Mutex
var NbMachineSeen int
var NbMachinePruned int
var NbHaltingMachines int
var NbNonHaltingMachines int
var NbUndecidedTime int
var NbUndecidedSpace int
var MaxNbSteps int
var MaxSpace int
var MaxNbGoRoutines int
// Logging related internal variables
var lastLogTime time.Time
var notFirstLog bool
// Invariant: tm's transition (state, read) is not defined
func Enumerate(nbStates byte, tm TM, state byte, read byte,
previous_steps_count int, previous_space_count int,
slow_down int, simulation_backend SimulationBackend) {
// mutexMetrics.Lock()
// printTM(tm)
// mutexMetrics.Unlock()
// Get the list of candidate target states
// taking all states up to the first completely undefined
// As in http://turbotm.de/~heiner/BB/mabu90.html#Enumeration
var target_states [MAX_STATES]byte
var definedTransitionCount byte
var undefinedTransitionCount byte
for iState := 0; iState < int(nbStates); iState += 1 {
target_states[iState] = byte(iState + 1)
if tm[6*(iState)+3*0+2] == 0 {
undefinedTransitionCount += 1
} else {
definedTransitionCount += 1
}
if tm[6*(iState)+3*1+2] == 0 {
undefinedTransitionCount += 1
} else {
definedTransitionCount += 1
}
// The following allows to take the min of the completely undefined states
// last condition very important to discard current state (which is about to not be completely undefined)
if tm[6*(iState)+3*0+2] == 0 && tm[6*(iState)+3*1+2] == 0 && byte(iState+1) != state {
break
}
}
// Last transition
if target_states[nbStates-1] != 0 && undefinedTransitionCount == 1 {
return
}
isRoot := definedTransitionCount == 1
var target_state byte
var localNbMachineSeen int
var localNbMachinePruned int
var localNbHalt int
var localNbNoHalt int
var localNbUndecidedTime int
var localNbUndecidedSpace int
var localMaxNbSteps int
var localBestTimeHaltingMachine TM
var localBestSpaceHaltingMachine TM
var localMaxSpace int
var loopIndex int
var wg sync.WaitGroup
for _, target_state = range target_states {
if target_state == 0 {
break
}
var move byte
for move = 0; move <= 1; move += 1 {
var write byte
for write = 0; write <= 1; write += 1 {
var newTm TM = tm
newTm[(state-1)*6+read*3] = write
newTm[(state-1)*6+read*3+1] = move
newTm[(state-1)*6+read*3+2] = target_state
if !isRoot && ActivateFiltering && pruneTM(nbStates, newTm, state, read) {
localNbMachinePruned += 1
continue
}
localNbMachineSeen += 1
var haltStatus HaltStatus
var after_state byte
var after_read byte
var steps_count int
var space_count int
switch simulation_backend {
case SIMULATION_GO:
haltStatus, after_state, after_read, steps_count, space_count = simulate(newTm, SimulationLimitTime, SimulationLimitSpace)
break
case SIMULATION_C:
haltStatus, after_state, after_read, steps_count, space_count = simulate_C_wrapper(newTm, SimulationLimitTime, SimulationLimitSpace)
break
}
switch haltStatus {
case HALT:
// Task Divisor
if isRoot {
if loopIndex/(8/TaskDivisor) != TaskDivisorMe {
loopIndex += 1
continue
} else {
loopIndex += 1
}
}
if steps_count > localMaxNbSteps {
localBestTimeHaltingMachine = newTm
}
if space_count > localMaxSpace {
localBestSpaceHaltingMachine = newTm
}
localMaxNbSteps = MaxI(localMaxNbSteps, steps_count)
localMaxSpace = MaxI(localMaxSpace, space_count)
localNbHalt += 1
if slow_down == 0 {
wg.Add(1)
go func() {
Enumerate(nbStates, newTm, after_state, after_read, steps_count, space_count,
SlowDownInit, simulation_backend)
wg.Done()
}()
} else {
Enumerate(nbStates, newTm, after_state, after_read, steps_count, space_count,
slow_down-1, simulation_backend)
}
break
case NO_HALT:
localNbNoHalt += 1
break
case UNDECIDED_TIME:
localNbUndecidedTime += 1
UndecidedTimeLog.Write(newTm[:])
break
case UNDECIDED_SPACE:
localNbUndecidedSpace += 1
UndecidedSpaceLog.Write(newTm[:])
break
}
}
}
}
wg.Wait()
mutexMetrics.Lock()
NbMachineSeen += localNbMachineSeen
NbMachinePruned += localNbMachinePruned
NbHaltingMachines += localNbHalt
NbNonHaltingMachines += localNbNoHalt
NbUndecidedTime += localNbUndecidedTime
NbUndecidedSpace += localNbUndecidedSpace
if localMaxNbSteps >= MaxNbSteps {
BBRecordLog.Write([]byte(fmt.Sprintf("*TIME %d SPACE %d\n%s\n",
localMaxNbSteps, localMaxSpace,
localBestTimeHaltingMachine.ToAsciiTable(nbStates))))
} else if localMaxSpace >= MaxSpace {
BBRecordLog.Write([]byte(fmt.Sprintf("TIME %d *SPACE %d\n%s\n",
localMaxNbSteps, localMaxSpace,
localBestSpaceHaltingMachine.ToAsciiTable(nbStates))))
}
MaxNbSteps = MaxI(localMaxNbSteps, MaxNbSteps)
MaxSpace = MaxI(localMaxSpace, MaxSpace)
MaxNbGoRoutines = MaxI(MaxNbGoRoutines, runtime.NumGoroutine())
if Verbose && (!notFirstLog || time.Since(lastLogTime) >= time.Duration(LogFreq)) {
notFirstLog = true
lastLogTime = time.Now()
fmt.Printf("run time: %s\ntotal: %d\npruned: %d (%.2f)\nhalt: %d (%.2f)\nnon halt: %d (%.2f)\nundecided time: %d (%.2f)\n"+
"undecided space: %d (%.2f)\nbb est.: %d\nbb space est.: %d\nrun/sec: %f\nmax go routines: %d\n\n",
time.Since(TimeStart), NbMachineSeen,
NbMachinePruned, float64(NbMachinePruned)/float64(NbMachineSeen),
NbHaltingMachines, float64(NbHaltingMachines)/float64(NbMachineSeen),
NbNonHaltingMachines, float64(NbNonHaltingMachines)/float64(NbMachineSeen),
NbUndecidedTime, float64(NbUndecidedTime)/float64(NbMachineSeen),
NbUndecidedSpace, float64(NbUndecidedSpace)/float64(NbMachineSeen),
MaxNbSteps, MaxSpace, float64(NbMachineSeen)/time.Since(TimeStart).Seconds(),
MaxNbGoRoutines)
}
mutexMetrics.Unlock()
}