-- specification AG !(proc1.state = critical & proc2.state = critical)  is true
-- specification AG (proc1.state = entering -> AF proc1.state = critical)  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample
Trace Type: Counterexample
  -> State: 1.1 <-
    semaphore = FALSE
    proc1.state = idle
    proc2.state = idle
  -> Input: 1.2 <-
    _process_selector_ = proc1
    running = FALSE
    proc2.running = FALSE
    proc1.running = TRUE
  -- Loop starts here
  -> State: 1.2 <-
    proc1.state = entering
  -> Input: 1.3 <-
    _process_selector_ = main
    running = TRUE
    proc1.running = FALSE
  -- Loop starts here
  -> State: 1.3 <-
  -> Input: 1.4 <-
    _process_selector_ = proc2
    running = FALSE
    proc2.running = TRUE
  -> State: 1.4 <-