flashing_led_with_invariant.out

     = ([(0%nat,
        [Tm (Output 1%nat)
           [CndLe (EClock (CVar "x")) (ELit 1);
           CndLe (ELit 1) (EClock (CVar "x"));
           CndLe (EClock (CVar "x")) (ELit 2)] [] 2%nat [(2, CVar "x")];
        Tm (Input 0%nat) [CndLt (ELit 0) (ELit 5)] [CVar "y"] 1%nat
          [(5, CVar "y")]]);
       (1%nat,
       [Tm (Input 1%nat) [CndLe (ELit 0) (ELit 1)] [CVar "x"] 0%nat
          [(1, CVar "x")]]);
       (2%nat,
       [Tm (Output 0%nat)
          [CndLe (EClock (CVar "x")) (ELit 2);
          CndLe (ELit 2) (EClock (CVar "x")); CndLe (ELit 0) (ELit 1)]
          [CVar "x"] 0%nat [(1, CVar "x")];
       Tm (Input 0%nat) [CndLe (EClock (CVar "x")) (ELit 2)] [CVar "y"] 3%nat
         [(2, CVar "x")]]);
       (3%nat,
       [Tm (Input 1%nat) [CndLe (EClock (CVar "x")) (ELit 2)] [] 2%nat
          [(2, CVar "x")];
       Tm (Output 2%nat)
         [CndLe (EClock (CVar "x")) (ELit 2);
         CndLe (ELit 2) (EClock (CVar "x"));
         CndLt (EClock (CVar "y")) (ELit 5)] [] 1%nat [(5, CVar "y")]])], SOME 1)
     : program