A forum for Spin users
You are not logged in.
Pages: 1
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
}
else
{
if {$ma_mode == 1} { set cargs "$cargs -DMA=$ival(4)" } # If the checkbox is selected, use the default value 100
}
Offline
Pages: 1