search

isabelle-utp / interaction-trees

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

Animation of RoboChart_ChemicalDetector_autonomous_maincontroller doesn't work #10

Open RandallYe opened 1 month ago

RandallYe commented 1 month ago

After changing to Isabelle 2023, now the animation of RoboChart_ChemicalDetector_autonomous_maincontroller doesn't work. The runtime error is shown below.

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

I suspect it might be due to the code generation of Number_Type. For example, now value "Chemical_Chem2_list" in RoboChart_ChemicalDetector_autonomous_general.thy cannot be evaluated. Similarly, mk_blist also cannot be evaluated. I had a look at the simulation code for Isabelle.

The definition of mk_built: "mkblist xs = map (bmake TYPE('n)) (lseqn xs CARD('n))"

For the new Isabell 2023, it generates

mk_blist uu xs =  map (Bounded_List.Bmake HOL.Type)   (lseqn xs ((Finite_Set.card :: Set.Set a -> Arith.Nat) Set.top_set));
`

But for the old Isabelle/'2021, it generated.

mk_blist uu xs =  map (Bmake Type) (lseqn xs (of_phantom (card_UNIV :: Phantom a Nat)));