[isabelle-dev] Problem in the AFP

[Florian Haftmann]

> 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20150321/1fa358a3/attachment.asc>