You can test our model checker for FJ (combination of a translator FJ2HORS from FJ to mu-HORS, and a model checker RTrecS for mu-HORS). Enter a FJ program in the box below, and press the "submit" button. It checks that the program does not fail (specified by a special global action "fail") nor cause "message not understood" errors. (Among the examples above, you cannot test twofiles.java, as you need to write a property-automaton by yourself and pass it to RTrecS.) The underlying model checker RTRecS can be tested here. You can check only small examples as the time-out is set to one second.
Programs used in the experiments in the draft paper above: