Suppose I have modeled the behavior of my system by Deterministic Finite Automaton (DFA) A, and I need to check if it satisfies a safety condition. I have created another DFA S, which represents the behavior that invalidates the safety property. Then I need to take intersection of these two to see if A contains bad traces. Finally, I need to code A into C program.
Could you please introduce me to a few tools that take two DFA as input and tell me if the intersection is not empty?
Are there tools that translate the DFA directly to C or Java Code?