main.go 13.3 KB
Newer Older
Etienne Renault's avatar
Etienne Renault committed
1
2
3
4
5
// Copyright (C) 2020 Laboratoire de Recherche et Developpement
// de l'EPITA (LRDE).
//
// This file is part of Go2Pins, a tool for Golang model-checking
//
Etienne Renault's avatar
Etienne Renault committed
6
// Go2Pins is free software; you can redistribute it and/or modify it
Etienne Renault's avatar
Etienne Renault committed
7
8
9
10
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
Etienne Renault's avatar
Etienne Renault committed
11
// Go2Pins is distributed in the hope that it will be useful, but WITHOUT
Etienne Renault's avatar
Etienne Renault committed
12
13
14
15
16
17
18
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

19
20
21
22
package {{.PackageName}}

/*
#include "go2pins.h"
23
24
#cgo CFLAGS: -I .
#cgo LDFLAGS: -L . -lgo2pins
25
26
27
*/
import "C"
import (
Hugo Moreau's avatar
Hugo Moreau committed
28
	"{{.Output}}/structs"
29
30
	"flag"
	"fmt"
Etienne Renault's avatar
Etienne Renault committed
31
	"log"
32
	"os"
Etienne Renault's avatar
Etienne Renault committed
33
	"os/exec"
Etienne Renault's avatar
Etienne Renault committed
34
	"path/filepath"
35
	"regexp"
36
	"strconv"
37
	"strings"
38
39
40
	"unsafe"
)

Hugo Moreau's avatar
Hugo Moreau committed
41
42
func G2PEntry(src structs.G2PStateType) []structs.G2PStateType {
	res := make([]structs.G2PStateType, 0)
43
44
	for _, g := range G2PGoroutines {
		if src[g.Status] != 0 { // is goroutine active ?
45
			res = append(res, g.Func(src))
46
47
48
		}
	}

Hugo Moreau's avatar
Hugo Moreau committed
49
50
	result := append(res, G2PMain(src))

Hugo Moreau's avatar
Hugo Moreau committed
51
	var final []structs.G2PStateType = []structs.G2PStateType{}
Etienne Renault's avatar
Etienne Renault committed
52
53
54
55
56
	WAIT_READ := -1
	WAIT_WRITE := 1
	for _, succ := range result {

		all_are_clear := true
Hugo Moreau's avatar
Hugo Moreau committed
57
		var toadd []structs.G2PStateType = []structs.G2PStateType{}
Etienne Renault's avatar
Etienne Renault committed
58

Hugo Moreau's avatar
Hugo Moreau committed
59
		for _, channel := range G2PChannels {
Etienne Renault's avatar
Etienne Renault committed
60
61
62
63
64
65
66
67
68
69
70
71
			for pid, idx := 0, channel.State; idx < channel.State+channel.Length; pid, idx = pid+1, idx+2 {
				// There is sync in progress
				if succ[idx] == WAIT_WRITE || succ[idx] == WAIT_READ {
					all_are_clear = false

					// Look for a sync. friend
					if succ[idx] == WAIT_WRITE {

						allclear1 := true
						for jdx := channel.State; jdx < channel.State+channel.Length; jdx += 2 {
							if succ[jdx] == WAIT_READ {
								// build the combination of the 2
Hugo Moreau's avatar
Hugo Moreau committed
72
								var new_succ structs.G2PStateType = succ
Etienne Renault's avatar
Etienne Renault committed
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94

								// Reset WAIT_READ / WAIT_WRITE operations
								new_succ[idx] = 0
								new_succ[jdx] = 0
								// Set the new successor
								new_succ[new_succ[jdx+1]] = new_succ[idx+1]
								// Reset Values
								new_succ[idx+1] = 0
								new_succ[jdx+1] = 0
								toadd = append(toadd, new_succ)
							}
						}

						// Other process can progress or this is the first step of sync.
						if allclear1 {
							if pid == 0 && ((src[1] == succ[1]) || (src[idx] != succ[idx])) {
								toadd = append(toadd, succ)

							} else if (src[G2PGoroutines[pid-1].LineCounter] == succ[G2PGoroutines[pid-1].LineCounter]) || src[idx] != succ[idx] {
								toadd = append(toadd, succ)
							}
						}
Hugo Moreau's avatar
Hugo Moreau committed
95
96
97
					}
				}
			}
Etienne Renault's avatar
Etienne Renault committed
98
99
100
101
102
103
104
105
		}

		// add successor and process the next successor
		if all_are_clear {
			final = append(final, succ)
		} else if len(toadd) != 0 {
			for _, e := range toadd {
				final = append(final, e)
Hugo Moreau's avatar
Hugo Moreau committed
106
107
108
109
			}
		}
	}

Etienne Renault's avatar
Etienne Renault committed
110
	// Build the result by considering eventually RERS inputs
Hugo Moreau's avatar
Hugo Moreau committed
111
	var final2 []structs.G2PStateType = []structs.G2PStateType{}
112
	for i, _ := range final {
Hugo Moreau's avatar
Hugo Moreau committed
113
114
115
		if structs.G2PRersActive != 0 && src[structs.G2PRersPos] != result[i][structs.G2PRersPos] {
			for _, e := range structs.G2PRersValues {
				result[i][structs.G2PRersPos] = e
116
				final2 = append(final2, result[i])
Etienne Renault's avatar
Etienne Renault committed
117
118
			}
		} else {
119
			final2 = append(final2, final[i])
Etienne Renault's avatar
Etienne Renault committed
120
121
122
		}
	}
	return final2
123
124
}

125
126
//export get_state_variable_count
func get_state_variable_count() C.int {
Hugo Moreau's avatar
Hugo Moreau committed
127
	return C.int(structs.G2PStateSize)
128
129
}

130
131
132
133
// See https://github.com/golang/go/wiki/cgo#turning-c-arrays-into-go-slices
// for trick used in this function and the next one:
// The pointer is casted to a go array of size (2^30) then sliced to
// the size expected
Hugo Moreau's avatar
Hugo Moreau committed
134
135
136
func g2pCopyToC(arr *structs.G2PStateType, arrC *C.int) {
	arrC2 := (*[1 << 30]C.int)(unsafe.Pointer(arrC))[:structs.G2PStateSize:structs.G2PStateSize]
	for i := 0; i < structs.G2PStateSize; i++ {
137
138
139
140
		arrC2[i] = C.int(arr[i])
	}
}

Hugo Moreau's avatar
Hugo Moreau committed
141
142
143
func g2pCopyFromC(arrC *C.int, arr *structs.G2PStateType) {
	arrC2 := (*[1 << 30]C.int)(unsafe.Pointer(arrC))[:structs.G2PStateSize:structs.G2PStateSize]
	for i := 0; i < structs.G2PStateSize; i++ {
144
145
146
147
148
149
150
151
152
153
154
		arr[i] = int(arrC2[i])
	}
}

//export get_successors
func get_successors(
	model unsafe.Pointer,
	srcC *C.int,
	cb C.TransitionCB,
	arg unsafe.Pointer,
) C.int {
Hugo Moreau's avatar
Hugo Moreau committed
155
	src := structs.G2PStateType{}
156
	g2pCopyFromC(srcC, &src)
157
	dsts := G2PEntry(src)
Hugo Moreau's avatar
Hugo Moreau committed
158
	var dstC = (*C.int)(C.malloc(C.size_t(structs.G2PStateSize) * C.sizeof_int))
159
160
161
162
163
164
165
166
167
	for _, dst := range dsts {
		g2pCopyToC(&dst, dstC)
		C.callTransitionCb(cb, arg, nil, dstC)
	}
	return C.int(len(dsts))
}

//export get_initial_state
func get_initial_state(srcC *C.int) {
Hugo Moreau's avatar
Hugo Moreau committed
168
	src := structs.G2PStateType{0, 0}
169
170
171
172
173
174
175
176
	g2pCopyToC(&src, srcC)
}

var unknownVarName = C.CString("UNKNOWN_VAR")

//export get_state_variable_name
func get_state_variable_name(vC C.int) *C.char {
	v := int(vC)
Hugo Moreau's avatar
Hugo Moreau committed
177
178
	if v < len(structs.G2PVariableNames) {
		return (*C.char)(structs.G2PVariableNames[v])
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
	}
	return unknownVarName
}

//export get_state_variable_type
func get_state_variable_type(vC C.int) C.int {
	return C.int(0)
}

//export get_state_variable_type_count
func get_state_variable_type_count() C.int {
	return C.int(1)
}

var typeNames = []*C.char{
	C.CString("int"),
}
var unknownTypeName = C.CString("UNKNOWN_TYPE")

//export get_state_variable_type_name
func get_state_variable_type_name(vC C.int) *C.char {
	v := int(vC)
	if v < len(typeNames) {
		return typeNames[v]
	}
	return unknownTypeName
}

var typeValueCount = [1]C.int{
	// FIXME: Figure out what this means. When setting it to the count of all
	// possible integers, get_state_variable_type_value gets called that many
	// times and the program freezes.
	0,
}

//export get_state_variable_type_value_count
func get_state_variable_type_value_count(vC C.int) C.int {
	v := int(vC)
	if v < len(typeValueCount) {
		return typeValueCount[v]
	}
	return C.int(0)
}

var unknownTypeValueName = C.CString("UNKNOWN_VALUE")

//export get_state_variable_type_value
func get_state_variable_type_value(tC C.int, vC C.int) *C.char {
	return unknownTypeValueName
}

Etienne Renault's avatar
Etienne Renault committed
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
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
// ------------------------------------------------------------
// The following is required by LTSmin, but not used since POR
// reductions are not yet available for Go2Pins.

//export get_transition_count
func get_transition_count() C.int {
	fmt.Printf("[Go2Pins] get_transition_count: unimplemented ... SKIP\n")
	return C.int(0)
}

//export have_property
func have_property() C.int {
	fmt.Printf("[Go2Pins] have_property: unimplemented ... SKIP\n")
	return C.int(0)
}

//export get_transition_read_dependencies
func get_transition_read_dependencies(t C.int) *C.int {
	fmt.Printf("[Go2Pins] get_transition_read_dependencies: unimplemented ... SKIP\n")
	return nil
}

//export get_transition_actions_read_dependencies
func get_transition_actions_read_dependencies(t C.int) *C.int {
	fmt.Printf("[Go2Pins] get_transition_actions_read_dependencies: unimplemented ... SKIP\n")
	return nil
}

//export get_transition_may_write_dependencies
func get_transition_may_write_dependencies(t C.int) *C.int {
	fmt.Printf("[Go2Pins] get_transition_may_write_dependencies: unimplemented ... SKIP\n")
	return nil
}

//export get_transition_must_write_dependencies
func get_transition_must_write_dependencies(t C.int) *C.int {
	fmt.Printf("[Go2Pins] get_transition_must_write_dependencies: unimplemented ... SKIP\n")
	return nil
}

//export get_guard_matrix
func get_guard_matrix(t C.int) *C.int {
	fmt.Printf("[Go2Pins] get_guard_matrix: unimplemented ... SKIP\n")
	return nil
}

//export get_guards
func get_guards(t C.int) *C.int {
	fmt.Printf("[Go2Pins] get_guards: unimplemented ... SKIP\n")
	return nil
}

//export get_all_guards
func get_all_guards(t C.int) **C.int {
	fmt.Printf("[Go2Pins] get_all_guards: unimplemented ... SKIP\n")
	return nil
}

//export get_guard_count
func get_guard_count() C.int {
	fmt.Printf("[Go2Pins] get_guard_count: unimplemented ... SKIP\n")
	return C.int(0)
}

//export get_successor
func get_successor(
	model unsafe.Pointer,
	srcC *C.int,
	cb C.TransitionCB,
	arg unsafe.Pointer,
) C.int {
	fmt.Printf("[Go2Pins] get_successor: unimplemented ... SKIP\n")
	return C.int(0)
}

//export get_action
func get_action(
	model unsafe.Pointer,
	srcC *C.int,
	cb C.TransitionCB,
	arg unsafe.Pointer,
) C.int {
	fmt.Printf("[Go2Pins] get_action: unimplemented ... SKIP\n")
	return C.int(0)
}

//export get_guard
func get_guard(
	model unsafe.Pointer,
	t int,
	src unsafe.Pointer,
) **C.int {
	fmt.Printf("[Go2Pins] get_guard: unimplemented ... SKIP\n")
	return nil
}

//export get_guard_all
func get_guard_all(
	model unsafe.Pointer,
	src unsafe.Pointer,
	guard *C.int,
) **C.int {
	fmt.Printf("[Go2Pins] get_guard_all: unimplemented ... SKIP\n")
	return nil
}

//export get_guard_may_be_coenabled_matrix
337
func get_guard_may_be_coenabled_matrix(g C.int) *C.int {
Etienne Renault's avatar
Etienne Renault committed
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
	fmt.Printf("[Go2Pins] get_guard_may_be_coenabled_matrix: unimplemented ... SKIP\n")
	return nil
}

//export get_guard_nes_matrix
func get_guard_nes_matrix(g C.int) *C.int {
	fmt.Printf("[Go2Pins] get_guard_nes_matrix: unimplemented ... SKIP\n")
	return nil
}

//export get_guard_nds_matrix
func get_guard_nds_matrix(g C.int) *C.int {
	fmt.Printf("[Go2Pins] get_guard_nds_matrix: unimplemented ... SKIP\n")
	return nil
}

// ------------------------------------------------------------

356
var (
357
358
359
360
361
362
	help      = flag.Bool("help", false, "Show usages.")
	backend   = flag.String("backend", "spot", "[spot|ltsmin] The model-checking backend to use")
	display   = flag.Bool("display", false, "Display the state-space in DOT (only spot backend)")
	kripke_ss = flag.Bool("kripke-size", false, "The size of the state space (only spot backend)")
	list_var  = flag.Bool("list-variables", false, "Display the list of variable names.")
	ltl       = flag.String("ltl", "", "The LTL formulae to check")
363
	nb_threads = flag.Int("nb-threads", 1, "The number of threads to use")
364
365
366
367
368
369
370
371
372
)

func init() {
	flag.Usage = func() {
		fmt.Fprintln(os.Stderr, "Usage: "+os.Args[0]+" [options]\n")
		flag.PrintDefaults()
	}
}

Etienne Renault's avatar
Etienne Renault committed
373
374
375
376
377
378
379
380
381
382
func spot_path() string {
	path, err := exec.LookPath("modelcheck")
	if err != nil {
		panic("\n\tSpot backend not aivalable! Update your PATH to have modelcheck in it.\n\texport PATH=<path_to_spot>/tests/ltsmin/:$PATH")
	}

	fmt.Println("Using : ", path)
	return path
}

383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
type DevNull struct{}

func (DevNull) Write(p []byte) (int, error) {
	return len(p), nil
}

func spot_dev_version() bool {
	path, _ := exec.LookPath("modelcheck")
	mcCmd := exec.Command(path, "--version")
	mcCmd.Stdout = new(DevNull)
	mcCmd.Stderr = new(DevNull)
	err := mcCmd.Run()
	if err != nil {
		return false
	}
	return true
}

Etienne Renault's avatar
Etienne Renault committed
401
402
403
404
405
406
407
408
409
410
func ltsmin_path() string {
	path, err := exec.LookPath("dve2lts-mc")
	if err != nil {
		panic("\n\tLTSmin backend not aivalable! Update your PATH to have dve2lts-mc in it.\n\texport PATH=<path_to_ltsmin>/bin/:$PATH")
	}

	fmt.Println("Using : ", path)
	return path
}

411
func main() {
412
	flag.Parse()
413

414
415
416
417
	if len(os.Args) == 1 || *help {
		flag.Usage()
		os.Exit(1)
	}
Etienne Renault's avatar
Etienne Renault committed
418

Etienne Renault's avatar
Etienne Renault committed
419
420
421
422
423
424
425
426
	path, err := os.Executable()
	if err != nil {
		log.Println(err)
	}
	path = filepath.Dir(path)
	maindve2C := path + "/main.dve2C"


Etienne Renault's avatar
Etienne Renault committed
427
	if *list_var {
Hugo Moreau's avatar
Hugo Moreau committed
428
		fmt.Println("State size:", structs.G2PStateSize)
429
		fmt.Println("List of variable names:")
Hugo Moreau's avatar
Hugo Moreau committed
430
431
		for i := 0; i < structs.G2PStateSize; i++ {
			fmt.Println(" - " + C.GoString((*C.char)(structs.G2PVariableNames[i])))
432
433
		}
	}
Etienne Renault's avatar
Etienne Renault committed
434
435
436
437

	if *ltl != "" {
		var mcCmd *exec.Cmd
		if *backend == "ltsmin" {
438
439
			mcCmd = exec.Command(ltsmin_path(),
				"--threads", strconv.Itoa(*nb_threads),
Etienne Renault's avatar
Etienne Renault committed
440
				"--ltl", *ltl, maindve2C)
Etienne Renault's avatar
Etienne Renault committed
441
		} else if *backend == "spot" || *backend == "" {
442
			if !spot_dev_version() {
443
444
445
				if *nb_threads != 1 {
					panic ("This version of spot does not support multithreading")
				}
Etienne Renault's avatar
Etienne Renault committed
446
				mcCmd = exec.Command(spot_path(), maindve2C, "!"+*ltl)
447

448
			} else {
449
450
451
452
				// Use BDD based algorithms
				if *nb_threads == 1 {
					mcCmd = exec.Command(spot_path(), "-e",
						"--model", maindve2C,
453
						"--csv",
454
455
456
457
458
						"--formula", "!"+*ltl)
				} else { // Use parallel algorithms
					mcCmd = exec.Command(spot_path(), "-e",
						"--model", maindve2C,
						"--formula", "!"+*ltl,
459
						"--csv",
460
461
						"--parallel", strconv.Itoa(*nb_threads))
				}
462
			}
Etienne Renault's avatar
Etienne Renault committed
463
464
465
466
467
468
		} else {
			panic("backend '" + *backend + "' unknown!")
		}

		mcCmd.Stdout = os.Stdout
		mcCmd.Stderr = os.Stderr
469
470
		mcCmd.Run()
		mcOut, _ := mcCmd.Output()
Etienne Renault's avatar
Etienne Renault committed
471
472
473
474
		fmt.Println(string(mcOut))
	}

	if *display {
475
476
		var mcCmd *exec.Cmd
		if !spot_dev_version() {
Etienne Renault's avatar
Etienne Renault committed
477
			mcCmd = exec.Command(spot_path(), "-gm", maindve2C, "true")
478
		} else {
Etienne Renault's avatar
Etienne Renault committed
479
			mcCmd = exec.Command(spot_path(), "--model", maindve2C, "--dot=model")
480
		}
Etienne Renault's avatar
Etienne Renault committed
481
482
483
484
485
486
487
488
489
		mcCmd.Stdout = os.Stdout
		mcCmd.Stderr = os.Stderr
		err := mcCmd.Run()
		if err != nil {
			log.Fatalf("command failed with %s\n", err)
		}
		mcOut, err := mcCmd.Output()
		fmt.Println(string(mcOut))
	}
490
491

	if *kripke_ss {
492
493
494
		var out []byte

		if !spot_dev_version() {
Etienne Renault's avatar
Etienne Renault committed
495
			out, _ = exec.Command(spot_path(), maindve2C, "F \"LabelCounter==-1\"").Output()
496
497
		} else {
			out, _ = exec.Command(spot_path(), "-e",
Etienne Renault's avatar
Etienne Renault committed
498
				"--model", maindve2C,
499
500
501
				"--formula", "F \"LabelCounter==-1\"").Output()
		}

502
503
		output := string(out[:])
		r, _ := regexp.Compile(".*unique.*")
504
505
506
507
508
		r1, _ := regexp.Compile(".*transitions.*")
		st := strings.Replace(r.FindString(output), " unique states visited", "", -1)
		tr := strings.Replace(r1.FindString(output), " transitions explored", "", -1)
		fmt.Println("\nKripke Size:\n\t-", st, "states", "\n\t-", tr, "transitions")
		fmt.Println("#kripke," + strings.TrimSpace(st) + "," + strings.TrimSpace(tr))
509
	}
510
}