Try

Enter a system and two states, and Id(s, t) and the other questions are computed together. Every answer is returned only after a checker, running apart from the computation, has checked its certificate. What the inputs mean and how to read the results are in “Docs”.