Closing a channel causes GMC synthesis to fail.

[antonis19]

In the program below, because of the line where the channel is closed the following happen:

i) GMC synthesis fails.

ii) The global graph constructed ends up being simpler than when the channel is not closed. When the channel is not closed the global graph becomes very complex (contains many diamond and "|" nodes).

package main

func Sender(ch chan <- int, end chan <- bool) {
    ch <-42 
    close(ch)  // <------
    end <- true
}

func Receiver(ch <- chan int, end chan <- bool) {
    <-ch
    end <-true
}

func main() {
    ch := make(chan int)
    end := make(chan bool)
    go Sender(ch,end)
    go Receiver(ch,end)
    <-end
    <-end
}