Animation of a patrol robot model
Based on operational semantics of RoboChart using Interaction Trees
![](/~ky582/showcase/animation_of_patrol_robot/Featured_hu022584ec861fb5fb603cb43189fc6f04_1083944_720x2500_fit_q75_h2_lanczos_3.webp)
Here we demonstrate the animation of a patrol robot model below using Interaction Trees in Isabelle/HOL.
![RoboChart model with nondeterministic choice and shared variables](/~ky582/showcase/animation_of_patrol_robot/PatrolMod_hu38db1eb6168b86b42bf1b461bf10a67e_2104495_e3a7d1138351897ee48dbbbb0f070be7.webp)
The corridor for the robot to patrol has three sections, shown below.
![Sectioned corridor with soft and hard boundaries](/~ky582/showcase/animation_of_patrol_robot/Corridor_sections_hu9c767e2eb6e7fe0b4aefa2a101f579ca_248902_3f86ac5ad25e9f35e4eebddb4b3995da.webp)
The Isabelle/HOL theories for the animation can be found here.