From: Chao Wang (Wangc_at_colorado.edu)
Date: Tue Jan 20 2004 - 15:51:34 MST
Fang:
The current implementation of ltl_model_check does not have automatic
abstraction refinement.
However, Cone-of-influence (COI) reduction has been used on the composed
system MxA (M - model; A - Buechi automaton), so as to retain only the
relevant part of the system for language-emptiness checking. To disable
the COI reduction, one has to modified the source code. Please check the
call to Mc_ConstructReducedFsm() in vis/src/ltl.c, you can comment it out,
or inspect the latches that are actually in the reduced Fsm.
Besides, different symbolic algorithms for language-emptiness are
automatically selected based on the "strength" of the Buechi automaton.
(This has been discribed in Bleom, Ravi and Somenzi, "Efficient Decision
Procedures for LTL Model Checking", CAV99.) To disable this streng
reduction feature, please use the "-X" option.
Chao
On Tue, 20 Jan 2004, Fang Wang wrote:
>
> Hello,
>
> I'd like to know if there are some automatic reduction
> methods in the VIS LTL model checking application.
> If yes, how to deactivate them.
>
> Sincerly
> Fang wang
>
>
>
>
--
This archive was generated by hypermail 2.1.7 : Tue Jan 20 2004 - 15:53:58 MST