Tobe,
I can reproduce your problem with the vis-1.4 distribution. The
problem is solved in our current development version. I believe it is
related to a bug fix in a CUDD function that was introduced in the
latest release.
I'll send you the corrected file, so that we can check whether this is
the explanation.
Fabio
>>>>> "TT" == Tobe Toben <Tobe.Toben@Informatik.Uni-Oldenburg.DE> writes:
TT> Hello,
TT> I'm generating the timed automata semantics of so-called PLC-Automata [1]
TT> as verilog code in order to modelcheck them by means of VIS. Therefore I
TT> had to implement a mechanism to ensure that either every module increases
TT> their clocks or exactly one module make a discrete transition.
TT> But since I added this grant mechanism, VIS keeps segfaulting whenever it
TT> is about to write out the debug trace.
TT> I have attached an example. My steps are:
TT> $ vl2mv autControl.v
TT> autControl.v
TT> $ vis -x -f autControl.vis
TT> Warning: Some variables are unused in model main.
TT> Warning: Some variables are unused in model aut1.
TT> Warning: Some variables are unused in model Control.
TT> # MC: formula failed --- AG(!(aut1.state=1))
TT> Segmentation Fault
TT> :-( Perhaps you could have a look at my example.
TT> Thank you,
TT> Tobe.
TT> I can reproduce the behaviour on:
TT> . SunOS fats 5.5.1 Generic_103640-12 sun4u sparc SUNW,Ultra-2
TT> (vis release 1.4 (compiled Tue Jun 5 18:05:50 MET DST 2001))
TT> . Linux extreme 2.4.8 #6 Sat Aug 11 11:10:20 CEST 2001 i686 unknown
TT> (vis release 1.4 (compiled 31-Mai-01 at 7:06 PM))
TT> [1] H.Dierks. PLC-Automata: A New Class of Implementable Real-Time Automata
TT> ftp://theoretica.Informatik.Uni-Oldenburg.DE/pub/Papers/hd97-arts.ps.gz
This archive was generated by hypermail 2b30 : Tue Aug 28 2001 - 10:07:26 MDT