A3: working version, i hope

go/TrafficLights/TrafficLight.go

@@ -4,7 +4,7 @@ import (
 	"fmt"
 )
 
-var debuggingAllowed = true
+var printDebugMessages = false
 
 type CardinalDirection string
 
@@ -15,131 +15,137 @@ const (
 	west  = CardinalDirection("West")
 )
 
-var Directions = []CardinalDirection{
-	north, south, east, west,
-}
-
-type Colour string
-
-const (
-	red    = Colour("\u001B[31m Red \u001B[0m")
-	green  = Colour("\u001B[33m Green \u001B[0m")
-	yellow = Colour("\u001B[32m Yellow \u001B[0m")
-)
-
-var Colours = []Colour{
-	red, green, yellow,
-}
-
 func nextDirection(currentDirection CardinalDirection) CardinalDirection {
 	switch currentDirection {
 	case north:
 		return east
-	case south:
-		return west
 	case east:
 		return south
+	case south:
+		return west
 	case west:
 		return north
-	default:
-		return north
 	}
-
+	return north
 }
 
-func nextColour(currentColour Colour) Colour {
+func oppositeDirection(currentDirection CardinalDirection) CardinalDirection {
-	switch currentColour {
+	switch currentDirection {
-	case red:
+	case north:
-		return green
+		return south
-	case green:
+	case east:
-		return yellow
+		return west
-	case yellow:
+	case south:
-		return red
+		return north
-	default:
+	case west:
-		return red
+		return east
 	}
+	return north
+}
+
+type Colour int
+
+const (
+	red Colour = iota
+	green
+	yellow
+)
+
+func (colour Colour) String() string {
+	switch colour {
+	case red:
+		return "Red"
+	case yellow:
+		return "Yellow"
+	case green:
+		return "Green"
+	default:
+		return "null"
+	}
+}
+
+func nextColour(colour Colour) Colour {
+	return (colour + 1) % (yellow + 1)
+}
+
+var northChannel = make(chan string)
+var southChannel = make(chan string)
+var eastChannel = make(chan string)
+var westChannel = make(chan string)
+
+func getChannel(direction CardinalDirection) chan string {
+	switch direction {
+	case north:
+		return northChannel
+	case south:
+		return northChannel
+	case east:
+		return eastChannel
+	case west:
+		return eastChannel
+	}
+	return nil
 }
 
 func main() {
 	var quitChannel = make(chan string)
 
-	var northColour = make(chan Colour, 2)
+	go TrafficLight(north)
-	var southColour = make(chan Colour, 2)
+	go TrafficLight(south)
-	var eastColour = make(chan Colour, 2)
+	go TrafficLight(east)
-	var westColour = make(chan Colour, 2)
+	go TrafficLight(west)
-
-	var northDirection = make(chan string, 2)
-	var southDirection = make(chan string, 2)
-	var eastDirection = make(chan string, 2)
-	var westDirection = make(chan string, 2)
-
-	go TrafficLight(north, northColour, southColour, northDirection, eastDirection, southDirection)
-	go TrafficLight(south, southColour, northColour, southDirection, westDirection, northDirection)
-	go TrafficLight(east, eastColour, westColour, eastDirection, southDirection, westDirection)
-	go TrafficLight(west, westColour, eastColour, westDirection, northDirection, eastDirection)
 
 	<-quitChannel
 }
 
-func TrafficLight(direction CardinalDirection, currentColour <-chan Colour, oppositeColour chan<- Colour, currentDirection <-chan string, nextDirectionChan chan<- string, oppositeDirection chan<- string) {
+func TrafficLight(direction CardinalDirection) {
 	var colour = red
 
-	if direction != north && direction != south {
+	if direction == east || direction == west {
-		nextDirectionChan <- string(nextDirection(direction))
+		handover("changeDirection", direction)
-
 	}
 
 	for {
 		show(direction, colour)
 
 		if colour == red {
-			syncLight(currentDirection, oppositeDirection)
+			sync("wait", direction)
-			changeDirection(direction, currentDirection, nextDirectionChan)
+			handover("changeDirection", direction)
 		}
-		colour = changeLight(colour, currentColour, oppositeColour)
 
+		sync("changeLight"+string(nextColour(colour)), direction)
+		colour = nextColour(colour)
 	}
 }
 
-func syncLight(currentDirection <-chan string, oppositeDirection chan<- string) {
+func handover(message string, direction CardinalDirection) {
-	oppositeDirection <- "sync"
+	getChannel(nextDirection(direction)) <- message
-	select {
-	case msg := <-currentDirection:
-		if msg == "sync" {
-			return
 
-		}
+	select {
+	case msg := <-getChannel(direction):
+		debug(msg)
 	}
 }
 
-func changeDirection(direction CardinalDirection, currentDirection <-chan string, nextDirectionChan chan<- string) {
+func sync(message string, direction CardinalDirection) {
-	nextDirectionChan <- string(nextDirection(direction))
+	defer debug(string(direction) + " done with message " + message)
-	select {
-	case msg := <-currentDirection:
-		if msg == string(direction) {
-			return
-		}
-	}
-}
 
-func changeLight(colour Colour, currentColour <-chan Colour, oppositeColour chan<- Colour) Colour {
+	debug(string(direction) + " sync with message " + message)
-	oppositeColour <- nextColour(colour)
 
 	select {
-	case msg := <-currentColour:
+	case getChannel(direction) <- message:
-		if msg == nextColour(colour) {
+	case msg := <-getChannel(direction):
-			return nextColour(colour)
+		debug(msg)
-		}
 	}
-	return colour
+
 }
 
 func show(direction CardinalDirection, colour Colour) {
-	fmt.Println(string(direction), " : ", string(colour))
+	fmt.Println(string(direction), " : ", colour.String())
 }
 
 func debug(message string) {
-	if debuggingAllowed {
+	if printDebugMessages {
-		fmt.Println("Debug:", message)
+		fmt.Println("Debug: " + message)
 	}
 }

mCRL2/TrafficLights/v4/v4_spec.mcrl2

@@ -52,7 +52,6 @@ proc
 				-> wait . ChangeDirection(direction) %Richtungswechsel, wenn wieder zurück
 					. ChangeLight(direction, colour) % -> zur nächsten Farbe wechseln.
 				<> ChangeLight(direction, colour) %ansonsten zum nächsten Zustand wechseln.
-		
 	;
 
 	ChangeDirection(direction : CardinalDirection) =