
module main
{
  type state_t = enum { RED, GREEN };

  var red1, green1 : state_t;
  var red2, green2 : state_t;

  init {
    red1 = RED; green1 = GREEN;
    red2 = RED; green2 = GREEN;
  }

  transition {
    // Traffic light 1 transitions
    if red1 == RED && green1 == GREEN {
      red1' = GREEN; green1' = RED;
    }
    else {
      red1' = RED; green1' = GREEN;
    }

    // Traffic light 2 transitions
    if red2 == RED && green2 == GREEN {
      red2' = GREEN; green2' = RED;
    }
    else {
      red2' = RED; green2' = GREEN;
    }
  }
}
