| |
|
||||||
|
|
|||||||
<Generator name="Automaton(A-B-Spec-Eventually-B).x.A-B-Machine" ftype="RabinAutomaton"> % % Statistics for Automaton(A-B-Spec-Eventually-B).x.A-B-Machine % % States: 10 % Init/Marked: 1/3 % Events: 4 % Transitions: 20 % StateSymbols: 10 % Attrib. E/S/T: 0/0/0 % <Alphabet> a b c d </Alphabet> <States> A|I|r1m A|R|r1m B|R|r1m A|I|r2m B|F|r2m dump|R|r2m B|R|r2m dump|I|r2m dump|F|r2m A|F|r1m </States> <TransRel> A|I|r1m a A|R|r1m A|I|r1m b B|R|r1m A|R|r1m c A|I|r1m A|R|r1m d A|F|r1m B|R|r1m c A|I|r2m B|R|r1m d B|F|r2m A|I|r2m a A|R|r1m A|I|r2m b B|R|r1m B|F|r2m a dump|R|r2m B|F|r2m b B|R|r2m dump|R|r2m c dump|I|r2m dump|R|r2m d dump|F|r2m B|R|r2m c A|I|r2m B|R|r2m d B|F|r2m dump|I|r2m a dump|R|r2m dump|I|r2m b dump|R|r2m dump|F|r2m a dump|R|r2m dump|F|r2m b dump|R|r2m A|F|r1m a A|R|r1m A|F|r1m b B|R|r1m </TransRel> <InitStates> A|I|r1m </InitStates> <MarkedStates> A|I|r1m A|I|r2m dump|I|r2m </MarkedStates> <RabinAcceptance> <RabinPair name="RabinPair"> <R> A|I|r2m dump|I|r2m </R> <I> A|I|r1m A|R|r1m B|R|r1m A|I|r2m B|F|r2m B|R|r2m A|F|r1m </I> </RabinPair> </RabinAcceptance> </Generator>
libFAUDES 2.33l --- 2025.09.16 --- with "omegaaut-synthesis-observer-observability-diagnosis-hiosys-iosystem-multitasking-coordinationcontrol-timed-simulator-iodevice-priorities-luabindings-hybrid-example-pybindings"