Strix Demo
Assumptions:
true
Guarantees:
G (request_0 -> F grant_0) G (request_1 -> F grant_1) G (!grant_0 || !grant_1) (!grant_0 & !request_0) W request_0 (!grant_1 & !request_1) W request_1
Input propositions:
request_0, request_1
Output propositions:
grant_0, grant_1
Format:
Mealy machine
AIGER circuit
BDD
Options:
Minimize controller
Synthesize! (Timelimit: 60 sec)
We use
dot
to render the controller to SVG.