• Alexandre Duret-Lutz's avatar
    DVE2: preliminary implementation of compressed states. · c938e652
    Alexandre Duret-Lutz authored
    * iface/dve2/dve2.cc (dve2_compressed_state): New class.
    (callback_context): Deal with general state*s, not dve2_state*s.
    (transition_callback_compress): New function.
    (dve2_kripke): Take a compress option.
    (get_init_state, compute_state_condition, succ_iter,
    format_state, state_condition): Handle compressed states.
    (get_vars, compute_state_condition_aux): New helper methods.
    * iface/dve2/dve2.hh (load_dve2): Add a compress option.
    * iface/dve2/dve2check.cc: Add a -z option.
    * iface/dve2/finite.test, iface/dve2/dve2check.test: Add more
    tests.
    c938e652
intvcomp.cc 3.51 KB