Hello, I'm just trying to get a better understanding of what's going on at syntcomp.
The specification https://github.com/meyerphi/syntcomp-reference/blob/master/specifications/realizable/ltl2dba22.tlsf makes perfect sense to me. And the target model is a mealy machine.
I understand that syntcomp requires implementations to be expressed in the aag format. I'm having trouble though interpreting https://github.com/meyerphi/syntcomp-reference/blob/master/implementations/realizable/ltl2dba22.aag as a mealy machine.
Could someone elaborate? Alternatively, is there a tool that will take this aag and transform it into an output that is more readily interpreted by a human that understands mealy machines?
Thank you!
Hello, I'm just trying to get a better understanding of what's going on at syntcomp.
The specification https://github.com/meyerphi/syntcomp-reference/blob/master/specifications/realizable/ltl2dba22.tlsf makes perfect sense to me. And the target model is a mealy machine.
I understand that syntcomp requires implementations to be expressed in the aag format. I'm having trouble though interpreting https://github.com/meyerphi/syntcomp-reference/blob/master/implementations/realizable/ltl2dba22.aag as a mealy machine.
Could someone elaborate? Alternatively, is there a tool that will take this aag and transform it into an output that is more readily interpreted by a human that understands mealy machines?
Thank you!