A forum for Spin users

You are not logged in.

#1 2013-02-19 12:50:34

Registered: 2011-05-13
Posts: 43

Possible bug in ispin110.tcl

The customization of "+minimized automata (slow)" might be buggy.
In the source code of ispin110.tck, at lines 3885 - 3889, the original code is

if {$V_Panel_3} {
if {$ma_mode == 1} { set cargs "$cargs -DMA=[$t.top.right.row4.ent get]" }
if {$ma_mode == 1} { set cargs "$cargs -DMA=$ival(4)" }
} else {

It seems suspicious to have two if ($ma_mode == 1) consecutively together. My understanding is that the first line reads the input from the text box "Size for Minimized Automaton", and the second one uses the default value (100). If I type 200 in the text box, then the compiler option has two -DMA consecutively, e.g., -DMA=200 -DMA=100.

I boldly change the code as follows.  It worked properly. Can you please confirm if my change is valid? 

if {$V_Panel_3}   # If the text box is modified
  if {$ma_mode == 1} { set cargs "$cargs -DMA=[$t.top.right.row4.ent get]" } # If the checkbox is selected, use the text box value
  if {$ma_mode == 1} { set cargs "$cargs -DMA=$ival(4)" }  # If the checkbox is selected, use the default value 100


#2 2013-02-20 02:47:12

Registered: 2010-11-18
Posts: 678

Re: Possible bug in ispin110.tcl

Yes, you're right!


Board footer

Powered by FluxBB