Deadlock not detected in simple program

[antonis19]

Dingo-Hunter is not able to detect a deadlock for the program below: (you can also find the code in this pastebin link https://pastebin.com/C4Md3yLB). The extracted CFSMs are correct, however the GMC synthesis succeeds for all 3 machines, when in fact it should fail.

This is the most simple example I am showing. I have other examples where deadlocks are not detected, when previously they were detected. Is it possible that an update in GMC synthesis tool caused deadlocks to go undetected ?

package main

type end struct{}

// !int . ?string . end
func party1(intChannel chan int, stringChannel chan string, endChannel chan end) {
	//!int
	intChannel <- 42
	// ?string
	<-stringChannel
	// end
	endChannel <- end{}

}

// !string . ?int . end
func party2(intChannel chan int, stringChannel chan string, endChannel chan end) {
	//!string
	stringChannel <- "Hello World"
	// ?int
	<-intChannel
	//end
	endChannel <- end{}
}

func main() {
	intChannel := make(chan int)
	stringChannel := make(chan string)
	endChannel := make(chan end)
	go party1(intChannel, stringChannel, endChannel)
	go party2(intChannel, stringChannel, endChannel)
	<-endChannel
	<-endChannel
}

[nickng]

Is it possible for you to attach the generated global graph (and the output of the synthesis?

[antonis19]

Here is the output of the synthesis:

user@Lenovo:~/go/src/github.com/nickng/dingo-hunter/third_party/gmc-synthesis$ ./runsmc.py inputs/output_cfsms 
----------------- GMC Check -----------------
Parsing CFSMs file... (factor 0)
Machine 5: True
Machine 3: True
Machine 1: False
Machine 2: False
Machine 4: True
Machine 0: False

----------------- Global Graph Synthesis -----------------
Parsing PN file...
Transformation 1 (One-Source Petri Net)
Transformation 2 (Joined Petri Net)
Transformation 3 (PN to Pre-Global Graph)
Transformation 4 (Pre-Global Graph to Global Graph)
Global Graph Construction Done; see output folder.

Execution time:  0.150355100632   ( Start: 1527690669.44  --> End: 1527690669.59 )

These are the generated graphs:

[nickng]

/cc @julien-lange

Confirmed as incorrect behaviour - fix will be issued in synthesis tool