// Example that demonstrates how to use counting automata in this automata library
// Author: Jacob Maxam, Marcel Ebbinghaus
// Date: 2020-07-12


// Declare a nondeterministic counting automaton called "nca1".
CountingAutomaton nca1 = (
     alphabet = {a b},
	 counters = {c d},
     states = {q1 q2},
     initialConditions = {
		 (q1 "true")
		 (q2 "false")
	 },
     finalConditions = {
		 (q1 "false")
		 (q2 "(or (and (< c 2) (>= d 0)) (= d 2) (and (> d 0) (= c 7)))")
	 },
     transitions = {
         (q1 a "true" {c := "(+ d 1)", d := "(+ d 1)"} q1)
		 (q1 b "(> c 3)" {} q2)
		 (q2 a "true" {c := "(+ c 1)"} q2)
		 (q2 b "true" {} q1)
     }
);

CountingAutomaton nca2 = complement(nca1);
print(nca2);