> isabelle: e6f0c361ac73 tip
> afp: 2a0dc69c001b tip
> Building LTL_to_GBA ...
>
> LTL_to_GBA FAILED
> (see also
> /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/LTL_to_GBA)
>
> => ('a, 'c) node_scheme set => ('a, 'c) node_scheme set"
> Phase "id_op"
> Failed to identify: create_name_gba
> Failed to identify: ti_Lcnv
> 0.048s elapsed time, 0.288s cpu time, 0.000s GC time
> ### theory "LTL_to_GBA_impl"
> ### 61.088s elapsed time, 341.092s cpu time, 22.988s GC time
> *** Failed to apply proof method (line 1156 of
> "/mnt/home/haftmann/data/afp/master/thys/LTL_to_GBA/LTL_to_GBA_impl.thy"):
> *** goal (1 subgoal):
> *** 1. (?c,
> *** %\<phi>.
> *** create_name_gba \<phi> >>=
> *** (%A. gba_to_idx A >>=
> *** (%A'. stat_set_data_nres (card (frg_V A)) (card (frg_V0 A'))
> *** (igbg_num_acc A') >>=
> *** (%_. RETURN A'))))
> *** : \<langle>Id\<rangle>ltln_rel \<rightarrow>
> *** \<langle>igbav_impl_rel_ext unit_rel nat_rel
> *** (\<langle>Id\<rangle>fun_set_rel)\<rangle>nres_rel
> *** At command "apply" (line 1156 of
> "/mnt/home/haftmann/data/afp/master/thys/LTL_to_GBA/LTL_to_GBA_impl.thy")
> CAVA_buildchain1 CANCELLED
> CAVA_buildchain3 CANCELLED
> CAVA_LTL_Modelchecker CANCELLED
> Unfinished session(s): CAVA_LTL_Modelchecker, CAVA_buildchain1,
> CAVA_buildchain3, LTL_to_GBA
> 0:20:58 elapsed time, 0:59:35 cpu time, factor 2.84-- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
