search

isabelle-utp / interaction-trees

Interactions Trees in Isabelle/HOL and a CSP model
6 stars 1 forks source link

Merge branch robochart_nondeterminism_resolving to master #9

Closed RandallYe closed 4 months ago

RandallYe commented 4 months ago

@simondfoster I would like to merge robochart_nondeterminism_resolving into master. Because our JLAMP paper points to that branch, I don't want to change anything in the branch. Instead, I have created a new branch (pre_merge_robochart) from that branch, and merged your latest changes from the master. I have checked RoboChart animation still works. So I think it is a good time to merge RoboChart changes back to master now.

simondfoster commented 4 months ago

Hello Randall. I had to do the merge manually, due to a couple of changes upstream. I also needed to slightly modify your simulation code, so that it uses the ghc binary in ISABELLE_GHC. However, the animation for Patrol_Robot at least now works. Please can you check that the master is now in an acceptable state for you.

RandallYe commented 4 months ago

Hi @simondfoster , thanks a lot for it. The master is in a good state for me now. I may need some time to figure how to fix issues for another two examples: RoboChart_basic and RoboChart_ChemicalDetector_autonomous

I also needed to slightly modify your simulation code, so that it uses the ghc binary in ISABELLE_GHC.

I didn't see where you have changed

Patrol_Robot works for me too.

For another RoboChart_basic, I use animate from ITree_Simulation. It fails to compile, and the log is shown below.

Simulate.hs:14:15: error: [GHC-76037]
    Not in scope: type constructor or class ‘Uval’
   |
14 | instance Show Uval where
   |               ^^^^

Simulate.hs:15:8: error: [GHC-76037]
    Not in scope: data constructor ‘UnitV’
   |
15 |   show UnitV = "()"
   |        ^^^^^

Simulate.hs:16:9: error: [GHC-76037]
    Not in scope: data constructor ‘BoolV’
   |
16 |   show (BoolV x) = show x

For the RoboChart_ChemicalDetector_autonomous example, I was able to animate one controller but not another. Now I cannot animate any controller or the whole module now. The runtime error is shown below.

Starting ITree Simulation...
Simulation: Finite_Set.hs:21:1-52: Non-exhaustive patterns in function card
RandallYe commented 4 months ago

Simon, I have fixed RoboChart_basic by changing to animate1 from RoboChart_simulate.thy.

For RoboChart_ChemicalDetector_autonomous, it still doesn't work. I have investigated the issue and will create a new issue for it.