Simulator

A formula that describes the starting states of the simulation (e.g., initial condition x<=2).
A formula that describes the relation between the state prior and posterior to running the program (e.g., the state relation x=xpre+1 describes the deterministic program x:=x+1). You are running KeYmaera X without ModelPlex, please provide manually.
Warning: Your program does not support evolution for {{numSteps}} steps with current step duration {{stepDuration}}. Points to a possible condition where the model ends up in a state without further possible evolution.