2 # the next line restarts using wish \
3 exec wish c
:/cygwin
/bin
/xspin
-- $*
5 # cd ;# enable to cd to home directory by default
8 # adjust the first argument to wish above with the name and
9 # location of this tcl/tk file on your system, if different.
12 # if you use cygwin, do not refer to the file as /usr/bin/xspin
13 # /usr/bin is a symbolic link to /bin, which really
14 # lives in c:/cygwin, hence the contortions above
16 # on Unix/Linux/Solaris systems
17 # replace the first line with something like
19 # using the pathname for the wish executable on your system
21 #======================================================================#
22 # Tcl/Tk Spin Controller, written by Gerard J. Holzmann, 1995-2005. #
23 # See the README.html file for full installation notes. #
24 # http://spinroot.com/spin/whatispin.html #
25 #======================================================================#
26 set xversion
"5.1.0 -- 24 April 2008"
28 # -- Xspin Installation Notes (see also README.html):
30 # 1. On Unix systems: change the first line of this file to point to the wish
31 # executable you want to use (e.g., wish4.2 or /usr/local/bin/wish8.0)
32 # ==> be careful, the pathname should be 30 characters or less
34 # 2. If you use another C compiler than gcc, change the set CC line below
36 # 3. Browse the configurable options below if you would like to
37 # change or adjust the visual appearance of the GUI
39 # 4. If you run on a PC, and have an ancient version of tcl/tk,
40 # you must set the values fo Unix, CMD, and Go32 by hand below
41 # => with Tcl/Tk 7.5/4.1 or later, this happens automatically
43 # set CC "cc -w -Wl -woff,84" ;# ANSI-C compiler, suppress warnings
44 # set CC "cl -w -nologo" ;# Visual Studio C/C++ compiler, prefered on PCs
45 set CC
"gcc -w" ;# standard gcc compiler - no warnings
48 # set CPP "cpp" ;# the normal default C preprocessor
49 set CPP
"gcc -E -x c" ;# c preprocessor, assuming we have gcc
51 set SPIN
"spin" ;# use a full path-name if necessary, e.g. c:/cygwin/bin/spin.exe
52 set DOT
"dot" ;# optional, graph layout interface
53 ;# no prob if dot is not available
54 set BG
"white" ;# default background color for text
55 set FG
"black" ;# default foreground color for text
56 set CMD
"" ;# default is empty, and adjusted below
57 set Unix
1 ;# default is Unix, but this is adjusted below
58 set Ptype
"color" ;# printer-type: mono, color, or gray
59 set NT
0 ;# scratch variable, ignore
63 toplevel .debug
; #debugging window
64 text .debug.txt
-width 80 -height 60 -relief raised
-bd 2 \
65 -yscrollcommand ".debug.scroll set"
66 scrollbar .debug.scroll
-command ".debug.txt yview"
67 pack .debug.scroll
-side right
-fill y
68 pack .debug.txt
-side left
73 catch { .debug.txt insert end
"\n$txt" }
76 if [info exists tcl_platform
] {
77 set sys
$tcl_platform(platform
)
78 # if {$sys == "macintosh"} {
79 # ... no adjustments needed? ...
81 if {[string match windows
$sys]} {
82 set Unix
0 ;# means Windows95/98/2000/NT/XP
84 # if {[auto_execok cl] != ""} {
85 # set CC "cl -w -nologo" ;# Visual Studio compiler, PCs
89 if {$tcl_platform(os
) == "Windows 95"} {
90 set CMD
"command.com" ;# Windows95
96 #-- GUI configuration options - by Leszek Holenderski <lhol@win.tue.nl>
98 set HelvBig
-Adobe-Helvetica
-Medium
-R
-Normal
--*-120-*-*-*-*-*-*
100 if {$NT} { ;# on a windows nt machine
101 set SmallFont
"-*-Courier-Bold-R-Normal--*-110-*"
102 set BigFont
"-*-Courier-Bold-R-Normal--*-110-*"
104 set SmallFont
"-*-Courier-Bold-R-Normal--*-80-*"
105 set BigFont
"-*-Courier-Bold-R-Normal--*-80-*"
108 # Some visual aspects of Xspin GUI can be configured by the user.
109 # On PCs, the values of configuration options that are hard-coded
110 # into this script can be modified (see below). On Unix, in addition to
111 # (or rather, instead of) the manual modification, the values can be set in
112 # an Xspin resource file ($HOME/.xspinrc) and/or in the X11 default resource
113 # file (usually, $HOME/.Xdefaults).
115 # Since the same option can be specified in several places, options can have
116 # several, possibly inconsistent, values. The value which takes effect is
117 # determined by the order in which options are scanned. The values specified
118 # later in the order have higher priority. First, hard-coded options are
119 # scanned, then options specified in .Xdefaults, and finally options
120 # specified in .xspinrc.
122 # When setting configuration options in an .xspinrc file, convert the
123 # settings below to the format of an X11 resource file. For example,
125 # # width of scrollbars (any Tk dimension, default 15 pixels)
126 # option add *Scrollbar.width 13 startupFile
128 # should be converted to
130 # ! width of scrollbars (any Tk dimension, default 15 pixels)
131 # *Scrollbar.width 13
132 # In .Xdefaults file, configuration options should be preceded by the
133 # application's name, so the above option should be converted to
135 # ! width of scrollbars (any Tk dimension, default 15 pixels)
136 # xspin*Scrollbar.width 13
137 # side on which side scrollbars are put (left or right, default=right)
139 option add
*Scrollbar.side left startupFile
142 # width of scrollbars (any Tk dimension, default 15 pixels)
143 option add
*Scrollbar.width
13 startupFile
144 # width of borders (in pixels, typically 1 or 2, default 2)
145 option add
*borderWidth
1 startupFile
146 # initial width of the input/log area (in characters, default 80)
147 option add
*Input
*Text.width
72 startupFile
148 option add
*Log
*Text.width
72 startupFile
149 # initial height of the input area (in lines, default 24)
150 option add
*Input
*Text.height
20 startupFile
151 # initial height of the log area (in lines, default 24)
152 option add
*Log
*Text.height
5 startupFile
153 # size of the handle used to adjust the height of the log area
154 # (in pixels, default 0)
155 option add
*Handle.width
10 startupFile
156 option add
*Handle.height
10 startupFile
158 # colors for the input/log area
159 option add
*Input
*Text.background white startupFile
160 option add
*Input
*Text.foreground black startupFile
161 option add
*Log
*Text.background gray95 startupFile
162 option add
*Log
*Text.foreground black startupFile
163 # colors for the editable/read-only area
164 option add
*Entry.background white startupFile
165 option add
*Edit
*Text.background white startupFile
166 option add
*Edit
*Text.foreground black startupFile
167 # colors for the editable/read-only area
168 option add
*Read
*Text.background gray95 startupFile
169 option add
*Read
*Text.foreground black startupFile
171 # fonts for the input/log area (default is system dependent,
172 # usually -*-Courier-Medium-R-Normal--*-120-*)
173 option add
*Input
*Text.
font -*-Helvetica-Medium
-R
-Normal
--*-120-* startupFile
174 #option add *Input*Text.font -schumacher-clean-medium-r-normal--*-120-*-60-* startupFile
175 #option add *Log*Text.font -schumacher-clean-medium-r-normal--*-120-*-60-* startupFile
178 # simple texts (dialogs which present read-only texts, such as help)
179 option add
*SimpleText.Text.width
60
180 option add
*SimpleText.Text.height
30
181 option add
*SimpleText.Text.background white
183 # sections (decorated frames for grouping related buttons)
184 option add
*Section
*Title.
font -*-Helvetica-Bold
-R
-Normal
--*-100-* startupFile
186 #option add *Section*Checkbutton.font -*-Helvetica-Medium-R-Normal--*-100-* startupFile
187 #option add *Section*Radiobutton.font -*-Helvetica-Medium-R-Normal--*-100-* startupFile
188 #option add *Section*Label.font -*-Helvetica-Medium-R-Normal--*-100-* startupFile
190 ################ end of configurable parameters #######################
192 wm title .
"SPIN CONTROL $xversion"
201 #### seed the advanced parameters settings
203 set e
(0) "Physical Memory Available (in Mbytes): "
205 set expl
(0) "explain"
207 set e
(1) "Estimated State Space Size (states x 10^3): "
209 set expl
(1) "explain"
211 set e
(2) "Maximum Search Depth (steps): "
213 set expl
(2) "explain"
215 set e
(7) "Nr of hash-functions in Bitstate mode: "
217 set expl
(7) "explain"
219 set e
(3) "Extra Compile-Time Directives (Optional): "
223 set e
(4) "Extra Run-Time Options (Optional): "
227 set e
(5) "Extra Verifier Generation Options: "
231 set ival
(6) 1 ;# which error is reported, default is 1st
234 # allow no more than one entry per selection
235 catch { tk_listboxSingleSelect Listbox
}
237 proc msg_file
{f nowarn
} {
241 while {[gets $ef line
] > -1} {
243 if {[string first
"warning" $line] < 0} {
244 set msg
"$msg\n$line"
247 set msg
"$msg\n$line"
253 scan $tk_version "%d.%d" tk_major tk_minor
257 if {[auto_execok $SPIN] == "" \
258 ||
[auto_execok $SPIN] == 0} {
259 set version
"Error: No executable $SPIN found..."
262 set version
[exec $SPIN -V]
264 catch { exec $SPIN -V >&pan.tmp
} err
266 set version
[msg_file pan.tmp
1]
269 puts "is there a $SPIN and a go32.exe?"
272 if {[string first
"Spin Version 5" $version] < 0 \
273 && [string first
"Spin Version 4" $version] < 0 \
274 && [string first
"Spin Version 3" $version] < 0 } {
275 set version
"Spin Version not recognized: $version"
281 menubutton .
menu.
file -text "File.." \
282 -relief raised
-menu .
menu.
file.m
283 menubutton .
menu.run
-text "Run.." -fg red
\
284 -relief raised
-menu .
menu.run.m
285 menubutton .
menu.edit
-text "Edit.." \
286 -relief raised
-menu .
menu.edit.m
287 menubutton .
menu.view
-text "View.." \
288 -relief raised
-menu .
menu.view.m
289 label .
menu.title
-text "SPIN DESIGN VERIFICATION" -fg blue
292 label .
menu.lno
-text "Line#:" -relief raised
293 entry .
menu.ent
-width 6 -textvariable lno
\
294 -relief sunken
-background white
-foreground black
295 bind .
menu.ent
<Return
> {
296 .inp.t tag remove hilite
0.0 end
297 .inp.t tag add hilite
$lno.0 $lno.1000
298 .inp.t tag configure hilite
-background $FG -foreground $BG
299 .inp.t yview
-pickplace [expr $lno-4]
302 label .
menu.fnd1
-text "Find:" -relief raised
303 entry .
menu.fnd2
-width 8 -textvariable pat
\
304 -relief sunken
-background white
-foreground black
305 bind .
menu.fnd2
<Return
> {
306 .inp.t tag remove hilite
0.0 end
307 forAllMatches .inp.t
$pat
310 menubutton .
menu.help
-text "Help" -relief raised
\
314 .
menu.
file {left
frame w
} \
315 .
menu.edit
{left
frame w
} \
316 .
menu.view
{left
frame w
} \
317 .
menu.run
{left
frame w
} \
318 .
menu.help
{left
frame w
} \
319 .
menu.title
{left
frame c expand
} \
320 .
menu.fnd2
{right
frame e
} \
321 .
menu.fnd1
{right
frame e
} \
322 .
menu.ent
{right
frame e
} \
323 .
menu.lno
{right
frame e
}
327 text .log.t
-bd 2 -height $loglines -background $FG -foreground $BG
329 button .log.b.pl
-text "+" \
330 -command {incr loglines
1; .log.t configure
-height $loglines}
331 button .log.b.mn
-text "-" \
332 -command {incr loglines
-1; .log.t configure
-height $loglines}
333 pack append .log.b .log.b.pl
{top
}
334 pack append .log.b .log.b.mn
{top
}
335 pack append .log .log.b
{left filly
}
336 pack append .log .log.t
{right expand fill
}
340 set from
[.inp.t index insert
]
342 set upto
[.inp.t index insert
]
343 .inp.t tag add sel
$from $upto
344 # .inp.t tag configure hilite -background $FG -foreground $BG
347 #- fetch the value of user-defined configuration options
349 proc fetchOption
{name
default args
} {
354 # class encoded in name ?
355 switch -glob -- $name *.
* {
356 set list [split $name .
]
357 switch [llength $list] 2 {} default { error "wrong option \"$name\" }
358 set class [lindex $list 0]
359 set name [lindex $list 1]
362 # create a unique dummy frame of requested class and get the option's value
364 while {[winfo exists $dummy]} { append dummy 0 }
365 frame $dummy -class $class
366 set value [option get $dummy $name $class]
369 # option not defined ?
370 switch -- $value "" { return $default }
372 # check a restriction on option's value
373 switch [llength $args] {
376 1 { # restriction is given as a list of allowed values
377 switch -- [lsearch -exact [lindex $args 0] $value] -1 {
378 set msg "wrong value
\"$value\" of
option \"$fullName\"\
379 (should be one of
$args)"
380 return -code error -errorinfo $msg $msg
383 2 { # restriction is given as a range (min and max)
384 set min [lindex $args 0]
385 set max [lindex $args 1]
386 if {$value < $min} { set $value $min }
387 if {$value > $max} { set $value $max }
390 error "internal
error in fetchOption
: wrong restriction
\"$args\""
398 set BD [fetchOption borderWidth 1 0 4]
399 #option add *Text.highlightThickness $BD startupFile
402 set scrollbarSide [fetchOption Scrollbar.side right {left right}]
406 scrollbar .inp.s -command ".inp.t yview
"
407 text .inp.t -bd 2 -font $HelvBig -yscrollcommand ".inp.s
set" -wrap word
409 pack .inp.s -side $scrollbarSide -fill y
411 .inp.t {left expand fill}
413 menu .inp.t.edit -tearoff 0
414 .inp.t.edit add command -label "Cut
" \
415 -command {tk_textCopy .inp.t; tk_textCut .inp.t}
416 .inp.t.edit add command -label "Copy
" \
417 -command {tk_textCopy .inp.t}
418 .inp.t.edit add command -label "Paste
" \
421 bind .inp.t <ButtonPress-3> {
422 tk_popup .inp.t.edit %X %Y
424 bind .inp.t <ButtonRelease-1> { setlno }
427 set l_typ 0; # used by both simulator and validator
428 set lt_typ 0; # used by ltl panel
429 set ol_typ -1; # remembers setting last used in compilation
430 set m_typ 2; # used by simulator
433 .menu.file.m add command -label "New
" \
434 -command ".inp.t delete
0.0 end
"
435 # .menu.file.m add command -label "UnSelect
" \
436 # -command ".inp.t tag remove hilite
0.0 end
;\
437 # .inp.t tag remove Rev 0.0 end;\
438 # .inp.t tag remove sel 0.0 end"
439 .
menu.
file.m add command
-label "ReOpen" -command "open_spec"
440 .
menu.
file.m add command
-label "Open.." -command "open_spec 0"
441 .
menu.
file.m add command
-label "Save As.." -command "save_spec 0"
442 .
menu.
file.m add command
-label "Save" -command "save_spec"
443 .
menu.
file.m add command
-label "Quit" \
444 -command "cleanup 1; destroy .; exit"
447 .
menu.help.m add command
-label "About Spin" \
449 .
menu.help.m add separator
450 .
menu.help.m add command
-label "Promela Usage" \
452 .
menu.help.m add command
-label "Xspin Usage" \
454 .
menu.help.m add command
-label "Simulation" \
456 .
menu.help.m add command
-label "Verification" \
458 .
menu.help.m add command
-label "LTL Formulae" \
460 .
menu.help.m add command
-label "Spin Automata View" \
462 .
menu.help.m add command
-label "Reducing Complexity" \
466 .
menu.run.m add command
-label "Run Syntax Check" \
467 -command {syntax_check
"-a -v" "Syntax Check"}
468 .
menu.run.m add command
-label "Run Slicing Algorithm" \
469 -command {syntax_check
"-A" "Property-Specific Slicing"}
470 .
menu.run.m add separator
471 .
menu.run.m add command
-label "Set Simulation Parameters.." \
473 .
menu.run.m add command
-label "(Re)Run Simulation" \
474 -command Rewind
-state disabled
475 .
menu.run.m add separator
476 .
menu.run.m add command
-label "Set Verification Parameters.." \
478 .
menu.run.m add command
-label "(Re)Run Verification" \
479 -command {runval
"0"} -state disabled
480 .
menu.run.m add separator
481 .
menu.run.m add command
-label "LTL Property manager.." \
483 .
menu.run.m add separator
484 .
menu.run.m add command
-label "View Spin Automaton for each Proctype.." \
489 .
menu.edit.m add command
-label "Cut" \
490 -command {tk_textCopy .inp.t
; tk_textCut .inp.t
}
491 .
menu.edit.m add command
-label "Copy" \
492 -command {tk_textCopy .inp.t
}
493 .
menu.edit.m add command
-label "Paste" \
494 -command {tk_textPaste .inp.t
}
499 .
menu.view.m add command
-label "Larger" \
502 set HelvBig
"-Adobe-Helvetica-Medium-R-Normal--*-$FSz-*-*-*-*-*-*"
503 .inp.t configure
-font $HelvBig
505 .
menu.view.m add command
-label "Default text size" \
508 set HelvBig
"-Adobe-Helvetica-Medium-R-Normal--*-$FSz-*-*-*-*-*-*"
509 .inp.t configure
-font $HelvBig
511 .
menu.view.m add command
-label "Smaller" \
514 set HelvBig
"-Adobe-Helvetica-Medium-R-Normal--*-$FSz-*-*-*-*-*-*"
515 .inp.t configure
-font $HelvBig
517 .
menu.view.m add separator
518 .
menu.view.m add command
-label "Clear Selections" \
519 -command ".inp.t tag remove hilite 0.0 end;\
520 .inp.t tag remove Rev 0.0 end;\
521 .inp.t tag remove sel 0.0 end"
524 scan [.inp.t index insert
] "%d.%d" lno cno
525 .
menu.ent delete
0 end
526 .
menu.ent insert end
$lno
527 .inp.t tag remove hilite
$lno.0 $lno.end
;# or else cursor is invis
531 proc add_log
{{y
""}} {
533 if {$y == "\n"} { return }
534 .log.t insert end
"\n$y"
535 .log.t yview
-pickplace end
540 if {$Unix == 0 && $how == 1} {
541 add_log
"removing temporary files, please wait.."; update
543 rmfile
"pan.h pan.c pan.t pan.m pan.b pan.tmp pan.ltl"
544 rmfile
"pan.oin pan.pre pan.out pan.exe pan.otl"
545 rmfile
"pan_in pan_in.trail trail.out pan"
546 rmfile
"_tmp1_ _tmp2_ pan.o pan.obj pan.exe"
547 if {$Unix == 0 && $how == 1} { add_log
"done.." }
552 .log
{bot
frame w fillx
} \
553 .inp
{bot
frame w expand fill
} \
556 # simulation parameters - initial settings
558 set msc
1; set svars
1
560 set stop
0; set tsc
0
561 set seed
"1"; # random sumulation
562 set jumpsteps
"0"; # guided simulation
565 # meaning s_type values:
566 # 0 - Random Simulation (using seed)
567 # 1 - Guided Simulation (using pan.trail)
568 # 2 - Interactive Simulation
571 # meaning of whichsim values:
572 # 0 - use pan_in.tra(il)
573 # 1 - use user specified file
575 tkwait visibility .log
578 add_log
"Xspin Version $xversion"
579 add_log
"TclTk Version [info tclversion]/$tk_version\n"
582 if {[auto_execok $CC0] == "" \
583 ||
[auto_execok $CC0] == 0} {
584 set m
"Error: no C compiler found: $CC"
586 catch { tk_messageBox -icon info -message $m }
589 .inp.t configure
-background $BG -foreground $FG
591 # process execution barchart
600 global Data Name n PlaceBar
601 for {set i
0} {$i <= $n} {incr i
} {
606 set PlaceBar
[wm geometry .bar
]
607 set k
[string first
"\+" $PlaceBar]
609 set PlaceBar
[string range
$PlaceBar $k end
]
611 catch { destroy .bar
}
628 proc stepbar
{v nm
} {
632 if { [info exists Data
($v)] } {
640 if { [string length
$nm] > 4} {
641 set Name
($v) [string range
$nm 0 4]
649 proc adjustbar
{v w
} {
657 global n Data bar_handle Ptype PlaceBar
659 catch { destroy .bar
}
661 wm minsize .bar
200 200
664 set maxy
[expr [winfo screenheight .
] - 200]
665 if {$PlaceBar == ""} {
666 set PlaceBar
"+[expr [winfo rootx .]+150]+$maxy"
668 wm geometry .bar
$PlaceBar
670 set bar_handle
[canvas .bar.c
-height 410 -width 410 -relief raised
]
673 button .bar.buts.s1
-text "Save in: panbar.ps" \
674 -command ".bar.c postscript -file panbar.ps -colormode $Ptype"
676 button .bar.buts.b
-text " Close " -command "stopbar"
677 pack .bar.buts.b .bar.buts.s1
-side right
678 pack append .bar .bar.c
{top expand fill
} .bar.buts
{bot
frame e
}
687 for {set i
0} {$i < $n} {incr i
} {
688 if { [info exists Data
($i)] } {
695 for {set i
0} {$i < $n} {incr i
} {
699 -fill #222222 -tags grid
700 .bar.c create
text $i 105 \
702 .bar.c create
text $i 110 \
704 -fill blue
-tags grid
706 if { [info exists Data
($i)] } {
707 set y
[expr ($Data($i)*100)/$sum]
711 -width 35 -fill red
-tags data
717 .bar.c create
text $i 95 \
719 -fill $nrcol -tags grid
723 .bar.c create
text [expr ($n)/2.0] -15 -text "Percentage of $sum System Steps" \
724 -anchor c
-justify center
-tags grid
725 .bar.c create
text [expr ($n)/2.0] -8 -text "Executed Per Process ($n total)" \
726 -anchor c
-justify center
-tags grid
727 .bar.c
scale all
0 0 55 3
729 .bar.c move all
100 60
731 .bar.c move all
50 60
739 button .bar.buts.b4
-text "Larger" \
740 -command "$bar_handle scale all 0 0 1.1 1.1"
741 button .bar.buts.b5
-text "Smaller" \
742 -command "$bar_handle scale all 0 0 0.9 0.9"
743 pack append .bar.buts
\
744 .bar.buts.b4
{right padx
5} \
745 .bar.buts.b5
{right padx
5}
749 # Files and Generic Boxes
755 global Unix CMD tk_major tk_minor
758 catch { eval file delete
-force $f } err
759 if {$err == "" } { return }
762 catch {exec rm
-f $f}
765 for {set i
0} {$i < $n} {incr i
} {
768 if {$tk_major >= 4 && $tk_minor >= 2} {
769 catch {exec $CMD /c del
$g}
771 catch {exec $CMD >&@stdout
/c del
$g}
777 global Unix CMD tk_major tk_minor
780 catch { file rename -force $f $g } err
781 if {$err == "" } { return }
784 catch {exec mv
$f $g}
786 if {$tk_major >= 4 && $tk_minor >= 2} {
787 catch {exec $CMD /c move
$f $g}
789 catch {exec $CMD >&@stdout
/c move
$f $g}
795 global Unix CMD tk_major tk_minor
798 catch { file copy
-force $f $g } err
799 if {$err == "" } { return }
802 catch {exec cp
$f $g}
804 if {$tk_major >= 4 && $tk_minor >= 2} {
805 catch {exec $CMD /c copy
$f $g}
807 catch {exec $CMD >&@stdout
/c copy
$f $g}
816 catch {exec cmp
$f $g} err
818 if {[file exists
$f] == 0 \
819 ||
[file exists
$g] == 0} {
825 set n1
[gets $fd1 line1
]
826 set n2
[gets $fd2 line2
]
828 ||
[string compare
$line1 $line2] != 0} {
829 set err
"files differ"
832 if {$n1 < 0} { break }
841 if {[file exists
$f]} {
842 if {![file isfile
$f] ||
![file writable
$f]} {
843 set m
"error: file $f is not writable"
845 catch { tk_messageBox -icon info -message $m }
853 set fd
[open pan_in w
]
855 fconfigure $fd -translation lf
856 puts $fd [.inp.t get
0.0 end
] nonewline
858 if {$HasNever != ""} {
859 if [catch {set fdn
[open $HasNever r
]} errmsg
] {
861 catch { tk_messageBox -icon info -message $errmsg }
863 while {[gets $fdn line
] > -1} {
872 proc no_ltlchange
{} {
874 if {![file exists pan.ltl
]} {
877 if {![file exists pan.otl
]} {
878 cpfile pan.ltl pan.otl
879 return 0 ; first
time
881 set err
[cmpfile pan.ltl pan.otl
]
882 if {[string length
$err] > 0} {
883 cpfile pan.ltl pan.otl
884 return 0 ;# different
886 return 1 ;# unchanged
892 mkpan_in
;# keep this up to date
893 if {![file exists pan.oin
]} {
894 cpfile pan_in pan.oin
895 return 0 ; first
time
897 set err
[cmpfile pan_in pan.oin
]
898 if {[string length
$err] > 0} {
899 cpfile pan_in pan.oin
900 return 0 ;# different
905 return [no_ltlchange
] ;# unchanged
909 global Unix CC SPIN notignored
911 set nochange
[no_change
]
912 if {$nochange == 1 && [file exists
"pan"]} {
913 add_log
"<no recompilation needed>"
917 add_log
"<compiling executable>"
919 warner
"Compiling" "Please wait until compilation of the \
920 executable produced by spin completes." 300
922 add_log
"$SPIN -a pan_in"
924 catch {exec $SPIN -a pan_in
>&pan.tmp
}
925 set errmsg
[msg_file pan.tmp
1]
927 if {[string length
$errmsg]>0} {
929 catch { tk_messageBox -icon info -message $errmsg }
930 add_log
"<stopped compilation attempt>"
931 catch { destroy .warn
}
935 add_log
"$CC -o pan -D_POSIX_SOURCE pan.c"; update
937 catch { eval exec $CC -o pan
-D_POSIX_SOURCE pan.c
>pan.tmp
2>pan.err
} errmsg
939 catch { eval exec $CC -o pan
-D_POSIX_SOURCE pan.c
>pan.tmp
2>pan.err
}
941 set errmsg
[msg_file pan.tmp
0]
942 set errmsg
"$errmsg \n [msg_file pan.err 0]"
944 if {[string length
$errmsg]>0 && $notignored} {
946 catch { tk_messageBox -icon info -message $errmsg }
947 catch { destroy .warn
}
950 add_log
"<compilation complete>"
951 catch {destroy .warn
}
955 set PlaceWarn
"+20+20"
957 proc warner
{banner msg w
} {
960 catch {destroy .warn
}
963 wm title .warn
"$banner"
964 wm iconname .warn
"Info"
965 set k
[string first
"\+" $PlaceWarn]
967 set PlaceWarn
[string range
$PlaceWarn $k end
]
969 wm geometry .warn
$PlaceWarn
971 message .warn.t
-width $w -text $msg
972 button .warn.ok
-text "Ok" \
973 -command "set PlaceWarn [wm geometry .warn]; destroy .warn"
975 pack append .warn .warn.t
{top expand fill
}
976 pack append .warn .warn.ok
{bottom
}
982 global Fname xversion
984 if {[file_ok
$Fname]==0} return
985 set fd
[open $Fname w
]
986 add_log
"<saved spec in $Fname>"
987 puts $fd "[.inp.t get 0.0 end]" nonewline
990 wm title .
"SPIN CONTROL $xversion -- File: $Fname"
993 proc save_spec
{{curr
1}} {
995 #- Save the input area into a file.
997 #- If 'curr' is true then we save to the current file. Otherwise, a file
998 #- selection dialog is presented. If a file is selected (note that the
999 #- dialog can be canceled) then we try to write to it.
1005 switch -- $Fname "" {
1006 add_log
"no file to save to, try \"Save as ...\""
1009 writeoutfile .inp.t
$Fname
1011 # try to use the predefined file selection dialog
1012 switch [info commands
tk_getSaveFile] "" {
1013 # some old version of Tk so use our own file selection dialog
1014 set fileselect
"FileSelect save"
1016 set fileselect
"tk_getSaveFile"
1019 # get the file (return if the file selection dialog canceled)
1020 switch -- [set file [eval $fileselect]] "" return
1022 # write the file and update Fname if the file written successfully
1023 if [writeoutfile .inp.t
$file] {
1029 proc consider_it
{} {
1030 global file Fname xversion
1032 if {[file isdirectory
$file]} then
{
1037 if {![file isfile
$file]} {
1040 readinfile .inp.t
$file
1043 cpfile
$file.trail pan_in.trail
1047 wm title .
"SPIN CONTROL $xversion -- File: $Fname"
1052 #----------------------------------------------------------------------
1053 # Improvements - by Leszek Holenderski <lhol@win.tue.nl>
1054 # GUI configuration and File Selection dialogs
1055 #----------------------------------------------------------------------
1057 # predefined priorities for options stored in the option data base are
1063 # most of frames are used for layout purposes so they should be invisible
1064 option add
*Frame.borderWidth
0 interactive
1066 proc try_with
{xspinrc
} {
1068 if ![file exists
$xspinrc] return
1070 if ![file isfile
$xspinrc] {
1071 puts "xspin warning: the resource file \"$xspinrc\" exists but is not\
1075 if ![file readable
$xspinrc] {
1076 puts "xspin warning: the resource file \"$xspinrc\" exists but is not\
1080 if [catch {option readfile
$xspinrc userDefault
} result
] {
1081 puts "xspin warning: some problems when trying to load the resource\
1082 file \"$xspinrc\"\n$result"
1087 if [info exists env
(HOME
)] {
1089 try_with
[file join $env(HOME
) .xspinrc
]
1091 try_with
[file join $env(HOME
) xspinrc
]
1095 proc FileSelect
{mode
{title
""}} {
1096 switch -- $mode open - save
{} default { set mode
open }
1101 set okButtonText Open
1105 set okButtonText Save
1112 if [winfo exists
$w] {
1114 $this(okButton
) config
-text $okButtonText
1115 catch {wm geom
$w $this(geom
)}
1118 toplevel $w -class Fileselect
1120 # the minimal size is given in characters and lines (setgrid is on)
1124 pack [set f
[frame $w.f
]] -padx 5 -pady 5 -fill both
-expand yes
1125 pack [set buttons
[frame $f.b
]] -side bottom
-fill x
1126 pack [set name
[frame $f.n
]] -side bottom
-fill x
-pady 5
1127 pack [set path
[frame $f.p
]] -side top
-fill x
1128 pack [set files
[frame $f.f
]] -side top
-fill both
-expand yes
1130 # create ok/cancel buttons
1131 set okButton
[button $buttons.ok
-text $okButtonText \
1132 -command "FileSelect.Close $w 1"]
1133 pack $okButton -side right
1135 set cancelButton
[button $buttons.cancel
-text Cancel
\
1136 -command "FileSelect.Close $w 0"]
1137 pack $cancelButton -side left
1139 MakeSameWidth
"$okButton $cancelButton"
1141 # create path button
1142 set pathButton
$path.path
1144 set pathMenu
[tk_optionMenu $pathButton $w|currDir
""]
1145 pack $pathButton -side top
1147 # create the list of files
1148 global scrollbarSide
1150 set fileList
$files.l
1151 set scrollbar $files.s
1152 pack [scrollbar $files.s
-command "$fileList yview"] \
1153 -side $scrollbarSide -fill y
1154 pack [listbox $fileList -yscrollcommand "$files.s set" -selectmode single
-setgrid on
] \
1155 -side $scrollbarSide -expand yes
-fill both
1157 bind $fileList <ButtonPress-1
> "FileSelect.Selected $w %x %y"
1158 bind $fileList <Double-ButtonPress-1
> "FileSelect.Chosen $w %x %y"
1160 set fileEntry
$name.e
1161 pack [label $name.l
-text File
:] -side left
1162 pack [entry $fileEntry] -side right
-expand yes
-fill x
1164 set this
(okButton
) $okButton
1165 set this
(pathButton
) $pathButton
1166 set this
(pathMenu
) $pathMenu
1167 set this
(fileList
) $fileList
1168 set this
(fileEntry
) $fileEntry
1170 foreach widget
"$okButton $cancelButton $pathButton $fileList $scrollbar" {
1171 $widget config
-highlightthickness 0
1174 wm protocol
$w WM_DELETE_WINDOW
[$cancelButton cget
-command]
1177 # fill in the list of files
1178 if ![info exists this
(path
)] { set this
(path
) [pwd] }
1179 FileSelect.
cd $w $this(path
)
1181 # make the dialog modal (set a grab and claim the focus)
1183 set oldFocus
[focus]
1184 set oldGrab
[grab current
$w]
1185 if {$oldGrab != ""} { set grabStatus
[grab status
$oldGrab] }
1187 focus $this(fileEntry
)
1189 # make the contents of file entry selected (for easy deletion)
1190 $this(fileEntry
) select from
0
1191 $this(fileEntry
) select to end
1193 # Wait for the user to respond, then restore the focus and return the
1194 # contents of file entry.
1195 # Restore the focus before deleting the window, since otherwise the
1196 # window manager may take the focus away so we can't redirect it.
1197 # Finally, restore any grab that was in effect.
1200 tkwait variable $w|response
1201 catch {focus $oldFocus}
1203 set this
(geom
) [wm geom
$w]
1205 if {$oldGrab != ""} {
1206 if {$grabStatus == "global"} {
1207 grab -global $oldGrab
1212 return [set $w|response
]
1215 proc CompareNoCase
{s1 s2
} {
1216 return [string compare
[string tolower
$s1] [string tolower
$s2]]
1219 proc FileSelect.LoadFiles
{w
} {
1222 # split all names in the current directory into dirs and files
1226 if [info exists this
(filter
)] { set filter
$this(filter
) }
1227 switch -- $filter "" { set filter
* }
1228 foreach f
[lsort -command CompareNoCase
[glob -nocomplain .
* *]] {
1229 if [file isdir
$f] {
1230 # exclude the '.' and '..' directory
1231 switch -- $f .
- ..
continue
1234 if [file isfile
$f] {
1236 switch -glob -- $f $filter { lappend files
$f }
1240 # Fill in the file list
1241 $this(fileList
) delete
0 end
1243 # append directory mark to the name (tricky)
1244 set d
[string trimright
[file join $d a
] a
]
1245 $this(fileList
) insert end
$d
1247 foreach f
$files { $this(fileList
) insert end
$f }
1250 proc FileSelect.LoadPath
{w
} {
1253 # convert path to list
1254 set dirs
[file split $this(path
)]
1256 # compute prefix paths
1260 set path
[file join $path $d]
1264 # reverse dirs and paths
1266 foreach d
$dirs { set rev_dirs
[concat [list $d] $rev_dirs] }
1268 foreach p
$paths { set rev_paths
[concat [list $p] $rev_paths] }
1270 # update the path menubutton
1272 set $w|currDir
[lindex $rev_dirs 0]
1274 # fill in the path menu
1275 $this(pathMenu
) delete
0 end
1276 foreach d
[lrange $rev_dirs 1 end
] p
[lrange $rev_paths 1 end
] {
1277 $this(pathMenu
) add command
-label $d -command "FileSelect.cd $w $p"
1281 proc FileSelect.Selected
{w x y
} {
1284 # determine the selected list element
1285 set elem
[$this(fileList
) get
[$this(fileList
) index
@$x,$y]]
1286 switch -- $elem "" return
1288 # directories cannot be selected (they can only be chosen)
1289 if [file isdir
$elem] return
1291 $this(fileEntry
) delete
0 end
1292 $this(fileEntry
) insert end
$elem
1295 proc FileSelect.Chosen
{w x y
} {
1298 # determine the selected list element
1299 set elem
[$this(fileList
) get
[$this(fileList
) index
@$x,$y]]
1300 switch -- $elem "" return
1302 # if directory then cd, otherwise close the dialog
1303 if [file isdir
$elem] { FileSelect.
cd $w $elem } { FileSelect.Close
$w 1 }
1306 proc FileSelect.Close
{w
{ok
1}} {
1307 # trigger the end of dialog
1308 upvar #0 $w this $w|response response
1310 set response
[file join $this(path
) [$this(fileEntry
) get
]]
1316 proc FileSelect.
cd {w dir
} {
1319 if [catch {cd $dir} errmsg
] {
1320 puts "xspin warning: $errmsg"
1324 set this
(path
) [pwd]
1325 FileSelect.LoadFiles
$w
1326 FileSelect.LoadPath
$w
1329 proc open_spec
{{curr
1}} {
1333 switch -- $Fname "" {
1334 add_log
"no file to reopen, try \"Open ...\""
1337 readinfile .inp.t
$Fname
1339 # try to use the predefined file selection dialog
1340 switch [info commands
tk_getOpenFile] "" {
1341 # some old version of Tk so use our own file selection dialog
1342 set fileselect
"FileSelect open"
1344 set fileselect
"tk_getOpenFile"
1347 # get the file (return if the file selection dialog canceled)
1348 switch -- [set file [eval $fileselect -initialdir { $init_dir } ]] "" return
1350 # load the file and update some items if the file loaded successfully
1351 if [readinfile .inp.t
$file] {
1353 cpfile
$file.trail pan_in.trail
1361 proc set_path
{Fname
} {
1362 #cd to directory in file
1363 set fullpath
[split $Fname /]
1364 set nlen
[llength $fullpath]
1365 set fullpath
[lrange $fullpath 0 [expr $nlen - 2]] ;# get rid of filename
1366 set wd
[join $fullpath /] ;#put path back together
1372 proc loaddefault_tl
{} {
1373 global Fname defname
1375 if {$defname ==""} {
1376 set file2
"$Fname.ltl"
1381 .tl.main.e1 delete
0 end
1382 .tl.macros.t delete
0.0 end
1383 .tl.notes.t delete
0.0 end
1384 .tl.never.t delete
0.0 end
1385 .tl.results.t delete
0.0 end
1387 if {![file exists
$file2]} {
1388 .tl.notes.t insert end
"Use Load to open a file or a template."
1392 .tl.notes.title configure
-text "Notes \[file $file2]:"
1394 readinfile .tl.never.t
$file2
1395 catch { extract_defs
}
1401 global defname suffix
1407 wm iconname .b
"Load"
1411 scrollbar .b.top.scroll
-command ".b.top.list yview"
1412 listbox .b.top.
list -yscroll ".b.top.scroll set" -relief raised
1414 button .b.zap
-text "Cancel" -command "destroy .b"
1415 button .b.all
-text "Show All Files" \
1421 message .b.bot.msg
-text "Dir: "
1422 entry .b.bot.
entry -textvariable dir
-relief sunken
-width 20
1423 pack append .b.top
\
1424 .b.top.scroll
{right filly
} \
1425 .b.top.
list {left expand fill
}
1426 pack append .b.bot
\
1430 .b.top
{top fillx
} \
1435 bind .b.bot.
entry <Return
> {
1436 set nd
[.b.bot.
entry get
]
1437 if {[file isdirectory
$nd]} {
1445 bind .b.top.
list <Double-Button-1
> {
1446 set file2
[selection get
]
1447 if {[string first
"---" $file2] >= 0} {
1449 } elseif
{[string first
"Invariance" $file2] >= 0} {
1451 .tl.main.e1 delete
0 end
1452 .tl.macros.t delete
0.0 end
1453 .tl.notes.t delete
0.0 end
1454 .tl.never.t delete
0.0 end
1455 .tl.results.t delete
0.0 end
1457 .tl.main.e1 insert end
"\[\] (p)"
1458 .tl.notes.t insert end
"'p' is invariantly true throughout
1460 .tl.notes.title configure
\
1461 -text "Notes \[template $file2]:"
1465 } elseif
{[string first
"Response" $file2] >= 0} {
1467 .tl.main.e1 delete
0 end
1468 .tl.macros.t delete
0.0 end
1469 .tl.notes.t delete
0.0 end
1470 .tl.never.t delete
0.0 end
1471 .tl.results.t delete
0.0 end
1473 .tl.main.e1 insert end
"\[\] ((p) -> (<> (q)))"
1474 .tl.notes.t insert end
"if 'p' is true in at least one state,
1475 then sometime thereafter 'q' must also
1476 become true at least once."
1477 .tl.notes.title configure
\
1478 -text "Notes \[template $file2]:"
1482 } elseif
{[string first
"Precedence" $file2] >= 0} {
1484 .tl.main.e1 delete
0 end
1485 .tl.macros.t delete
0.0 end
1486 .tl.notes.t delete
0.0 end
1487 .tl.never.t delete
0.0 end
1488 .tl.results.t delete
0.0 end
1490 .tl.main.e1 insert end
"\[\] ((p) -> ((q) U (r)))"
1491 .tl.notes.t insert end
"'p' is a trigger, or 'enabling' condition that
1492 determines when this requirement becomes applicable
1493 'r' is the fullfillment of the requirement, and
1494 'q' is a condition that must remain true in the interim."
1495 .tl.notes.title configure
\
1496 -text "Notes \[template $file2]:"
1500 } elseif
{[string first
"Objective" $file2] >= 0} {
1502 .tl.main.e1 delete
0 end
1503 .tl.macros.t delete
0.0 end
1504 .tl.notes.t delete
0.0 end
1505 .tl.never.t delete
0.0 end
1506 .tl.results.t delete
0.0 end
1508 .tl.main.e1 insert end
"\[\] ((p) -> <>((q) || (r)))"
1509 .tl.notes.t insert end
"'p' is a trigger, or 'enabling' condition that
1510 determines when this requirement becomes applicable
1511 'q' is the fullfillment of the requirement, and
1512 'r' is a discharging condition that terminates the
1513 applicability of the requirement."
1515 .tl.notes.title configure
\
1516 -text "Notes \[template $file2]:"
1520 } elseif
{[file isdirectory
$file2]} then
{
1525 if {![file isfile
$file2]} {
1529 .tl.main.e1 delete
0 end
1530 .tl.macros.t delete
0.0 end
1531 .tl.notes.t delete
0.0 end
1532 .tl.never.t delete
0.0 end
1533 .tl.results.t delete
0.0 end
1534 .tl.notes.title configure
\
1535 -text "Notes \[file $file2]:"
1537 readinfile .tl.never.t
$file2
1539 catch { extract_defs
}
1550 catch {readinfile .inp.t
$Fname} ermsg
1551 if {[string length
$ermsg]<=1} { return }
1553 catch { tk_messageBox -icon info -message $ermsg }
1556 proc check_xsp
{f
} {
1558 if [catch {set fd
[open $ff r
]} errmsg
] {
1559 # add_log "no file $ff"
1562 add_log
"reading $ff file"
1564 while {[gets $fd line
] > -1} {
1565 if {[string first
"X:" $line] == 0} {
1566 set C
[string range
$line 3 end
]
1569 catch { eval exec $C } errmsg
1570 if {$errmsg != ""} { add_log
$errmsg }
1572 if {[string first
"L:" $line] == 0} {
1573 set N
[string range
$line 3 end
]
1574 catch {.log.t configure
-height $N -bg black
-fg gold
}
1579 proc writeoutfile
{from to
} {
1581 if ![file_ok
$to] { return 0 }
1583 if [catch {set fd
[open $to w
]} errmsg
] {
1585 catch { tk_messageBox -icon info -message $ermsg }
1589 add_log
"<saved spec in $to>"
1590 puts $fd [string trimright
[$from get
0.0 end
] "\n"]
1591 # puts -nonewline $fd [$from get 0.0 end]
1596 proc readinfile
{into from
} {
1598 if [catch {set fd
[open $from r
]} errmsg
] {
1600 catch { tk_messageBox -icon info -message $ermsg }
1604 $into delete
0.0 end
1605 while {[gets $fd line
] > -1} { $into insert end
$line\n }
1607 add_log
"<open $from>"
1610 set LastGenerate
"" ;# used in Validation.tcl
1614 proc fillerup
{suffix
} {
1616 .b.top.
list delete
0 end
1620 catch { if {$suffix != ""} {
1621 set l
[lsort [glob *.
$suffix]]
1623 set l
[lsort [glob *]]
1626 .b.top.
list insert end
$i
1627 if {$i == ".."} { set dotdot
1 }
1630 .b.top.
list insert
0 ".."
1632 if {$suffix != ""} {
1633 .b.top.
list insert
0 "------files:--------"
1634 .b.top.
list insert
0 "Objective(p,q,r)"
1635 .b.top.
list insert
0 "Precedence(p,q,r)"
1636 .b.top.
list insert
0 "Response(p,q)"
1637 .b.top.
list insert
0 "Invariance(p)"
1638 .b.top.
list insert
0 "-----templates:-----"
1645 catch { destroy .ln
}
1647 wm title .ln
"Goto Line"
1648 wm iconname .ln
"Goto"
1650 label .ln.lab
-text "Enter line number:"
1651 entry .ln.ent
-width 20 -relief sunken
-textvariable lno
1653 .ln.lab
{left padx
1m
} \
1654 .ln.ent
{right expand
}
1655 bind .ln.ent
<Return
> {
1656 .inp.t tag remove hilite
0.0 end
1657 .inp.t tag add hilite
$lno.0 $lno.1000
1658 .inp.t tag configure hilite
\
1659 -background $FG -foreground $BG
1660 .inp.t yview
-pickplace [expr $lno-1]
1666 set fname
[.c
$b.f.e1 get
]
1667 if {[file_ok
$fname]==0} return
1668 set fd
[open $fname w
]
1669 add_log
"<saved output in $fname>"
1670 puts $fd "[.c$b.z.t get 0.0 end]" nonewline
1675 proc doplace
{a b
} {
1677 set PlaceBox
($a) [wm geometry .c
$b]
1678 set k
[string first
"\+" $PlaceBox($a)]
1680 set PlaceBox
($a) [string range
$PlaceBox($a) $k end
]
1684 proc mkbox
{n m p
{wd
60} {ht
10} {xp
200} {yp
200}} {
1685 global boxnr FG BG PlaceBox HelvBig
1686 global ind old_ss old_insert new_insert
;# for search capability
1691 wm title .c
$boxnr $n
1692 wm iconname .c
$boxnr $m
1694 if {[info exists PlaceBox
($n)] == 0} {
1695 set PlaceBox
($n) "+$xp+$yp"
1697 wm geometry .c
$boxnr $PlaceBox($n)
1699 #initialize search parameters
1704 frame .c
$boxnr.d
;# search bar
1705 label .c
$boxnr.d.l
-text "Search for: "
1706 entry .c
$boxnr.d.e
-width 15
1707 bind .c
$boxnr.d.e
<KeyPress-Return
> "search_sim .c$boxnr.z.t .c$boxnr.d.e .c$boxnr"
1708 button .c
$boxnr.d.b
-text "Find" -command "search_sim .c$boxnr.z.t .c$boxnr.d.e .c$boxnr"
1710 pack .c
$boxnr.d
-side top
-fill x
1711 pack .c
$boxnr.d.b
-side right
1712 pack .c
$boxnr.d.e
-side right
1713 pack .c
$boxnr.d.l
-side right
1717 text .c
$boxnr.z.t
-relief raised
-bd 2 -font $HelvBig \
1718 -background $BG -foreground $FG \
1719 -yscrollcommand ".c$boxnr.z.s set" \
1720 -setgrid 1 -width $wd -height $ht -wrap word
1721 bind .c
$boxnr.z.t
<ButtonRelease-1
> "+update idletasks; update_insert .c$boxnr.z.t"
1722 scrollbar .c
$boxnr.z.s
\
1723 -command ".c$boxnr.z.t yview"
1724 pack append .c
$boxnr.z
\
1725 .c
$boxnr.z.s
{left filly
} \
1726 .c
$boxnr.z.t
{left expand fill
}
1728 button .c
$boxnr.b
-text "Close" \
1729 -command "doplace {$n} {$boxnr}; destroy .c$boxnr"
1730 button .c
$boxnr.c
-text "Clear" \
1731 -command ".c$boxnr.z.t delete 0.0 end"
1732 pack append .c
$boxnr \
1733 .c
$boxnr.z
{top expand fill
} \
1734 .c
$boxnr.b
{right padx
5} \
1735 .c
$boxnr.c
{right padx
5}
1737 if {[string length
$p]>0} {
1738 frame .c
$boxnr.f
-relief sunken
1739 button .c
$boxnr.f.e0
-text "Save in: " \
1740 -command "savebox $boxnr"
1741 entry .c
$boxnr.f.e1
-relief flat
-width 10
1742 .c
$boxnr.f.e1 insert end
$p
1743 pack append .c
$boxnr.f
\
1744 .c
$boxnr.f.e0
{left padx
5} \
1745 .c
$boxnr.f.e1
{left
}
1746 pack append .c
$boxnr \
1747 .c
$boxnr.f
{right padx
5}
1750 tkwait visibility .c
$boxnr
1754 proc update_insert
{t
} {
1757 set new_insert
[$t index insert
]
1760 proc search_sim
{t e b
} {
1761 global ind old_ss old_insert new_insert
1769 #if user has selected use that lin.char as 'ind'. otherwise use end of last word found
1770 #set new_insert [$t index insert]
1771 if {$new_insert != $old_insert} {
1772 set ind
$new_insert ;# this is where we will start searching
1773 set old_insert
$new_insert ;# update select location
1776 set ind
[$t search
$ss $ind]
1780 $t yview
-pickplace $ind
1781 $t tag configure hilite
-foreground black
-background white
1782 $t tag delete hilite
1783 set split_ind
[split $ind "."]
1784 set char
[lindex $split_ind 1]
1785 set char
[incr char
[string length
$ss]]
1788 append indend
[lindex $split_ind 0] "." $char
1789 $t tag add hilite
$indstart $indend
1790 $t tag configure hilite
-foreground white
-background black
1794 catch { tk_messageBox -icon info -message "no match for $ss" }
1795 set ind
$cur_ind ;# restore ind to last good value
1801 # Tcl/Tk book, page 219
1802 proc forAllMatches
{w pattern
} {
1805 scan [$w index end
] %d numLines
1806 for {set i
1} {$i < $numLines} { incr i
} {
1807 $w mark
set last
$i.0
1808 if {[regexp -indices $pattern \
1809 [$w get last
"last lineend"] indices
]} {
1811 "last + [lindex $indices 0] chars"
1812 $w mark
set last
"last + 1 chars \
1813 + [lindex $indices 1] chars"
1814 .inp.t tag add hilite
$i.0 $i.end
1815 .inp.t tag configure hilite
\
1816 -background $FG -foreground $BG
1817 # .inp.t yview -pickplace [expr $i-1]
1820 # move to the next line that matches
1822 for {set i
[expr $lno+1]} {$i < $numLines} { incr i
} {
1823 $w mark
set last
$i.0
1824 if {[regexp -indices $pattern \
1825 [$w get last
"last lineend"] indices
]} {
1827 "last + [lindex $indices 0] chars"
1828 $w mark
set last
"last + 1 chars \
1829 + [lindex $indices 1] chars"
1830 .inp.t yview
-pickplace [expr $i-5]
1834 for {set i
1} {$i <= $lno} { incr i
} {
1835 $w mark
set last
$i.0
1836 if {[regexp -indices $pattern \
1837 [$w get last
"last lineend"] indices
]} {
1839 "last + [lindex $indices 0] chars"
1840 $w mark
set last
"last + 1 chars \
1841 + [lindex $indices 1] chars"
1842 .inp.t yview
-pickplace [expr $i-5]
1847 tk_messageBox -icon info -message "No Match of \"$pattern\""
1853 proc hasWord
{pattern
} {
1856 if {![file exists pan.pre
] && $noprep == 0} {
1857 add_log
"$SPIN -Z pan_in ;# preprocess input $pattern"
1858 catch {exec $SPIN -Z pan_in
>&pan.tmp
} err
1859 # leaves output in pan.pre
1860 add_log
"<done preprocess>"
1863 if {[string length
$err] == 0 && $noprep == 0} {
1864 set fd
[open pan.pre r
]
1865 while {[gets $fd line
] > -1} {
1866 if {[regexp -indices $pattern $line indices
]} {
1874 # else, there were errors, just ignore the include files:
1877 scan [.inp.t index end
] %d numLines
1878 for {set i
1} {$i < $numLines} { incr i
} {
1879 .inp.t mark
set last
$i.0
1880 if {[regexp -indices $pattern \
1881 [.inp.t get last
"last lineend"] indices
]} {
1915 add_log
"<fsm view option>"
1917 if {[mk_exec
] != 1} { return }
1922 wm title .z
"Double-Click Proc"
1924 listbox .z.
list -setgrid 1
1925 button .z.b
-text "Cancel" -command "destroy .z"
1928 .z.
list {top expand fill
} \
1932 add_log
"./pan -d # find proc names"; update
1933 set fd
[open "|./pan -d" w
+]
1935 add_log
"pan -d # find proc names"; update
1936 catch { eval exec pan
-d >&pan.tmp
} err
1938 add_log
"error: $err"
1940 set fd
[open pan.tmp r
]
1942 while {[gets $fd line
] > -1} {
1943 if {[string first
"proctype" $line] >= 0 } {
1944 .z.
list insert end
\
1945 [string trim
[string range
$line 9 end
]]
1949 bind .z.
list <Double-Button-1
> {
1950 set pfind
[selection get
]
1951 catch { destroy .z
}
1957 proc findfsm
{pfind
} {
1958 global Unix New Dist State Edges Label
1959 global Transit MaxDist reached_end TLabel DOT
1961 if {[mk_exec
] != 1} { return }
1963 set src
0; set trn
0; set trg
0
1964 set Want
0; set MaxDist
0; set startstate
""
1966 catch { foreach el
[array names State
] { unset State
($el) } }
1967 catch { foreach el
[array names Edges
] { unset Edges
($el) } }
1968 catch { foreach el
[array names Dist
] { unset Dist
($el) } }
1971 add_log
"./pan -d # compute fsm"; update
1972 set fd
[open "|./pan -d" w
+]
1974 add_log
"pan -d # compute fsm"; update
1975 catch { eval exec pan
-d >&pan.tmp
}
1976 set fd
[open pan.tmp r
]
1978 while {[gets $fd line
] > -1} {
1979 set k
[string first
"proctype" $line]
1985 set pname
[string range
$line $k end
]
1987 if { [string first
$pfind $line] >= 0 \
1988 && [string length
$pfind] == [string length
$pname]} {
1993 set Label
($nsrc) "end"
1996 } elseif
{ $Want == 1 \
1997 && [string first
"statement" $line] < 0
1998 && [string first
"state" $line] >= 0} {
1999 scan $line " state %d -(tr %d)-> state %d" \
2001 if {$trg == 0} { set reached_end
1 }
2003 set nsrc
"$pname:$src"
2004 set ntrg
"$pname:$trg"
2006 if {$startstate == ""} { set startstate
$nsrc }
2008 set k
[string first
"line" $line]
2010 set m
[string first
"=>" $line]
2012 set lbl
[string range
$line $k $m]
2014 set action
[string range
$line $m end
]
2019 set Label
($nsrc) $lbl
2020 if { [info exists Dist
($nsrc)] == 0 } {
2024 if { [info exists Dist
($ntrg)] == 0 } {
2025 set Dist
($ntrg) [expr $Dist($nsrc) + 1]
2027 if {$Dist($ntrg) > $MaxDist } {
2028 set MaxDist
$Dist($ntrg)
2031 if { [expr $Dist($nsrc) + 1] < $Dist($ntrg) } {
2032 set Dist
($ntrg) [expr $Dist($nsrc) + 1]
2033 if {$Dist($ntrg) > $MaxDist } {
2034 set MaxDist
$Dist($ntrg)
2038 && [auto_execok $DOT] != 0 \
2039 && [auto_execok $DOT] != ""} {
2040 set z1
[string first
"\[" $action]
2041 set z2
[string last
"\]" $action]
2042 if {$z1 > 0 && $z2 > $z1} {
2044 set a1
[string range
$action 0 $z1]
2045 set a2
[string range
$action $z2 end
]
2048 set kkk
"$nsrc;$trg:$action"
2049 lappend Edges
($nsrc) "$kkk"
2050 lappend Edges
($kkk) $ntrg
2051 lappend Transit
($nsrc) "$lbl"
2052 lappend Transit
($kkk) ""
2053 set Dist
($kkk) $Dist($ntrg)
2054 set Label
($kkk) "T3"
2056 lappend Edges
($nsrc) $ntrg
2057 lappend Transit
($nsrc) $action
2062 dograph
$pfind $startstate
2064 add_log
"sorry, $pfind not found..."
2066 tk_messageBox -icon info -message "$pfind not found..."
2074 proc plunknode
{el prefix
} {
2075 global State Label TLabel
2078 set pn
[string range
$el $prefix end
]
2079 set State
($el) [mkNode
"$Label($el)" $pn $x $y]
2082 set x
[expr $x - 250]
2083 set x
[expr 250 - $x]
2085 set x
[expr 250 - $x]
2087 set x
[expr 250 + $x]
2091 proc dograph
{n s
} {
2092 global Dist Edges Label Transit MaxDist State ELabel
2093 global cnr lcnr reached_end x y Unix DOT
2096 set lcnr
[mkcanvas
"FSM $n" $n 300 300 0]
2097 set prefix
[string length
$n]
2101 while {$count < $MaxDist} {
2105 foreach el
[array names Dist
] {
2106 if { [ string first
$n $el ] >= 0 \
2107 && $Dist($el) == $count \
2108 && $el != "$n:0" } {
2109 plunknode
$el $prefix
2112 if {$reached_end == 1} {
2113 # force end state at the bottom
2116 plunknode
"$n:0" $prefix
2119 foreach el
[array names Edges
] {
2120 if { [ string first
$n $el ] >= 0 } {
2121 for {set i
0} { [lindex $Edges($el) $i] != "" } {incr i
} {
2122 set ntrg
[lindex $Edges($el) $i]
2123 set lbl
[lindex $Transit($el) $i]
2124 mkEdge
$lbl $State($el) $State($ntrg)
2125 set ELabel
($el,$ntrg) "$lbl"
2130 .f
$cnr.c itemconfigure
$State($s) -outline red
; update
2132 if {[auto_execok $DOT] != 0 \
2133 && [auto_execok $DOT] != ""} {
2135 # button .f$lcnr.b66 -text "Redraw with Dot" -command "dodot $n"
2136 # pack append .f$lcnr .f$lcnr.b66 {right padx 5}
2141 proc mkNode
{n t x y
} {
2143 global cnr NodeWidth NodeHeight HelvBig
2144 global nodeX nodeY New TLabel Lab2Node
2146 if {[string first
";" $t] > 0} {
2147 set New
[.f
$cnr.c create rectangle
[expr $x-1] [expr $y-1] \
2148 [expr $x+1] [expr $y+1] \
2152 set z
[string first
":" $t]; incr z
2153 set t
[string range
$t $z end
]
2154 set Lab
[.f
$cnr.c create
text $x $y -font $HelvBig -text $n -tags node
]
2156 set New
[.f
$cnr.c create oval
[expr $x-10] [expr $y-10] \
2157 [expr $x+10] [expr $y+10] \
2161 set Lab
[.f
$cnr.c create
text $x $y -font $HelvBig -text $n -tags node
]
2163 .f
$cnr.c
bind $Lab <Any-Enter
> "
2164 .f$cnr.c itemconfigure {$Lab} -fill black -text {$t}
2165 if {[string first \"end\" $n] < 0 } { set_src {$t} }
2167 .f
$cnr.c
bind $Lab <Any-Leave
> "
2168 .f$cnr.c itemconfigure {$Lab} -fill black -text {$n}
2173 set TLabel
($New) $Lab
2174 set Lab2Node
($Lab) $New
2175 set NodeWidth
($New) 10
2176 set NodeHeight
($New) 10
2184 scan $n "line %d" where
2185 .inp.t tag remove hilite
0.0 end
2189 proc mkEdge
{L a b
} {
2190 global cnr Xrem Yrem TransLabel HelvBig
2191 global nodeX nodeY edgeHead edgeTail
2193 if { $nodeY($b) > $nodeY($a) } {
2195 } elseif
{ $nodeY($b) < $nodeY($a) } {
2200 if { $nodeX($b) > $nodeX($a) } {
2202 } elseif
{ $nodeX($b) < $nodeX($a) } {
2207 set edge
[.f
$cnr.c create line
\
2208 $nodeX($a) $nodeY($a) \
2209 [expr $nodeX($b) + $xdiff] \
2210 [expr $nodeY($b) + $ydiff] \
2211 -arrow both
-arrowshape {4 3 3} ]
2212 .f
$cnr.c
lower $edge
2213 lappend edgeHead
($a) $edge
2214 lappend edgeTail
($b) $edge
2216 set Xrem
($edge) $xdiff
2217 set Yrem
($edge) $ydiff
2219 set midX
[expr $nodeX($a) + $nodeX($b)]
2220 set midX
[expr $midX / 2 ]
2221 set midY
[expr $nodeY($a) + $nodeY($b)]
2222 set midY
[expr $midY / 2 ]
2224 set TransLabel
($a,$b) \
2225 [.f
$cnr.c create
text $midX $midY -font $HelvBig -tags texttag
]
2227 .f
$cnr.c
bind $edge <Button-1
> "
2228 .f$cnr.c coords $TransLabel($a,$b) \[.f$cnr.c canvasx %x\] \[.f$cnr.c canvasy %y\]
2229 .f$cnr.c itemconfigure $TransLabel($a,$b) \
2230 -fill black -text {$L} -font $HelvBig
2232 .f
$cnr.c
bind $edge <ButtonRelease-1
> "
2233 .f$cnr.c itemconfigure $TransLabel($a,$b) \
2234 -fill black -text {}
2238 proc moveNode
{cnr node mx my together
} {
2239 global edgeHead edgeTail TLabel NodeWidth NodeHeight
2240 global nodeX nodeY Lab2Node
2241 global Xrem Yrem Scale
2243 set x
[.f
$cnr.c coords
$node]
2244 if {[llength $x] == 2} { set node
$Lab2Node($node) }
2246 set mx
[.f
$cnr.c canvasx
$mx]
2247 set my
[.f
$cnr.c canvasy
$my]
2249 set wx
$NodeWidth($node)
2250 set wy
$NodeHeight($node)
2252 .f
$cnr.c coords
$node \
2253 [expr $mx-$wx] [expr $my-$wy] \
2254 [expr $mx+$wx] [expr $my+$wy]
2255 .f
$cnr.c coords
$TLabel($node) $mx $my
2257 set nodeX
($node) $mx
2258 set nodeY
($node) $my
2259 if {$together == 0} { return }
2261 foreach edge
$edgeHead($node) {
2262 set ec
[.f
$cnr.c coords
$edge]
2263 set nx
[expr $nodeX($node) + $Xrem($edge)*$Scale]
2264 set ny
[expr $nodeY($node) + $Yrem($edge)*$Scale]
2265 .f
$cnr.c coords
$edge \
2267 [lindex $ec 2] [lindex $ec 3]
2270 foreach edge
$edgeTail($node) {
2271 set ec
[.f
$cnr.c coords
$edge]
2272 set nx
[expr $nodeX($node) + $Xrem($edge)*$Scale]
2273 set ny
[expr $nodeY($node) + $Yrem($edge)*$Scale]
2274 .f
$cnr.c coords
$edge \
2275 [lindex $ec 0] [lindex $ec 1] \
2280 set PlaceCanvas
(msc
) ""
2282 proc mkcanvas
{n m geox geoy placed
} {
2283 global cnr tk_version
2284 global Chandle Sticky
2285 global FG BG Ptype PlaceCanvas
2289 wm title .f
$cnr "$n"
2290 wm iconname .f
$cnr $m
2292 if {$PlaceCanvas($m) == ""} {
2293 set PlaceCanvas
($m) "+$geox+$geoy"
2295 set k
[string first
"\+" $PlaceCanvas($m)]
2297 set PlaceCanvas
($m) [string range
$PlaceCanvas($m) $k end
]
2299 wm geometry .f
$cnr $PlaceCanvas($m)
2301 wm minsize .f
$cnr 100 100
2303 if {[string first
"4." $tk_version] == 0 \
2304 ||
[string first
"8." $tk_version] == 0} {
2305 set cv
[canvas .f
$cnr.c
-relief raised
-bd 2\
2306 -scrollregion {-15c -5c 30c
40c
} \
2308 -xscrollcommand ".f$cnr.hscroll set" \
2309 -yscrollcommand ".f$cnr.vscroll set"]
2310 scrollbar .f
$cnr.vscroll
-relief sunken
\
2311 -command ".f$cnr.c yview"
2312 scrollbar .f
$cnr.hscroll
-relief sunken
-orient horiz
\
2313 -command ".f$cnr.c xview"
2315 set cv
[canvas .f
$cnr.c
-relief raised
-bd 2\
2316 -scrollregion {-15c -5c 30c
40c
} \
2318 -xscroll ".f$cnr.hscroll set" \
2319 -yscroll ".f$cnr.vscroll set"]
2320 scrollbar .f
$cnr.vscroll
-relief sunken
\
2321 -command ".f$cnr.c yview"
2322 scrollbar .f
$cnr.hscroll
-relief sunken
-orient horiz
\
2323 -command ".f$cnr.c xview"
2325 set Chandle
($cnr) $cv
2326 #-width 500 -height 500
2328 button .f
$cnr.b1
-text "Close" \
2329 -command "set PlaceCanvas($m) [wm geometry .f$cnr]; destroy .f$cnr"
2330 button .f
$cnr.b2
-text "Save in: $m.ps" \
2331 -command "$cv postscript -file $m.ps -colormode $Ptype"
2333 pack append .f
$cnr \
2334 .f
$cnr.vscroll
{right filly
} \
2335 .f
$cnr.hscroll
{bottom fillx
} \
2336 .f
$cnr.c
{top expand fill
}
2340 checkbutton .f
$cnr.b6
-text "Preserve" \
2341 -variable Sticky
($cnr) \
2343 pack append .f
$cnr \
2344 .f
$cnr.b6
{ right padx
5}
2346 pack append .f
$cnr \
2347 .f
$cnr.b1
{right padx
5} \
2348 .f
$cnr.b2
{right padx
5}
2350 bind $cv <2> "$cv scan mark %x %y" ;# Geert Janssen, TUE
2351 bind $cv <B2-Motion
> "$cv scan dragto %x %y"
2353 .f
$cnr.c
bind node
<B1-Motion
> "
2354 moveNode $cnr \[.f$cnr.c find withtag current] %x %y 1
2357 # .f$cnr.c bind node <B2-Motion> "
2358 # moveNode $cnr \[.f$cnr.c find withtag current] %x %y 1
2361 tkwait visibility .f
$cnr
2365 proc addscales
{p
} {
2366 global Chandle Scale
2370 button .f
$p.b4
-text "Larger" \
2371 -command "$cv scale all 0 0 1.1 1.1; set Scale [expr $Scale*1.1]"
2372 button .f
$p.b5
-text "Smaller" \
2373 -command "$cv scale all 0 0 0.9 0.9; set Scale [expr $Scale*0.9]"
2375 .f
$p.b4
{right padx
5} \
2376 .f
$p.b5
{right padx
5}
2381 global Edges edgeHead edgeTail NodeWidth NodeHeight Maxx Maxy
2382 global State ELabel TransLabel Unix cnr lcnr Xrem Yrem DOT
2384 add_log
"<dot graph layout...>"
2385 set fd
[open "|$DOT" w
+]
2387 puts $fd "digraph dodot {"
2389 foreach el
[array names Edges
] {
2390 if { [ string first
$n $el ] >= 0 } {
2391 for {set i
0} { [lindex $Edges($el) $i] != "" } {incr i
} {
2392 set ntrg
[lindex $Edges($el) $i]
2393 puts $fd " \"$el\" -> \"$ntrg\"; "
2401 while {[gets $fd line
] > -1} {
2402 if {[string first
"\}" $line] >= 0} {
2405 set dd
[string length
$line]; incr dd
-1
2406 while {[string range
$line $dd $dd] == "\\"} {
2408 set line
"[string range $line 0 [expr $dd-1]]$more"
2409 set dd
[string length
$line]; incr dd
-1
2411 if {[string first
" -> " $line] >= 0} {
2412 set a
[string first
"\[pos=\"" $line]; incr a
8
2413 set b
[string first
"\"\];" $line]; incr b
-1
2414 set b2
[string first
"->" $line]
2415 set line1
[string range
$line 0 [expr $a - 9]]
2416 set src
[string range
$line1 0 [expr $b2 - 1]]
2417 set src
[string trim
$src " \""]
2418 set trg
[string range
$line1 [expr $b2 + 3] [expr $a - 1]]
2419 set trg
[string trim
$trg " \""]
2420 set tp
[string range
$line [expr $a-2] [expr $a-2]]
2421 set line
[string range
$line $a $b]
2422 set k
[split $line " "]
2424 set j2
[trunc
[expr $j/2]]
2425 set coords
".f$cnr.c create line "
2426 set spline
"-smooth 1"
2427 set nl
$ELabel($src,$trg)
2430 for {set i
1} {$i < $j} {incr i
} {
2431 scan [lindex $k $i] "%d,%d" x y
2432 set coords
" $coords[expr 50 + $x] [expr 50 + $Maxy - $y] "
2435 $TransLabel($State($src),$State($trg)) \
2436 [expr 50 + $x] [expr 50 + $Maxy - $y]
2437 .f
$cnr.c itemconfigure
\
2438 $TransLabel($State($src),$State($trg)) \
2439 -fill black
-text "$nl"
2442 scan [lindex $k 0] "%d,%d" x y
2443 set coords
" $coords[expr 50 + $x] [expr 50 + $Maxy - $y] "
2446 for {set i
0} {$i < $j} {incr i
} {
2447 scan [lindex $k $i] "%d,%d" x y
2448 set coords
" $coords[expr 50 + $x] [expr 50 + $Maxy - $y] "
2451 $TransLabel($State($src),$State($trg)) \
2452 [expr 50 + $x] [expr 50 + $Maxy - $y]
2453 .f
$cnr.c itemconfigure
\
2454 $TransLabel($State($src),$State($trg)) \
2455 -fill black
-text "$nl"
2457 set coords
"$coords -arrow $ends $spline -tags connector"
2459 set ne
[eval $coords]
2465 if {[string first
"node " $line] >= 0 \
2466 ||
[string first
"\{" $line] >= 0} {
2469 if {[string first
"graph " $line] >= 0} {
2470 set a
[string first
"\"" $line]; incr a
2471 set b
[string last
"\"" $line]; incr b
-1
2472 set line
[string range
$line $a $b]
2473 set k
[split $line ","]
2474 if {[llength $k] == 4} {
2475 set Maxx
[lindex $k 2]
2476 set Maxy
[lindex $k 3]
2478 set Maxx
[lindex $k 0]
2479 set Maxy
[lindex $k 1]
2483 set a
[string first
"\[" $line]; incr a
2484 set b
[string last
"\]" $line]; incr b
-1
2485 set line1
[string range
$line 0 [expr $a - 2]]
2486 set line
[string range
$line $a $b]
2487 set nn
[string trim
$line1 " \""]
2489 set a
[string first
"pos=" $line]; incr a
5
2490 set b
[string first
"\"" [string range
$line $a end
]]
2491 set b
[expr $a + $b - 1]
2492 set line1
[string range
$line $a $b]
2493 set k
[split $line1 ","]
2497 set a
[string first
"width=" $line]; incr a
7
2498 set b
[string first
"\"" [string range
$line $a end
]]
2499 set b
[expr $a + $b - 1]
2500 set w
[expr 75 * [string range
$line $a $b]]
2502 set a
[string first
"height=" $line]; incr a
8
2503 set b
[string first
"\"" [string range
$line $a end
]]
2504 set b
[expr $a + $b - 1]
2505 set h
[expr 75 * [string range
$line $a $b]]
2508 set NodeWidth
($State($nn)) [expr $w/2]
2509 set NodeHeight
($State($nn)) [expr $h/2]
2510 moveNode
$lcnr $State($nn) \
2511 [expr 50 + $x] [expr 50 + $Maxy - $y] 0
2519 add_log
"<cannot find dot>"
2521 tk_messageBox -icon info -message "<cannot find dot>"
2526 foreach el
[array names Edges
] {
2527 if { [ string first
$n $el ] >= 0 } {
2529 foreach edge
$edgeHead($State($el)) {
2530 .f
$cnr.c delete
$edge
2532 unset edgeHead
($State($el))
2533 unset edgeTail
($State($el))
2536 .f
$cnr.c
bind node
<B1-Motion
> {} ;# no moving
2537 .f
$cnr.c
bind node
<B2-Motion
> {}
2538 catch { destroy .f
$lcnr.b6
}
2539 # button .f$lcnr.b6 -text "No Labels" \
2540 # -command ".f$lcnr.c delete texttag; destroy .f$lcnr.b6"
2541 button .f
$lcnr.b6
-text "No Labels" \
2542 -command "hide_automata_labels .f$lcnr.b6 .f$cnr.c"
2543 pack append .f
$lcnr .f
$lcnr.b6
{right padx
5}
2546 proc hide_automata_labels
{b c
} {
2547 $b configure
-text "Add Labels"
2548 $c itemconfigure texttag
-fill white
2549 $b configure
-command "show_automata_labels $b $c"
2552 proc show_automata_labels
{b c
} {
2553 $b configure
-text "No Labels"
2554 $c itemconfigure texttag
-fill black
2555 $b configure
-command "hide_automata_labels $b $c"
2559 set foo
[string first
"." $p]
2562 set p
[string range
$p 0 $foo]
2570 global FG BG HelvBig version xversion
2575 wm title .h
"About SPIN"
2576 wm iconname .h
"About"
2577 message .h.t
-width 600 -background $BG -foreground $FG -font $HelvBig \
2579 Xspin Version $xversion
2581 Spin is an on-the-fly LTL model checking system
2582 for proving properties of asynchronous software
2583 system designs, first distributed in 1991.
2585 The master sources for the latest version of
2586 this software can always be found via:
2588 http://spinroot.com/spin/whatispin.html
2590 For help: spin_list@spinroot.com
2592 The Spin sources are (c) 1990-2004 Bell Labs,
2593 Lucent Technologies, Murray Hill, NJ, USA.
2594 All rights are reserved. This software is for
2595 educational and research purposes only.
2596 No guarantee whatsoever is expressed or implied
2597 by the distribution of this code.
2599 button .h.b
-text "Ok" -command {destroy .h
}
2600 pack append .h .h.t
{top expand fill
}
2601 pack append .h .h.b
{top
}
2605 global FG BG HelvBig
2610 wm title .h
"Promela URL"
2611 wm iconname .h
"Promela"
2612 message .h.t
-width 600 -background $BG -foreground $FG -font $HelvBig \
2613 -text "All Promela references are available online:
2615 http://spinroot.com/spin/Man/index.html
2618 button .h.b
-text "Ok" -command {destroy .h
}
2619 pack append .h .h.t
{top expand fill
}
2620 pack append .h .h.b
{top
}
2624 global FG BG HelvBig
2629 wm title .h
"Help with Xspin"
2630 wm iconname .h
"Help"
2631 message .h.t
-background $BG -foreground $FG -font $HelvBig \
2633 Spin Version Controller - (c) 1993-2004 Bell Laboratories
2635 Enter a Promela model into the main text window, or 'Open'
2636 one via the File Menu (e.g., from Spin's Test directory).
2637 Once loaded, you can revert to the stored version of the file
2638 with option ReOpen. Select Clear to empty the text window.
2640 In the log, just below the text-window, background
2641 commands are printed that Xspin generates.
2642 Outputs from Simulation and Verification runs always
2643 appear in separate windows.
2645 All run-time options are available through the Run menu.
2646 A typical way of working with Xspin is to use:
2648 - First a Syntax Check to get hints and warnings
2649 - Random Simulation for further debugging
2650 - Add the properties to be verified (assertions, never claims)
2651 - Perform a Slicing Check to check for redundancy
2652 - Perform Verification for a correctness proof
2653 - Guided Simulation to inspect errors reported by
2654 the Verification option
2656 Clicking Button-1 in the main window updates the
2657 Line number display at the top of the window -- as a
2658 simple way of finding out at what line you are.
2660 You can also use another editor to update the
2661 specifications outside Xspin, and use the ReOpen
2662 command from the File menu to refresh the Xspin
2663 edit buffer before starting each new simulation or
2665 button .h.b
-text "Ok" -command {destroy .h
}
2666 pack append .h .h.t
{top expand fill
}
2667 pack append .h .h.b
{top
}
2675 proc put_template
{s
} {
2676 .tl.main.e1 delete
0 end
2677 .tl.main.e1 insert end
"$s"
2680 set PlaceTL
"+100+1"
2682 proc call_tl
{} { ;# expanded interface
2683 global formula tl_stat nv_typ an_typ cp_typ
2684 global FG BG Fname firstime PlaceTL
2689 set k
[string first
"\+" $PlaceTL]
2691 set PlaceTL
[string range
$PlaceTL $k end
]
2694 wm title .tl
"Linear Time Temporal Logic Formulae"
2695 wm iconname .tl
"LTL"
2696 wm geometry .tl
$PlaceTL
2699 entry .tl.main.e1
-relief sunken
\
2700 -background $BG -foreground $FG
2701 label .tl.main.e2
-text "Formula: "
2706 pack append .tl.op
[label .tl.op.s0
-text "Operators: " \
2707 -relief flat
] {left
}
2708 pack append .tl.op
[button .tl.op.always
-width 1 -text "\[\]" \
2709 -command ".tl.main.e1 insert insert \"$alw \""] {left
}
2710 pack append .tl.op
[button .tl.op.
event -width 1 -text "\<\>" \
2711 -command ".tl.main.e1 insert insert \"$eve \""] {left
}
2712 pack append .tl.op
[button .tl.op.until
-width 1 -text "U" \
2713 -command ".tl.main.e1 insert insert \" U \""] {left
}
2714 pack append .tl.op
[button .tl.op.impl
-width 1 -text "->" \
2715 -command ".tl.main.e1 insert insert \" -> \""] {left
}
2716 pack append .tl.op
[button .tl.op.and
-width 1 -text "and" \
2717 -command ".tl.main.e1 insert insert \" && \""] {left
}
2718 pack append .tl.op
[button .tl.op.or
-width 1 -text "or" \
2719 -command ".tl.main.e1 insert insert \" || \""] {left
}
2720 pack append .tl.op
[button .tl.op.not
-width 1 -text "not" \
2721 -command ".tl.main.e1 insert insert \" ! \""] {left
}
2723 frame .tl.b
-relief ridge
-borderwidth 4
2724 label .tl.b.s0
-text "Property holds for: "
2725 radiobutton .tl.b.s1
-text "All Executions (desired behavior)" \
2726 -variable tl_stat
-value 0
2727 radiobutton .tl.b.s2
-text "No Executions (error behavior)" \
2728 -variable tl_stat
-value 1
2734 .tl.main.e1 insert end
$formula
2736 button .tl.main.
file -text "Load..." \
2737 -command "browse_tl"
2739 bind .tl.main.e1
<Return
> { do_ltl
}
2741 pack append .tl.main
\
2742 .tl.main.e2
{top left
}\
2743 .tl.main.e1
{top left expand fill
} \
2744 .tl.main.
file {top right
}
2746 pack append .tl .tl.main
{top fillx
frame e
}
2747 pack append .tl .tl.op
{top
frame w
}
2748 pack append .tl .tl.b
{top fillx
frame w
}
2750 frame .tl.macros
-relief ridge
-borderwidth 4
2751 label .tl.macros.title
-text "Symbol Definitions:" -relief flat
2752 scrollbar .tl.macros.s
-relief flat
\
2753 -command ".tl.macros.t yview"
2754 text .tl.macros.t
-height 4 -relief raised
-bd 2 \
2755 -yscrollcommand ".tl.macros.s set" \
2756 -background $BG -foreground $FG \
2760 pack append .tl.macros
\
2761 .tl.macros.title
{top
frame w
} \
2762 .tl.macros.s
{left filly
} \
2763 .tl.macros.t
{left expand fill
}
2765 frame .tl.notes
-relief ridge
-borderwidth 4
2766 label .tl.notes.title
-text "Notes: " -relief flat
2767 scrollbar .tl.notes.s
-relief flat
\
2768 -command ".tl.notes.t yview"
2769 text .tl.notes.t
-height 4 -relief raised
-bd 2 \
2770 -yscrollcommand ".tl.notes.s set" \
2771 -background $BG -foreground $FG \
2774 pack append .tl.notes
\
2775 .tl.notes.title
{top fillx
frame w
} \
2776 .tl.notes.s
{left filly
} \
2777 .tl.notes.t
{left expand fill
}
2781 label .tl.never.top.title
-text "Never Claim:"\
2783 button .tl.never.top.gc
-text "Generate" \
2785 pack append .tl.never.top
\
2786 .tl.never.top.gc
{right
}\
2787 .tl.never.top.title
{left
}
2789 scrollbar .tl.never.s
-relief flat
\
2790 -command ".tl.never.t yview"
2791 text .tl.never.t
-height 8 -relief raised
-bd 2 \
2792 -yscrollcommand ".tl.never.s set" \
2795 pack append .tl.never
\
2796 .tl.never.top
{top fillx
frame w
} \
2797 .tl.never.s
{left filly
} \
2798 .tl.never.t
{left expand fill
}
2801 frame .tl.results.top
2803 button .tl.results.top.svp
-text "Run Verification" \
2804 -command "do_ltl; basicval2"
2805 label .tl.results.top.title
-text "Verification Result:"\
2807 pack append .tl.results.top
\
2808 .tl.results.top.svp
{right
}\
2809 .tl.results.top.title
{left
}
2811 scrollbar .tl.results.s
-relief flat
\
2812 -command ".tl.results.t yview"
2813 text .tl.results.t
-height 7 -relief raised
-bd 2 \
2814 -yscrollcommand ".tl.results.s set" \
2817 pack append .tl.results
\
2818 .tl.results.top
{top fillx
frame w
} \
2819 .tl.results.s
{left filly
} \
2820 .tl.results.t
{left expand fill
}
2823 .tl.notes
{top expand fill
} \
2824 .tl.macros
{top expand fill
} \
2825 .tl.never
{top expand fill
} \
2826 .tl.results
{top expand fill
} \
2828 pack append .tl
[button .tl.sv
-text "Save As.." \
2829 -command "save_tl"] {right
}
2830 pack append .tl
[button .tl.
exit -text "Close" \
2831 -command "set PlaceTL [wm geometry .tl]; destroy .tl"] {right
}
2833 pack append .tl
[button .tl.help
-text "Help" -fg red
\
2834 -command "roadmap4"] {left
}
2835 pack append .tl
[button .tl.clear
-text "Clear" \
2836 -command ".tl.main.e1 delete 0 end; .tl.never.t delete 0.0 end"] {left
}
2842 proc purge_nvr
{foo
} {
2843 set j
[llength $foo]; incr j
-1
2844 for {set i
$j} {$i >= 0} {incr i
-1} {
2845 set k
[lindex $foo $i]
2847 .tl.never.t delete
$k.0 $kk.0
2851 proc grab_nvr
{inp target
} {
2854 scan [.tl.never.t index end
] %d numLines
2858 for {set i
1} {$i < $numLines} { incr i
} {
2859 .tl.never.t mark
set last
$i.0
2860 set have
[.tl.never.t get last
"last lineend + 1 chars"]
2861 if {[regexp -indices $pattern $have indices
]} {
2863 set yes
[expr 1 - $yes]
2865 set pattern
"#endif"
2870 if {$yes && [string first
$inp $have] != 0} {
2871 $target insert end
"$have"
2878 proc extract_defs
{} {
2881 set pattern
"#define "
2882 scan [.tl.never.t index end
] %d numLines
2885 for {set i
1} {$i < $numLines} { incr i
} {
2886 .tl.never.t mark
set last
$i.0
2887 set have
[.tl.never.t get last
"last lineend + 1 chars"]
2888 if {[regexp -indices $pattern $have indices
]} {
2889 .tl.macros.t insert end
"$have"
2892 set have
[.tl.never.t get last
"last lineend"]
2893 set k
[string first
"Formula As Typed: " $have]
2895 set ff
[string range
$have [expr $k+18] end
]
2896 .tl.main.e1 insert end
$ff
2898 if {[string first
"To The Negated Formula " $have] > 0} {
2904 grab_nvr
"#ifdef NOTES" .tl.notes.t
2905 grab_nvr
"#ifdef RESULT" .tl.results.t
2908 proc inspect_ltl
{} {
2910 set formula
"[.tl.main.e1 get]"
2913 regsub -all {\&\&} "$x" " " y
; set x
$y
2914 regsub -all {\|
\|
} "$x" " " y
; set x
$y
2915 regsub -all {\/\\} "$x" " " y
; set x
$y
2916 regsub -all {\\\/} "$x" " " y
; set x
$y
2917 regsub -all {\!} "$x" " " y
; set x
$y
2918 regsub -all {<->} "$x" " " y
; set x
$y
2919 regsub -all {\->} "$x" " " y
; set x
$y
2920 regsub -all {\[\]} "$x" " " y
; set x
$y
2921 regsub -all {\<\>} "$x" " " y
; set x
$y
2922 regsub -all {[()]} "$x" " " y
; set x
$y
2923 regsub -all {\ \ *} "$x" " " y
; set x
$y
2924 regsub -all { U
} "$x" " " y
; set x
$y
2925 regsub -all { V
} "$x" " " y
; set x
$y
2926 regsub -all { X
} "$x" " " y
; set x
$y
2928 set predefs
" np_ true false "
2930 set k
[split $x " "]
2932 set line
[.tl.macros.t get
0.0 end
]
2933 for {set i
0} {$i < $j} {incr i
} {
2934 if {[string length
[lindex $k $i]] > 0 \
2935 && [string first
" [lindex $k $i] " $predefs] < 0} {
2936 set pattern
"#define [lindex $k $i]"
2937 if {[string first
$pattern $line] < 0} {
2939 .tl.macros.t insert end
"$pattern\t?\n"
2941 set line
[.tl.macros.t get
0.0 end
]
2946 global formula tl_stat SPIN tk_major tk_minor
2948 set formula
"[.tl.main.e1 get]"
2949 .tl.never.t delete
0.0 end
2952 catch { inspect_ltl
}
2954 set MostSystems
1 ;# change to 0 only if there are problems
2957 if {$tl_stat == 0} {
2958 add_log
"$SPIN -f \"!( $formula )\""
2960 catch {exec $SPIN -f "!($formula)" >&pan.ltl
} err
2962 # this variant was needed on some older systems,
2963 # but it causes problems on some of the newer ones...
2964 catch {exec $SPIN -f \"!($formula)\" >&pan.ltl
} err
2967 add_log
"$SPIN -f \"( $formula )\""
2969 catch {exec $SPIN -f "($formula)" >&pan.ltl
} err
2972 catch {exec $SPIN -f \"($formula)\" >&pan.ltl
} err
2978 add_log
"<error: $err>"
2979 add_log
"hint: check the Help Button for syntax rules"
2981 .tl.never.t insert end
\
2983 .tl.never.t insert end
\
2984 " * Formula As Typed: $formula\n"
2986 if {$tl_stat == 0} {
2987 .tl.never.t insert end
\
2988 " * The Never Claim Below Corresponds\n"
2989 .tl.never.t insert end
\
2990 " * To The Negated Formula !($formula)\n"
2991 .tl.never.t insert end
\
2992 " * (formalizing violations of the original)\n"
2995 .tl.never.t insert end
\
3000 set fd
[open pan.ltl r
]
3001 while {[gets $fd line
] > -1} {
3002 .tl.never.t insert end
"$line\n"
3014 set fnm
[.sv_tl.ent get
]
3017 if {[file_ok
$fnm]==0} return
3018 set fd
[open $fnm w
]
3019 add_log
"<save claim in $fnm>"
3020 catch { puts $fd "[.tl.macros.t get 0.0 end]" nonewline
}
3022 puts $fd "[.tl.never.t get 0.0 end]" nonewline
3024 catch { puts $fd "#ifdef NOTES"
3025 puts $fd "[.tl.notes.t get 0.0 end]" nonewline
3028 catch { puts $fd "#ifdef RESULT"
3029 puts $fd "[.tl.results.t get 0.0 end]" nonewline
3035 catch "destroy .sv_tl"
3036 catch "focus .tl.main.e1"
3040 global Fname PlaceWarn
3041 catch {destroy .sv_tl
}
3044 wm title .sv_tl
"Save Claim"
3045 wm iconname .sv_tl
"Save"
3046 wm geometry .sv_tl
$PlaceWarn
3048 label .sv_tl.msg
-text "Name for LTL File: " -relief flat
3049 entry .sv_tl.ent
-width 6 -relief sunken
-textvariable fnm
3050 button .sv_tl.b1
-text "Ok" -command { dump_tl
"" }
3051 button .sv_tl.b2
-text "Cancel" -command "destroy .sv_tl"
3052 bind .sv_tl.ent
<Return
> { dump_tl
"" }
3054 set fnm
[.sv_tl.ent get
]
3056 .sv_tl.ent insert end
"$Fname.ltl"
3059 pack append .sv_tl
\
3060 .sv_tl.msg
{top
frame w
} \
3061 .sv_tl.ent
{top
frame e expand fill
} \
3062 .sv_tl.b1
{right
frame e
} \
3063 .sv_tl.b2
{right
frame e
}
3068 global BG FG HelvBig PlaceWarn
3069 catch {destroy .warn
}
3071 set k
[string first
"\+" $PlaceWarn]
3073 set PlaceWarn
[string range
$PlaceWarn $k end
]
3076 wm title .warn
"Accept"
3077 wm iconname .warn
"Accept"
3078 wm geometry .warn
$PlaceWarn
3080 message .warn.t
-width 300 \
3081 -background $BG -foreground $FG -font $HelvBig \
3085 1. Save the Never Claim in a file, \
3086 for instance a file called 'never', \
3087 using the <Save> button.
3093 (the name of the file with the claim) \
3094 at the end of the main specification.
3096 3. Insert macro definitions (#define's) for all \
3097 propositional symbols used in the formula.
3099 For instance, with LTL formula
3100 '[] p -> <> q' add the macro defs:
3102 #define p (cnt == 1)
3105 These macros must be defined just above the line \
3106 with the #include \"never\" directive
3108 4. Perform the verification, and make sure that \
3109 the box 'Apply Never Claim' is checked in the \
3110 Verification Panel (or else the claim is ignored).
3111 You can have a library of claim files that you can \
3112 choose from for verification, by changing only the \
3113 name of the include file.
3115 5. Never claims have no effect during simulation runs.
3117 6. See the HELP->LTL menu for more information.
3120 button .warn.b
-text "Ok" \
3121 -command {set PlaceWarn
[wm geometry .warn
]; destroy .warn
}
3122 pack append .warn .warn.t
{top expand fill
}
3123 pack append .warn .warn.b
{right
frame e
}
3132 wm title .h
"LTL Help"
3133 wm iconname .h
"Help"
3135 scrollbar .h.z.s
-command ".h.z.t yview"
3136 text .h.z.t
-relief raised
-bd 2 \
3137 -background $BG -foreground $FG \
3138 -yscrollcommand ".h.z.s set" \
3139 -setgrid 1 -width 60 -height 30 -wrap word
3141 .h.z.s
{left filly
} \
3142 .h.z.t
{left expand fill
}
3143 .h.z.t insert end
"GUIDELINES:
3144 You can load an LTL template or a previously saved LTL
3145 formula from a file via the LOAD button on the upper
3146 right of the LTL Property Manager panel.
3148 Define a new LTL formula using lowercase names for the
3149 propositional symbols, for instance:
3151 The formula expresses either a positive (desired) or a
3152 negative (undesired) property of the model. A positive
3153 property is negated automatically by the translator to
3154 convert it in a never claim (which expresses the
3155 corresponding negative property (the undesired behavior
3156 that is claimed 'never' to occur).
3158 When you type a <Return> or hit the <Generate> button,
3159 the formula is translated into an equivalent never-claim.
3161 You must add a macro-definition for each propositional
3162 symbol used in the LTL formula. Insert these definitions
3163 in the symbols window of the LTL panel, they will be
3164 remembered together with the annotations and verification
3165 result if the formula is saved in an .ltl file.
3166 Enclose the symbol definitions in braces, to secure correct
3167 operator precedence, for instance:
3170 #define q (len(q) < 5)
3172 Valid temporal logic operators are:
3173 \[\] Always (no space between \[ and \])
3174 <> Eventually (no space between < and >)
3176 V The Dual of Until: (p V q) == !(!p U !q)
3178 All operators are left-associative (incl. U and V).
3181 && Logical And (alternative form: /\\, no spaces)
3183 || Logical Or (alternative form: \\/, no spaces)
3184 -> Logical Implication
3185 <-> Logical Equivalence
3189 any name that starts with a lowercase letter
3197 Generic properties/Templates:
3199 Response: p -> \<\> q
3200 Precedence: p -> (q U r)
3201 Objective: p -> \<\> (q || r)
3203 Each of the above 4 generic types of properties
3204 can (and will generally have to) be prefixed by
3205 temporal operators such as
3206 \[\], \<\>, \[\]\<\>, \<\>\[\]
3207 The last (objective) property can be read to mean
3208 that 'p' is a trigger, or 'enabling' condition that
3209 determines when the requirement becomes applicable
3210 (e.g. the sending of a new data message); then 'q'
3211 can be the fullfillment of the requirement (e.g.
3212 the arrival of the matching acknowledgement), and
3213 'r' could be a discharging condition that voids the
3214 applicability of the check (an abort condition).
3216 button .h.b
-text "Ok" -command {destroy .h
}
3217 pack append .h .h.z
{top expand fill
}
3218 pack append .h .h.b
{top
}
3219 .h.z.t configure
-state disabled
3220 .h.z.t yview
-pickplace 1.0
3231 catch {destroy .road1
}
3234 wm title .road1
"Help with Simulation"
3235 wm iconname .road1
"SimHelp"
3237 scrollbar .road1.z.s
-command ".road1.z.t yview"
3238 text .road1.z.t
-relief raised
-bd 2 \
3239 -background $BG -foreground $FG \
3240 -yscrollcommand ".road1.z.s set" \
3241 -setgrid 1 -width 60 -height 30 -wrap word
3242 pack append .road1.z
\
3243 .road1.z.s
{left filly
} \
3244 .road1.z.t
{left expand fill
}
3245 .road1.z.t insert end
"GUIDELINES:
3246 0. Always use a Syntax Check before running simulations.\
3247 It shakes out the more obvious flaws in the model.
3249 1. Random simulation option is used to debug a model.\
3250 Other than assert statements, no correctness requirements\
3251 are checked during simulation runs. All nondeterministic\
3252 decisions are resolved randomly. You can of course still\
3253 force a selection to go into a specific direction by \
3254 modifying the model.\
3255 A random run is repeated precisely if the Seed Value\
3256 for the random number generator is kept the same.
3258 2. Interactive simulation can be used to force the\
3259 execution towards a known point. The user is prompted\
3260 at every point in the execution where a nondeterministic\
3261 choice has to be resolved.
3263 3. A guided simulation is used to follow an error-trail that was\
3264 produced by the verifier. If the trail gets to be thousands of execution\
3265 steps long, this can be time-consuming. \
3266 You can skip the initial portion of such a long trail by typing\
3267 a number in the 'Steps Skipped' box in the Simulation Panel .
3269 4. The options in the Simulations Panel allow you to enable or\
3270 disable types of displays that are maintained during simulation\
3271 runs. Usually, it is not necessary to look at all possible display panels.\
3272 Experiment to see which displays you find most useful.
3274 5. To track the value changes of Selected variables, in the\
3275 Message Sequence Chart and in the Variable Values Panel, add a prefix\
3276 'show ' to the declaration of the selected variables in the Promela\
3277 specification, e.g. use 'show byte cnt;' instead of 'byte cnt;'"
3279 button .road1.b
-text "Ok" -command {destroy .road1
}
3280 pack append .road1 .road1.z
{top expand fill
}
3281 pack append .road1 .road1.b
{top
}
3282 .road1.z.t configure
-state disabled
3283 .road1.z.t yview
-pickplace 1.0
3290 catch {destroy .road2
}
3293 wm title .road2
"Help with Verification Parameters"
3294 wm iconname .road2
"ValHelp"
3296 scrollbar .road2.z.s
-command ".road2.z.t yview"
3297 text .road2.z.t
-relief raised
-bd 2 \
3298 -background $BG -foreground $FG \
3299 -yscrollcommand ".road2.z.s set" \
3300 -setgrid 1 -width 60 -height 18 -wrap word
3301 pack append .road2.z
\
3302 .road2.z.s
{left filly
} \
3303 .road2.z.t
{left expand fill
}
3304 .road2.z.t insert end
"Physical Memory Available:
3305 Set this number to amount of physical (not virtual)
3306 memory in your system, in MegaBytes, and leave it there for all runs.
3308 When the limit is reached, the verification is stopped to
3311 The number entered here is the number of MegaBytes directly
3312 (not a power of two, as in previous versions of xspin).
3314 If an exhaustive verification cannot be completed due to
3315 lack of memory, use compression, or switch to a
3316 supertrace/bitstate run under basic options."
3318 button .road2.b
-text "Ok" -command {destroy .road2
}
3319 pack append .road2 .road2.z
{top expand fill
}
3320 pack append .road2 .road2.b
{top
}
3321 .road2.z.t configure
-state disabled
3322 .road2.z.t yview
-pickplace 1.0
3328 catch {destroy .road2
}
3331 wm title .road2
"Help with Verification"
3332 wm iconname .road2
"ValHelp"
3334 scrollbar .road2.z.s
-command ".road2.z.t yview"
3335 text .road2.z.t
-relief raised
-bd 2 \
3336 -background $BG -foreground $FG \
3337 -yscrollcommand ".road2.z.s set" \
3338 -setgrid 1 -width 60 -height 15 -wrap word
3339 pack append .road2.z
\
3340 .road2.z.s
{left filly
} \
3341 .road2.z.t
{left expand fill
}
3342 .road2.z.t insert end
"Estimated State Space Size:
3343 This parameter is used to calculate the size of the
3344 hash-table. It results in a selection of a numeric argument
3345 for the -w flag of the verifier. Setting it too high may
3346 cause an out-of-memory error with zero states reached
3347 (meaning that the verification could not be started).
3348 Setting it too low can cause inefficiencies due to
3351 In Bitstate runs begin with the default estimate for
3352 this parameter. After a run completes successfully,
3353 double the estimate, and see if the number of reached
3354 stated changes much. Continue to do this until
3355 it stops changing, or until you overflow the memory
3356 bound and run out of memory.
3358 The closest power of two is taken by xspin to set the
3359 true number used for the number of reachable states.
3360 (The selected power of two is visible as the number that
3361 follow the -w flag in the run-line that xspin generates).
3363 To set a specific -w parameter, use the Extra Run-Time Option
3364 Field. If, for instance, -w32 is specified there, it will
3365 override the value computed from the Estimated State Space Size."
3367 button .road2.b
-text "Ok" -command {destroy .road2
}
3368 pack append .road2 .road2.z
{top expand fill
}
3369 pack append .road2 .road2.b
{top
}
3370 .road2.z.t configure
-state disabled
3371 .road2.z.t yview
-pickplace 1.0
3377 catch {destroy .road2
}
3380 wm title .road2
"Help with Verification"
3381 wm iconname .road2
"ValHelp"
3383 scrollbar .road2.z.s
-command ".road2.z.t yview"
3384 text .road2.z.t
-relief raised
-bd 2 \
3385 -background $BG -foreground $FG \
3386 -yscrollcommand ".road2.z.s set" \
3387 -setgrid 1 -width 60 -height 20 -wrap word
3388 pack append .road2.z
\
3389 .road2.z.s
{left filly
} \
3390 .road2.z.t
{left expand fill
}
3391 .road2.z.t insert end
"Maximum Search Depth:
3392 This number determines the size of the depth-first
3393 search stack that is used during the verification.
3394 The stack uses memory, so a larger number increases
3395 the memory requirements, and a lower number decreases
3396 it. In a tight spot, when there seems not to be
3397 sufficient memory for the search depth needed, you
3398 can reduce the estimated state space size to free some
3399 more memory for the stack.
3401 If you hit the maximum search depth during a verification
3402 (noted as 'Search not completed' or 'Search Truncated'
3403 in the verification output) without finding an error,
3404 double the search depth parameter and repeat the run."
3406 button .road2.b
-text "Ok" -command {destroy .road2
}
3407 pack append .road2 .road2.z
{top expand fill
}
3408 pack append .road2 .road2.b
{top
}
3409 .road2.z.t configure
-state disabled
3410 .road2.z.t yview
-pickplace 1.0
3417 catch {destroy .road2
}
3420 wm title .road2
"Help with Verification"
3421 wm iconname .road2
"ValHelp"
3423 scrollbar .road2.z.s
-command ".road2.z.t yview"
3424 text .road2.z.t
-relief raised
-bd 2 \
3425 -background $BG -foreground $FG \
3426 -yscrollcommand ".road2.z.s set" \
3427 -setgrid 1 -width 60 -height 10 -wrap word
3428 pack append .road2.z
\
3429 .road2.z.s
{left filly
} \
3430 .road2.z.t
{left expand fill
}
3431 .road2.z.t insert end
"Number of hash functions:
3432 This number determines how many bits are set per
3433 state when in Bitstate verification mode. The default is 2.
3434 At the end of a Bitstate verification run, the verifier
3435 can issue a recommendation for a different setting of
3436 this flag (which is the -k flag), it a change can be
3437 predicted to lead to better coverage."
3439 button .road2.b
-text "Ok" -command {destroy .road2
}
3440 pack append .road2 .road2.z
{top expand fill
}
3441 pack append .road2 .road2.b
{top
}
3442 .road2.z.t configure
-state disabled
3443 .road2.z.t yview
-pickplace 1.0
3450 catch {destroy .road2
}
3453 wm title .road2
"Help with Verification"
3454 wm iconname .road2
"ValHelp"
3456 scrollbar .road2.z.s
-command ".road2.z.t yview"
3457 text .road2.z.t
-relief raised
-bd 2 \
3458 -background $BG -foreground $FG \
3459 -yscrollcommand ".road2.z.s set" \
3460 -setgrid 1 -width 60 -height 26 -wrap word
3461 pack append .road2.z
\
3462 .road2.z.s
{left filly
} \
3463 .road2.z.t
{left expand fill
}
3464 .road2.z.t insert end
"GENERAL GUIDELINES:
3465 => When just starting out, it is safe to leave all parameters in the\
3466 Verification Options Panel set at their initial value and to simply\
3467 push the Run button in the Basic Options Panel for a default\
3468 exhaustive verification.\
3469 If you run out of memory, adjust the parameter settings as \
3470 indicated under the 'explain' options.
3472 => If an error is found, first try to reduce the search depth to \
3473 find a shorter equivalent. Once you're content with the length,\
3474 move on to a guided simulation to inspect the error-trail in detail.\
3475 Optionally, use the Find Shortest Trail option, but note that this\
3476 can increase runtime and memory use. So: do not use this option until\
3477 you are certain that an error exists -- leave it turned off by default).\
3478 If you are verifying a Safety Property, try the Breadth-First Search\
3479 mode to find the shortest counter-example. It may run out of memory\
3480 sooner than the default depth-first search mode, but it often works.
3482 => It is always safe to leave the Partial Order Reduction option enabled.\
3483 Turn it off only for debugging purposes, or when warned to do so by the \
3484 verifier itself. The Profiling option gathers statistics about the \
3485 verification hot-spots in the model.
3487 => If you save all error-trails, you have to copy the one you are\
3488 interested in inspecting with a guided simulation onto the file\
3489 pan_in.trail manually (outside xspin) after the run completes.\
3490 The trails are numbered in order of discovery."
3492 button .road2.b
-text "Ok" -command {destroy .road2
}
3493 pack append .road2 .road2.z
{top expand fill
}
3494 pack append .road2 .road2.b
{top
}
3495 .road2.z.t configure
-state disabled
3496 .road2.z.t yview
-pickplace 1.0
3503 catch {destroy .road2
}
3506 wm title .road2
"Help with Verification"
3507 wm iconname .road2
"ValHelp"
3509 scrollbar .road2.z.s
-command ".road2.z.t yview"
3510 text .road2.z.t
-relief raised
-bd 2 \
3511 -background $BG -foreground $FG \
3512 -yscrollcommand ".road2.z.s set" \
3513 -setgrid 1 -width 60 -height 25 -wrap word
3514 pack append .road2.z
\
3515 .road2.z.s
{left filly
} \
3516 .road2.z.t
{left expand fill
}
3517 .road2.z.t insert end
"BASIC GUIDELINES:
3518 When just starting out, it is safe to leave all parameters\
3519 at their initial value and to push the Run button for a\
3520 default exhaustive verification.\
3521 If you run out of memory, adjust the parameter settings\
3522 under Advanced Options.
3524 => Safety properties are properties of single states (like\
3525 deadlocks = invalid endstates, or assertion violations).
3527 => Liveness properties are properties of sequences of\
3528 states (typically: infinite sequences, i.e., cycles).\
3529 There are two types of cycles: non-progress (not passing\
3530 through any state marked with a 'progress' label) and\
3531 acceptance (passing infinitely often through a state\
3532 marked with an 'accept' label).
3534 => Use the Weak Fairness option only when really necessary,\
3535 to avoid unwated error reports. It can increase the CPU-time\
3536 requirements by a factor roughly equal to twice the number of\
3539 => It is safe to leave the Reduced Search option enabled.\
3540 Turn it off only for debugging purposes, or when warned to do so by the \
3541 verifier itself. The Profiling option gathers statistics about the \
3542 verification hot-spots in the model.
3544 => You can apply a Never Claim even when checking Safety Properties\
3545 when you want to restrict the search to the sequences that are\
3546 matched by the claim (a user-guided search pruning technique)."
3548 button .road2.b
-text "Ok" -command {destroy .road2
}
3549 pack append .road2 .road2.z
{top expand fill
}
3550 pack append .road2 .road2.b
{top
}
3551 .road2.z.t configure
-state disabled
3552 .road2.z.t yview
-pickplace 1.0
3559 catch {destroy .road2
}
3562 wm title .road2
"Help with Verification"
3563 wm iconname .road2
"ValHelp"
3565 scrollbar .road2.z.s
-command ".road2.z.t yview"
3566 text .road2.z.t
-relief raised
-bd 2 \
3567 -background $BG -foreground $FG \
3568 -yscrollcommand ".road2.z.s set" \
3569 -setgrid 1 -width 60 -height 15 -wrap word
3570 pack append .road2.z
\
3571 .road2.z.s
{left filly
} \
3572 .road2.z.t
{left expand fill
}
3573 .road2.z.t insert end
"GUIDELINES:
3574 This will run a verification for the specific LTL property\
3575 that was defined in the LTL options panel that brought you\
3576 here. The claim was placed in a separate .ltl\
3577 file, not included in the main specification.\
3578 (It will be picked up in the verification automatically.)\
3579 The separate .ltl file combines the notes, formula,\
3580 macros, results, etc., for easier tracking.
3582 On a first run, leave all choices at their initial\
3583 value and push the Run button for a default verification.\
3584 If you run out of memory, adjust the parameter settings\
3585 under Advanced Options.
3587 Use the Weak Fairness option only when really necessary,\
3588 to avoid unwated error reports. It can increase the CPU-time\
3589 requirements by a factor roughly equal to twice the number of\
3592 button .road2.b
-text "Ok" -command {destroy .road2
}
3593 pack append .road2 .road2.z
{top expand fill
}
3594 pack append .road2 .road2.b
{top
}
3595 .road2.z.t configure
-state disabled
3596 .road2.z.t yview
-pickplace 1.0
3603 catch {destroy .road2
}
3606 wm title .road2
"Help with Verification"
3607 wm iconname .road2
"ValHelp"
3609 scrollbar .road2.z.s
-command ".road2.z.t yview"
3610 text .road2.z.t
-relief raised
-bd 2 \
3611 -background $BG -foreground $FG \
3612 -yscrollcommand ".road2.z.s set" \
3613 -setgrid 1 -width 60 -height 20 -wrap word
3614 pack append .road2.z
\
3615 .road2.z.s
{left filly
} \
3616 .road2.z.t
{left expand fill
}
3617 .road2.z.t insert end
"GUIDELINES:
3618 When just starting out, it is safe to leave all
3619 verification parameters set at their initial values
3620 and to Run a default verification.
3621 If you run out of memory, or encounter other problems,
3622 look at the specific help options in the verification
3624 One parameter is important to set correctly right from
3625 the start: the physical memory size of your system.
3626 It is by default set to 64 Mbytes. Set it once to the
3627 true amount of physical memory on your system, in Megabytes,
3628 and never change it again (unless you buy more physical
3629 memory for your machine of course).
3630 You can find this parameter under advanced options in the
3631 verification parameters panel.
3632 Bitstate/Supertrace verifications are approximate, and
3633 only used for models too large to verify exhaustively.
3634 This option allows you to get at least an approximate
3635 answer to the correctness of models that could otherwise
3636 not be verified by a finite state system."
3638 button .road2.b
-text "Ok" -command {destroy .road2
}
3639 pack append .road2 .road2.z
{top expand fill
}
3640 pack append .road2 .road2.b
{top
}
3641 .road2.z.t configure
-state disabled
3642 .road2.z.t yview
-pickplace 1.0
3649 catch {destroy .road3
}
3652 wm title .road3
"Reducing Complexity"
3653 wm iconname .road3
"CompHelp"
3655 scrollbar .road3.z.s
-command ".road3.z.t yview"
3656 text .road3.z.t
-relief raised
-bd 2 \
3657 -background $BG -foreground $FG \
3658 -yscrollcommand ".road3.z.s set" \
3659 -setgrid 1 -width 60 -height 30 -wrap word
3660 pack append .road3.z
\
3661 .road3.z.s
{left filly
} \
3662 .road3.z.t
{left expand fill
}
3663 .road3.z.t insert end
"
3664 When a verification cannot be completed because of\
3665 computational complexity; here are some strategies that\
3666 can be applied to combat this problem.
3668 0. Run the Slicing Algorithm (in the Run Menu) to find\
3669 potential redundancy in your model for the stated properties.
3671 1. Try to make the model more general, more abstract.\
3672 Remember that you are constructing a verification model and not\
3673 an implementation. SPIN's strength is in proving properties of\
3674 *interactions* in a distributed system (the implicit assumptions\
3675 that processes make about each other) -- it's strength is not in\
3676 proving things about local *computations*, data dependencies etc.
3678 2. Remove everything that is not directly related to the property\
3679 you are trying to prove: redundant computations, redundant data. \
3680 *Avoid counters*; avoid incrementing variables that are used for\
3681 only book-keeping purposes.
3682 The Syntax Check option will warn about the gravest offenses.
3684 3. Asynchronous channels are a significant source of complexity in\
3685 verification. Use a synchronous channel where possible. Reduce the\
3686 number of slots in asynchronous channels to a minimum (use 2, or 3\
3687 slots to get started).
3689 4. Look for processes that merely transfer messages. Consider if\
3690 you can remove processes that only copy incoming messages from\
3691 one channel into another, by letting the sender generate the\
3692 final message right away. If the intermediate process makes\
3693 choices (e.g., to delete or duplicate, etc.), let the sender\
3694 make that choice, rather than the intermediate process.
3696 5. Combine local computations into atomic, or d_step, sequences.
3698 6. Avoid leaving scratch data around in variables. You can reduce\
3699 the number of states by, for instance, resetting local variables\
3700 that are used inside atomic sequences to zero at the end of those\
3701 sequences; so that the scratch values aren't visible outside the\
3702 sequence. Alternatively: introduce some extra global 'hidden'\
3703 variables for these purposes (see the WhatsNew.html document).
3704 Use the predefined variable \"_\" as a write-only scratch variable\
3707 7. If possible to do so: combine the behavior of two processes into\
3708 a single one. Generalize behavior; focus on coordination aspects\
3709 (i.e., the interfaces between processes, rather than the local\
3710 computation inside processes).
3712 8. Try to exploit the partial order reduction strategies.\
3713 Use the xr and xs assertions (see WhatsNew.html); avoid sharing\
3714 channels between multiple receivers or multiple senders.\
3715 Avoid merging independent data-streams into a single shared channel."
3717 button .road3.b
-text "Ok" -command {destroy .road3
}
3718 pack append .road3 .road3.z
{top expand fill
}
3719 pack append .road3 .road3.b
{top
}
3720 .road3.z.t configure
-state disabled
3721 .road3.z.t yview
-pickplace 1.0
3728 catch {destroy .road5
}
3731 wm title .road5
"Spin Automata"
3732 wm iconname .road5
"FsmHelp"
3734 scrollbar .road5.z.s
-command ".road5.z.t yview"
3735 text .road5.z.t
-relief raised
-bd 2 \
3736 -background $BG -foreground $FG \
3737 -yscrollcommand ".road5.z.s set" \
3738 -setgrid 1 -width 60 -height 30 -wrap word
3739 pack append .road5.z
\
3740 .road5.z.s
{left filly
} \
3741 .road5.z.t
{left expand fill
}
3742 .road5.z.t insert end
"
3743 The Spin Automata view option give a view of the
3744 structure of the automata models that Spin uses in
3745 the verification process.
3746 Each proctype is represented by a unique automaton.
3748 Chosing this option (in the Run menu) will cause Spin to
3749 first generate a verifier, compile it, and then run it
3750 (as pan -d) to obtain a description of the proctype
3751 names and the corresponding automata.
3753 After selecting (double-clicking) the proctype name desired,
3754 the graph will be produced. The default graph layout
3755 algorithm is small and a self-contained part of Xspin,
3756 but also rather crude. Be on guard, therefore, for edges
3757 that overlap (a typical case, for instance, is a backedge
3758 that hides behind a series of forward edges. Use DOT
3759 (see the README.html file on Spin) when possible for much
3760 better graph layout.
3762 In the default layout, the following button actions are
3763 defined (the first one is not needed when using DOT):
3765 1. Moving Nodes: either Button-1 or Button-2.
3766 2. Displaying Edge Labels: hold Button-1 down on the edge.
3767 3. Cross-References: Move the cursor over a Node to see the
3768 corresponding line in the Promela source, in the main
3771 If labels look bad -- try changing the font definitions at
3772 the start of the xspin.tcl file (hints are given there).
3774 button .road5.b
-text "Ok" -command {destroy .road5
}
3775 pack append .road5 .road5.z
{top expand fill
}
3776 pack append .road5 .road5.b
{top
}
3777 .road5.z.t configure
-state disabled
3778 .road5.z.t yview
-pickplace 1.0
3785 catch {destroy .road6
}
3788 wm title .road6
"Optional Compiler Directives"
3789 wm iconname .road6
"Optional"
3791 scrollbar .road6.z.s
-command ".road6.z.t yview"
3792 text .road6.z.t
-relief raised
-bd 2 \
3793 -background $BG -foreground $FG \
3794 -yscrollcommand ".road6.z.s set" \
3795 -setgrid 1 -width 80 -height 30 -wrap word
3796 pack append .road6.z
\
3797 .road6.z.s
{left filly
} \
3798 .road6.z.t
{left expand fill
}
3799 .road6.z.t insert end
"
3800 Use only when prompted:
3802 NFAIR=N size memory used for enforcing weak fairness (default N=2)
3803 VECTORSZ=N allocates memory (in bytes) for state vector (default N=1024)
3805 Related to partial order reduction:
3807 CTL limit p.o.reduction to subset consistent with branching time logic
3808 GLOB_ALPHA consider process death a global action
3809 XUSAFE disable validity checks of xr/xs assertions
3813 NOBOUNDCHECK don't check array bound violations
3814 NOCOMP don't compress states with fullstate storage (uses more memory)
3815 NOSTUTTER disable stuttering rules (warning: changes semantics)
3817 Memory saving (slower):
3819 MA=N use a minimized DFA encoding for state vectors up to N bytes
3823 BCOMP when in BITSTATE mode, computes hash over compressed state-vector
3824 NIBIS apply a small optimization of partial order reduction
3825 NOVSZ risky - removes 4 bytes from state vector - its length field.
3826 PRINTF enables printfs during verification runs
3827 RANDSTORE=N in BITSTATE mode, -DRANDSTORE=33 lowers prob of storing a state to 33%
3828 W_XPT=N with MA, write checkpoint files every multiple of N states stored
3829 R_XPT with MA, restart run from last checkpoint file written
3833 SDUMP with CHECK: adds ascii dumps of state vectors
3834 SVDUMP add run option -pN to write N-byte state vectors into file sv_dump
3836 Already set by the other xspin options:
3838 BITSTATE use supertrace/bitstate instead of exhaustive exploration
3839 HC use hash-compact instead of exhaustive exploration
3840 COLLAPSE collapses state vector size by up to 80% to 90%
3841 MEMCNT=N set upperbound of 2^N bytes to memory that can be allocated
3842 MEMLIM=N set upperbound of N Mbytes to memory that can be allocated
3843 NOCLAIM exclude never claim from the verification, if present
3844 NOFAIR disable the code for weak-fairness (is faster)
3845 NOREDUCE disables the partial order reduction algorithm
3846 NP enable non-progress cycle detection (option -l, replacing -a),
3847 PEG add complexity profiling (transition counts)
3848 REACH guarantee absence of errors within the -m depth-limit
3849 SAFETY optimize for the case where no cycle detection is needed
3850 VAR_RANGES compute the effective value range of byte variables
3851 CHECK generate debugging information (see also below)
3852 VERBOSE elaborate debugging printouts
3854 button .road6.b
-text "Ok" -command {destroy .road6
}
3855 pack append .road6 .road6.z
{top expand fill
}
3856 pack append .road6 .road6.b
{top
}
3857 .road6.z.t configure
-state disabled
3858 .road6.z.t yview
-pickplace 1.0
3863 # simulation options panel
3870 set Blue
"blue"; #"yellow"
3871 set Yellow
"yellow"; #"red"
3872 set White
"white"; #"yellow"
3873 set Red
"red"; #"yellow"
3874 set Green
"green"; #"green"
3900 set PlaceSim
"+200+100"
3902 proc simulation_old
{} {
3903 global s_typ l_typ showvars qv PlaceSim
3904 global fvars gvars lvars SparseMsc HelvBig
3905 global msc ebc tsc vv svars rvars seed jumpsteps
3906 global hide_q1 hide_q2 hide_q3
3908 catch { .
menu.run.m entryconfigure
5 -state normal
}
3912 set k
[string first
"\+" $PlaceSim]
3914 set PlaceSim
[string range
$PlaceSim $k end
]
3917 wm title .s
"Simulation Options"
3918 wm iconname .s
"SIM"
3919 wm geometry .s
$PlaceSim
3921 frame .s.opt
-relief flat
3925 frame .s.opt.mode
-relief raised
-borderwidth 1m
3926 label .s.opt.mode.fld0
\
3928 -text "Display Mode" \
3929 -relief sunken
-borderwidth 1m
3931 checkbutton .s.opt.mode.fld4b
-text "Time Sequence Panel - with:" \
3934 frame .s.opt.mode.flds
3935 radiobutton .s.opt.mode.flds.fld3
\
3936 -text " Interleaved Steps" \
3937 -variable m_typ
-value 2 \
3939 radiobutton .s.opt.mode.flds.fld1
\
3940 -text " One Window per Process" \
3941 -variable m_typ
-value 0 \
3943 radiobutton .s.opt.mode.flds.fld2
\
3944 -text " One Trace per Process" \
3945 -variable m_typ
-value 1 \
3947 frame .s.opt.mode.flds.fld0
-width 15
3948 pack append .s.opt.mode.flds
\
3949 .s.opt.mode.flds.fld0
{left
frame w
}\
3950 .s.opt.mode.flds.fld3
{top
frame w
}\
3951 .s.opt.mode.flds.fld1
{top
frame w
}\
3952 .s.opt.mode.flds.fld2
{top
frame w
}
3954 checkbutton .s.opt.mode.fld4a
-text "MSC Panel - with:" \
3957 frame .s.opt.mode.steps
3958 radiobutton .s.opt.mode.steps.fld5
-text " Step Number Labels" \
3959 -variable SYMBOLIC
-value 0 \
3961 radiobutton .s.opt.mode.steps.fld6
-text " Source Text Labels" \
3962 -variable SYMBOLIC
-value 1 \
3964 radiobutton .s.opt.mode.steps.fld7
-text " Normal Spacing" \
3965 -variable SparseMsc
-value 1 \
3967 radiobutton .s.opt.mode.steps.fld8
-text " Condensed Spacing" \
3968 -variable SparseMsc
-value 0 \
3970 frame .s.opt.mode.steps.fld0
-width 15
3971 pack append .s.opt.mode.steps
\
3972 .s.opt.mode.steps.fld0
{left
frame w
}\
3973 .s.opt.mode.steps.fld5
{top
frame w
}\
3974 .s.opt.mode.steps.fld6
{top
frame w
}\
3975 .s.opt.mode.steps.fld7
{top
frame w
}\
3976 .s.opt.mode.steps.fld8
{top
frame w
}
3978 checkbutton .s.opt.mode.fld4c
-text "Execution Bar Panel" \
3981 checkbutton .s.opt.mode.fld4d
-text "Data Values Panel" \
3985 frame .s.opt.mode.vars
3987 checkbutton .s.opt.mode.vars.fld4c
-text " Track Buffered Channels" \
3990 checkbutton .s.opt.mode.vars.fld4d
-text " Track Global Variables" \
3993 checkbutton .s.opt.mode.vars.fld4e
-text " Track Local Variables" \
3997 checkbutton .s.opt.mode.vars.fld4f
\
3998 -text " Display vars marked 'show' in MSC" \
3999 -variable showvars
\
4001 frame .s.opt.mode.vars.fld0
-width 15
4002 pack append .s.opt.mode.vars
\
4003 .s.opt.mode.vars.fld0
{left
frame w
}\
4004 .s.opt.mode.vars.fld4c
{top
frame w
}\
4005 .s.opt.mode.vars.fld4d
{top
frame w
}\
4006 .s.opt.mode.vars.fld4e
{top
frame w
}\
4007 .s.opt.mode.vars.fld4f
{top
frame w
}
4009 pack append .s.opt.mode .s.opt.mode.fld0
{top pady
4 frame w fillx
}
4011 pack append .s.opt.mode .s.opt.mode.fld4a
{top pady
4 frame w
}
4012 pack append .s.opt.mode .s.opt.mode.steps
{top
frame w
}
4014 pack append .s.opt.mode .s.opt.mode.fld4b
{top pady
4 frame w
}
4015 pack append .s.opt.mode .s.opt.mode.flds
{top
frame w
}
4017 pack append .s.opt.mode .s.opt.mode.fld4d
{top pady
4 frame w
}
4018 pack append .s.opt.mode .s.opt.mode.vars
{top
frame w
}
4020 pack append .s.opt.mode .s.opt.mode.fld4c
{top pady
4 frame w
}
4022 pack append .s.opt .s.opt.mode
{left
frame n
}
4024 frame .s.opt.mesg
-relief raised
-borderwidth 1m
4025 label .s.opt.mesg.loss0
\
4027 -text "A Full Queue" \
4028 -relief sunken
-borderwidth 1m
4029 radiobutton .s.opt.mesg.loss1
-text "Blocks New Msgs" \
4030 -variable l_typ
-value 0 \
4032 radiobutton .s.opt.mesg.loss2
-text "Loses New Msgs" \
4033 -variable l_typ
-value 1 \
4035 pack append .s.opt.mesg .s.opt.mesg.loss0
{top pady
4 frame w fillx
}
4036 pack append .s.opt.mesg .s.opt.mesg.loss1
{top pady
4 frame w
}
4037 pack append .s.opt.mesg .s.opt.mesg.loss2
{top pady
4 frame w
}
4039 frame .s.opt.hide
-relief raised
-borderwidth 1m
4040 label .s.opt.hide.txt
\
4042 -text "Hide Queues in MSC" \
4043 -relief sunken
-borderwidth 1m
4044 pack append .s.opt.hide .s.opt.hide.txt
{top pady
4 frame w fillx
}
4046 for {set i
1} {$i < 4} {incr i
} {
4047 frame .s.opt.hide.q
$i
4048 label .s.opt.hide.q
$i.qno
\
4051 entry .s.opt.hide.q
$i.
entry \
4052 -relief sunken
-width 8
4053 pack append .s.opt.hide.q
$i .s.opt.hide.q
$i.qno
{left pady
4 frame n
}
4054 pack append .s.opt.hide.q
$i .s.opt.hide.q
$i.
entry {left pady
4 frame n
}
4055 pack append .s.opt.hide .s.opt.hide.q
$i {top pady
4 frame w fillx
}
4057 frame .s.opt.lframe
-relief raised
-borderwidth 1m
4058 label .s.opt.lframe.tl
\
4060 -text "Simulation Style" \
4061 -relief sunken
-borderwidth 1m
4062 radiobutton .s.opt.lframe.is
-text "Interactive" \
4063 -variable s_typ
-value 2 \
4065 radiobutton .s.opt.lframe.gs
-text "Guided (using pan.trail)" \
4066 -variable s_typ
-value 1 \
4068 frame .s.opt.lframe.b
4069 entry .s.opt.lframe.b.
entry -relief sunken
-width 8
4070 label .s.opt.lframe.b.
label \
4072 -text "Steps Skipped"
4073 pack append .s.opt.lframe.b
\
4074 .s.opt.lframe.b.
label {left
} \
4075 .s.opt.lframe.b.
entry {left
}
4077 radiobutton .s.opt.lframe.rs
-text "Random (using seed)" \
4078 -variable s_typ
-value 0 \
4080 frame .s.opt.lframe.s
4081 entry .s.opt.lframe.s.
entry -relief sunken
-width 8
4082 label .s.opt.lframe.s.
label \
4085 pack append .s.opt.lframe.s
\
4086 .s.opt.lframe.s.
label {left
} \
4087 .s.opt.lframe.s.
entry {left
}
4089 pack append .s.opt.lframe .s.opt.lframe.tl
{top pady
4 frame w fillx
} \
4090 .s.opt.lframe.rs
{top pady
4 frame w
} \
4091 .s.opt.lframe.s
{top pady
4 frame e
} \
4092 .s.opt.lframe.gs
{top pady
4 frame w
} \
4093 .s.opt.lframe.b
{top pady
4 frame e
} \
4094 .s.opt.lframe.is
{top pady
4 frame w
}
4096 pack append .s.opt .s.opt.lframe
{top
frame n
}
4097 pack append .s.opt .s.opt.mesg
{top
frame n fillx
}
4098 pack append .s.opt .s.opt.hide
{top
frame n expand fillx filly
}
4100 pack append .s .s.opt
{ top
frame n
}
4102 pack append .s
[button .s.rewind
-text "Start" \
4103 -command "Rewind" ] {right
frame e
}
4104 pack append .s
[button .s.
exit -text "Cancel" \
4105 -command "Stopsim" ] {right
frame e
}
4106 pack append .s
[button .s.help
-text "Help" -fg red
\
4107 -command "roadmap1" ] {right
frame e
}
4109 .s.opt.lframe.s.
entry insert end
$seed
4110 .s.opt.lframe.b.
entry insert end
$jumpsteps
4112 .s.opt.hide.q1.
entry insert end
$hide_q1
4113 .s.opt.hide.q2.
entry insert end
$hide_q2
4114 .s.opt.hide.q3.
entry insert end
$hide_q3
4120 proc simulation
{} {
4121 global s_typ l_typ showvars qv PlaceSim
4122 global fvars gvars lvars SparseMsc HelvBig
4123 global msc ebc tsc vv svars rvars seed jumpsteps
4124 global hide_q1 hide_q2 hide_q3
4127 catch { .
menu.run.m entryconfigure
5 -state normal
}
4131 catch {rmfile pan_in9999999.trail
}
4132 debug
{about to remove pan_in9999999.trail
}
4133 rmfile pan_in9999999.trail
4134 set k
[string first
"\+" $PlaceSim]
4136 set PlaceSim
[string range
$PlaceSim $k end
]
4139 wm title .s
"Simulation Options"
4140 wm iconname .s
"SIM"
4141 wm geometry .s
$PlaceSim
4145 # lower frame with 'start', 'cancel' and 'help' buttons
4146 frame .s.l
-relief flat
4147 pack .s.l
-side bottom
-fill both
4149 pack [button .s.l.rewind
-text " Start " \
4150 -command "Rewind" ] -side right
-fill y
-padx 4
4151 pack [button .s.l.
exit -text "Cancel" \
4154 catch {rmfile pan_in9999999.trail}
4156 ] -side right
-fill y
-padx 4
4157 pack [button .s.l.help
-text " Help " -fg red
\
4158 -command "roadmap1" ] -side right
-fill y
-padx 4
4160 # upper frame with modes and options
4161 frame .s.u
-relief flat
4162 pack .s.u
-side top
-fill both
4164 frame .s.u.mode
-relief raised
-borderwidth 1m
4165 pack .s.u.mode
-side left
-fill both
-expand 1
4167 frame .s.u.mode.fdis
-relief flat
4168 pack .s.u.mode.fdis
-side top
-fill x
-expand 1
4170 label .s.u.mode.fdis.fld0
\
4172 -text "Display Mode" \
4173 -relief sunken
-borderwidth 1m
4174 pack .s.u.mode.fdis.fld0
-side top
-fill x
4178 frame .s.u.mode.fmsc
-relief flat
4179 pack .s.u.mode.fmsc
-side top
-fill x
4181 checkbutton .s.u.mode.fmsc.fld4a
-text "MSC Panel - with:" \
4184 pack .s.u.mode.fmsc.fld4a
-side left
4186 frame .s.u.mode.msc
-relief flat
4187 pack .s.u.mode.msc
-side top
-fill x
4189 frame .s.u.mode.msc.lab
-relief flat
4190 pack .s.u.mode.msc.lab
-side top
-fill x
4192 frame .s.u.mode.msc.lab.dummy
-width 18 -relief flat
4193 pack .s.u.mode.msc.lab.dummy
-side left
-fill y
4195 frame .s.u.mode.msc.lab.radios
-relief flat
4196 pack .s.u.mode.msc.lab.radios
-side left
-fill x
4198 frame .s.u.mode.msc.lab.radios.fnum
-relief flat
4199 pack .s.u.mode.msc.lab.radios.fnum
-side top
-fill x
4201 radiobutton .s.u.mode.msc.lab.radios.fnum.fld5
\
4202 -text " Step Number Labels" \
4203 -variable SYMBOLIC
-value 0 \
4205 pack .s.u.mode.msc.lab.radios.fnum.fld5
-side left
4207 frame .s.u.mode.msc.lab.radios.ftext
-relief flat
4208 pack .s.u.mode.msc.lab.radios.ftext
-side top
-fill x
4210 radiobutton .s.u.mode.msc.lab.radios.ftext.fld6
\
4211 -text " Source Text Labels" \
4212 -variable SYMBOLIC
-value 1 \
4214 pack .s.u.mode.msc.lab.radios.ftext.fld6
-side left
4216 frame .s.u.mode.msc.lab.bracket
4217 pack .s.u.mode.msc.lab.bracket
-side left
-fill y
4219 canvas .s.u.mode.msc.lab.bracket.c
-width 10 -height 40
4220 pack .s.u.mode.msc.lab.bracket.c
-side top
4221 .s.u.mode.msc.lab.bracket.c create line
5 15 10 15 10 38 5 38
4223 frame .s.u.mode.msc.space
-relief flat
4224 pack .s.u.mode.msc.space
-side top
-fill x
4226 frame .s.u.mode.msc.space.dummy
-width 18 -relief flat
4227 pack .s.u.mode.msc.space.dummy
-side left
-fill y
4229 frame .s.u.mode.msc.space.radios
-relief flat
4230 pack .s.u.mode.msc.space.radios
-side left
-fill x
4232 frame .s.u.mode.msc.space.radios.fnorm
-relief flat
4233 pack .s.u.mode.msc.space.radios.fnorm
-side top
-fill x
4235 radiobutton .s.u.mode.msc.space.radios.fnorm.fld7
\
4236 -text " Normal Spacing" \
4237 -variable SparseMsc
-value 1 \
4239 pack .s.u.mode.msc.space.radios.fnorm.fld7
-side left
4241 frame .s.u.mode.msc.space.radios.fcond
-relief flat
4242 pack .s.u.mode.msc.space.radios.fcond
-side top
-fill x
4244 radiobutton .s.u.mode.msc.space.radios.fcond.fld8
\
4245 -text " Condensed Spacing" \
4246 -variable SparseMsc
-value 0 \
4248 pack .s.u.mode.msc.space.radios.fcond.fld8
-side left
4250 frame .s.u.mode.msc.space.bracket
4251 pack .s.u.mode.msc.space.bracket
-side left
-fill y
4253 canvas .s.u.mode.msc.space.bracket.c
-width 10 -height 40
4254 pack .s.u.mode.msc.space.bracket.c
-side top
4255 .s.u.mode.msc.space.bracket.c create line
5 15 10 15 10 38 5 38
4257 # Time Sequence Panel
4259 frame .s.u.mode.ftsp
-relief flat
4260 pack .s.u.mode.ftsp
-side top
-fill x
4262 checkbutton .s.u.mode.ftsp.fld4b
\
4263 -text "Time Sequence Panel - with:" \
4266 pack .s.u.mode.ftsp.fld4b
-side left
4269 pack .s.u.mode.tsp
-side top
-fill x
4271 frame .s.u.mode.tsp.
proc
4272 pack .s.u.mode.tsp.
proc -side top
-fill x
4274 frame .s.u.mode.tsp.
proc.dummy
-width 18
4275 pack .s.u.mode.tsp.
proc.dummy
-side left
-fill y
4277 frame .s.u.mode.tsp.
proc.radios
-relief flat
4278 pack .s.u.mode.tsp.
proc.radios
-side left
-fill y
4280 frame .s.u.mode.tsp.
proc.radios.is
4281 pack .s.u.mode.tsp.
proc.radios.is
-side top
-fill x
4283 radiobutton .s.u.mode.tsp.
proc.radios.is.fld3
\
4284 -text " Interleaved Steps" \
4285 -variable m_typ
-value 2 \
4287 pack .s.u.mode.tsp.
proc.radios.is.fld3
-side left
4289 frame .s.u.mode.tsp.
proc.radios
.1win
-relief flat
4290 pack .s.u.mode.tsp.
proc.radios
.1win
-side top
-fill x
4292 radiobutton .s.u.mode.tsp.
proc.radios
.1win.fld1
\
4293 -text " One Window per Process" \
4294 -variable m_typ
-value 0 \
4296 pack .s.u.mode.tsp.
proc.radios
.1win.fld1
-side left
4298 frame .s.u.mode.tsp.
proc.radios
.1trace -relief flat
4299 pack .s.u.mode.tsp.
proc.radios
.1trace -side top
-fill x
4301 radiobutton .s.u.mode.tsp.
proc.radios
.1trace.fld2
\
4302 -text " One Trace per Process" \
4303 -variable m_typ
-value 1 \
4305 pack .s.u.mode.tsp.
proc.radios
.1trace.fld2
-side left
4307 frame .s.u.mode.tsp.
proc.bracket
4308 pack .s.u.mode.tsp.
proc.bracket
-side left
-fill y
4311 canvas .s.u.mode.tsp.
proc.bracket.c
-width 10 -height 66
4312 pack .s.u.mode.tsp.
proc.bracket.c
-side top
4313 .s.u.mode.tsp.
proc.bracket.c create line
5 [expr 0 + $y] \
4321 frame .s.u.mode.fdvp
-relief flat
4322 pack .s.u.mode.fdvp
-side top
-fill x
4324 checkbutton .s.u.mode.fdvp.fld4d
-text "Data Values Panel" \
4327 pack .s.u.mode.fdvp.fld4d
-side left
4329 frame .s.u.mode.vars
4330 pack .s.u.mode.vars
-side top
-fill x
4332 frame .s.u.mode.vars.dummy
-width 18
4333 pack .s.u.mode.vars.dummy
-side left
-fill y
4335 frame .s.u.mode.vars.chks
-relief flat
4336 pack .s.u.mode.vars.chks
-side left
-fill y
4338 frame .s.u.mode.vars.chks.ftbc
4339 pack .s.u.mode.vars.chks.ftbc
-side top
-fill x
4341 checkbutton .s.u.mode.vars.chks.ftbc.fld4c
-text " Track Buffered Channels" \
4344 pack .s.u.mode.vars.chks.ftbc.fld4c
-side left
4346 frame .s.u.mode.vars.chks.ftgv
4347 pack .s.u.mode.vars.chks.ftgv
-side top
-fill x
4349 checkbutton .s.u.mode.vars.chks.ftgv.fld4d
-text " Track Global Variables" \
4352 pack .s.u.mode.vars.chks.ftgv.fld4d
-side left
4354 frame .s.u.mode.vars.chks.ftlv
4355 pack .s.u.mode.vars.chks.ftlv
-side top
-fill x
4357 checkbutton .s.u.mode.vars.chks.ftlv.fld4e
-text " Track Local Variables" \
4360 pack .s.u.mode.vars.chks.ftlv.fld4e
-side left
4362 frame .s.u.mode.vars.chks.fshow
4363 pack .s.u.mode.vars.chks.fshow
-side top
-fill x
4365 checkbutton .s.u.mode.vars.chks.fshow.fld4f
\
4366 -text " Display vars marked 'show' in MSC" \
4367 -variable showvars
\
4370 pack .s.u.mode.vars.chks.fshow.fld4f
-side left
4372 frame .s.u.mode.fexecbar
-relief flat
4373 pack .s.u.mode.fexecbar
-side top
-fill x
4375 checkbutton .s.u.mode.fexecbar.fld4c
-text "Execution Bar Panel" \
4378 pack .s.u.mode.fexecbar.fld4c
-side left
4381 frame .s.u.r
-relief flat
4382 pack .s.u.r
-side right
-fill y
-expand 1
4385 frame .s.u.r.sim
-relief raised
-borderwidth 1m
4386 pack .s.u.r.sim
-side top
-fill both
-expand 1
4388 frame .s.u.r.sim.flab
-relief sunken
4389 pack .s.u.r.sim.flab
-side top
-fill x
4391 label .s.u.r.sim.flab.tl
\
4393 -text "Simulation Style" \
4394 -relief sunken
-borderwidth 1m
4395 pack .s.u.r.sim.flab.tl
-side top
-fill x
4397 frame .s.u.r.sim.random
4398 pack .s.u.r.sim.random
-side top
-fill x
4400 radiobutton .s.u.r.sim.random.rs
-text "Random (using seed)" \
4401 -variable s_typ
-value 0 \
4403 -command "enable_disable_sub_buttons"
4404 pack .s.u.r.sim.random.rs
-side left
4406 frame .s.u.r.sim.seedvalue
4407 pack .s.u.r.sim.seedvalue
-side top
-fill x
4409 frame .s.u.r.sim.seedvalue.dummy
-width 18
4410 pack .s.u.r.sim.seedvalue.dummy
-side left
-fill y
4412 label .s.u.r.sim.seedvalue.
label \
4415 pack .s.u.r.sim.seedvalue.
label -side left
4417 entry .s.u.r.sim.seedvalue.
entry -relief sunken
-width 8
4418 pack .s.u.r.sim.seedvalue.
entry -side left
4420 frame .s.u.r.sim.guided
4421 pack .s.u.r.sim.guided
-side top
-fill x
4423 radiobutton .s.u.r.sim.guided.gs
-text "Guided" \
4424 -variable s_typ
-value 1 \
4426 -command "enable_disable_sub_buttons"
4427 pack .s.u.r.sim.guided.gs
-side left
4429 frame .s.u.r.sim.guided_type
4430 pack .s.u.r.sim.guided_type
-side top
-fill x
4432 frame .s.u.r.sim.guided_type.dummy
-width 18
4433 pack .s.u.r.sim.guided_type.dummy
-side left
-fill y
4435 frame .s.u.r.sim.guided_type.radios
4436 pack .s.u.r.sim.guided_type.radios
-side left
4438 frame .s.u.r.sim.guided_type.radios.pan_trail
4439 pack .s.u.r.sim.guided_type.radios.pan_trail
-side top
-fill x
4441 radiobutton .s.u.r.sim.guided_type.radios.pan_trail.rb
\
4442 -text "Using pan_in.trail" \
4443 -variable whichsim
-value 0 \
4445 pack .s.u.r.sim.guided_type.radios.pan_trail.rb
-side left
4447 frame .s.u.r.sim.guided_type.radios.trail_other
4448 pack .s.u.r.sim.guided_type.radios.trail_other
-side top
-fill x
4450 radiobutton .s.u.r.sim.guided_type.radios.trail_other.rb
\
4452 -variable whichsim
-value 1 \
4454 pack .s.u.r.sim.guided_type.radios.trail_other.rb
-side left
4456 entry .s.u.r.sim.guided_type.radios.trail_other.
entry \
4458 pack .s.u.r.sim.guided_type.radios.trail_other.
entry -side left
4460 button .s.u.r.sim.guided_type.radios.trail_other.
button -text "Browse" \
4461 -command select_trail_file
4462 pack .s.u.r.sim.guided_type.radios.trail_other.
button -side left
4464 frame .s.u.r.sim.skipstep
4465 pack .s.u.r.sim.skipstep
-side top
-fill x
4467 label .s.u.r.sim.skipstep.
label \
4469 -text "Steps Skipped"
4470 pack .s.u.r.sim.skipstep.
label -side left
4472 entry .s.u.r.sim.skipstep.
entry -relief sunken
-width 8
4473 pack .s.u.r.sim.skipstep.
entry -side left
4475 frame .s.u.r.sim.interactive
4476 pack .s.u.r.sim.interactive
-side top
-fill x
4478 radiobutton .s.u.r.sim.interactive.is
-text "Interactive" \
4479 -variable s_typ
-value 2 \
4481 -command "enable_disable_sub_buttons"
4482 pack .s.u.r.sim.interactive.is
-side left
4485 frame .s.u.r.fq
-relief raised
-borderwidth 1m
4486 pack .s.u.r.fq
-side top
-fill both
-expand 1
4488 frame .s.u.r.fq.
label -relief sunken
4489 pack .s.u.r.fq.
label -side top
-fill x
4491 label .s.u.r.fq.
label.loss0
\
4493 -text "A Full Queue" \
4494 -relief sunken
-borderwidth 1m
4495 pack .s.u.r.fq.
label.loss0
-side top
-fill x
4497 frame .s.u.r.fq.block
4498 pack .s.u.r.fq.block
-side top
-fill x
4500 radiobutton .s.u.r.fq.block.loss1
-text "Blocks New Msgs" \
4501 -variable l_typ
-value 0 \
4503 pack .s.u.r.fq.block.loss1
-side left
4505 frame .s.u.r.fq.lose
4506 pack .s.u.r.fq.lose
-side top
-fill x
4508 radiobutton .s.u.r.fq.lose.loss2
-text "Loses New Msgs" \
4509 -variable l_typ
-value 1 \
4511 pack .s.u.r.fq.lose.loss2
-side left
4514 frame .s.u.r.hq
-relief raised
-borderwidth 1m
4515 pack .s.u.r.hq
-side top
-fill both
-expand 1
4517 frame .s.u.r.hq.flabel
-relief sunken
4518 pack .s.u.r.hq.flabel
-side top
-fill x
4520 label .s.u.r.hq.flabel.txt
\
4522 -text "Hide Queues in MSC" \
4523 -relief sunken
-borderwidth 1m
4524 pack .s.u.r.hq.flabel.txt
-side top
-fill x
4526 for {set i
1} {$i < 4} {incr i
} {
4528 pack .s.u.r.hq.q
$i -side top
-fill x
4529 label .s.u.r.hq.q
$i.qno
\
4532 pack .s.u.r.hq.q
$i.qno
-side left
4533 entry .s.u.r.hq.q
$i.
entry \
4534 -relief sunken
-width 8
4535 pack .s.u.r.hq.q
$i.
entry -side left
4538 .s.u.r.sim.seedvalue.
entry insert end
$seed
4539 .s.u.r.sim.skipstep.
entry insert end
$jumpsteps
4541 .s.u.r.hq.q1.
entry insert end
$hide_q1
4542 .s.u.r.hq.q2.
entry insert end
$hide_q2
4543 .s.u.r.hq.q3.
entry insert end
$hide_q3
4544 enable_disable_sub_buttons
4546 tkwait visibility .s
4550 proc enable_disable_sub_buttons
{} {
4552 switch -regexp $s_typ {
4553 0|
2 { .s.u.r.sim.guided_type.radios.pan_trail.rb configure
-state disabled
4554 .s.u.r.sim.guided_type.radios.trail_other.rb configure
-state disabled
4555 .s.u.r.sim.guided_type.radios.trail_other.
button configure
-state disabled
4557 1 { .s.u.r.sim.guided_type.radios.pan_trail.rb configure
-state normal
4558 .s.u.r.sim.guided_type.radios.trail_other.rb configure
-state normal
4559 .s.u.r.sim.guided_type.radios.trail_other.
button configure
-state normal
4560 .s.u.r.sim.guided_type.radios.pan_trail.rb select
4566 proc select_trail_file
{} {
4567 global Trail_filename
4568 .s.u.r.sim.guided_type.radios.trail_other.rb select
4569 # try to use the predefined file selection dialog
4570 switch [info commands
tk_getOpenFile] "" {
4571 # some old version of Tk so use our own file selection dialog
4572 set fileselect
"FileSelect open"
4574 set fileselect
"tk_getOpenFile"
4577 # get the file (return if the file selection dialog canceled)
4578 switch -- [set file [eval $fileselect -initialdir { { $init_dir } } ]] "" return
4579 .s.u.r.sim.guided_type.radios.trail_other.
entry insert end
$file
4584 proc bld_s_options
{} {
4585 global fvars gvars lvars svars qv
4586 global rvars l_typ showvars vv
4587 global s_typ seed jumpsteps s_options
4588 global hide_q1 hide_q2 hide_q3 ival whichsim trail_file trail_num
4590 set s_options
"-X -p -v $ival(5)"
4592 if {$showvars && $gvars == 0 && $lvars == 0} {
4593 catch { tk_messageBox -icon info \
4594 -message "Display variables marked 'show' selected, \
4595 but no local or global vars are being tracked"
4597 if {$showvars==1} { set s_options
[format "%s -Y" $s_options] }
4598 if {$s_typ==2} { set s_options
[format "%s -i" $s_options] }
4599 if {$vv && $gvars} { set s_options
[format "%s -g" $s_options] }
4600 if {$vv && $lvars} { set s_options
[format "%s -l" $s_options] }
4601 if {$svars} { set s_options
[format "%s -s" $s_options] }
4602 if {$rvars} { set s_options
[format "%s -r" $s_options] }
4603 if {$l_typ} { set s_options
[format "%s -m" $s_options] }
4604 if {$hide_q1 != ""} { set s_options
[format "%s -q%s" $s_options $hide_q1] }
4605 if {$hide_q2 != ""} { set s_options
[format "%s -q%s" $s_options $hide_q2] }
4606 if {$hide_q3 != ""} { set s_options
[format "%s -q%s" $s_options $hide_q3] }
4607 if {$s_typ==1} then
{
4610 if {$whichsim == 1} {
4611 #using user specified file
4612 if ![file exists
$trail_file] {
4613 catch { tk_messageBox -icon info \
4614 -message "Trail file $trail_file does not exist."
4618 # see if file is in current directory. if not, copy to
4619 # pan_in9999999.trail in current directory
4620 set ind
[string last
"\/" $trail_file]
4622 if {[pwd] != [string range
$trail_file 0 [expr $ind - 1]]} {
4623 cpfile
$trail_file pan_in9999999.trail
4624 set trail_file
"pan_in9999999.trail"
4627 set trail_file
[string range
$trail_file \
4629 [expr [string length
$trail_file] - 1]]
4632 #see if it's a 'pan_in<#>.trail' file
4633 set is_pan_in_trail_file
0
4634 if {[string range
$trail_file 0 5] == "pan_in"} {
4635 set l
[string length
$trail_file]
4637 if {[string range
$trail_file \
4638 [expr $l-6] [expr $l-1]] == ".trail"} {
4639 set num
[string range
$trail_file 6 [expr $l-7]]
4640 if [string is integer
$num] {
4642 set is_pan_in_trail_file
1
4644 if !($is_pan_in_trail_file) {
4645 # not a 'pan_in<#>.trail' file - copy file to pan_in9999999.trail
4646 # in current directory
4647 cpfile
$trail_file pan_in9999999.trail
4648 if [file exists pan_in9999999.trail
] {
4649 set trail_num
9999999
4651 catch {tk_messageBox -icon info \
4652 -message "Unable to create input file in $pwd \
4653 check write permissions."
4659 if {![file exists pan_in.trail
] && ![file exists pan_in.tra
]} {
4660 catch { tk_messageBox -icon info \
4661 -message "Trail file \'pan_in.tra(il)\' does not exist."
4667 set s_options
[format "%s -t%s" $s_options $trail_num]
4669 if {[string length
$seed] > 0} {
4670 set s_options
[format "%s -n%s" $s_options $seed]
4672 if {$s_typ!=2} then
{
4673 if {[string length
$jumpsteps] > 0} {
4674 set s_options
[format "%s -j%s" $s_options $jumpsteps]
4680 global stop dbox2 Sticky PlaceSim PlaceCanvas
4681 global stepper stepped howmany fd
4686 add_log
"<stop simulation>"
4687 if {[winfo exists .s
]} {
4688 set PlaceSim
[wm geometry .s
]
4691 catch {set howmany
0}
4693 catch { if {$Sticky($dbox2) == 0} {
4694 set PlaceCanvas
(msc
) [wm geometry .f
$dbox2]
4705 global stepper stepped sbox simruns PlaceSim
4709 if {$simruns == 0} {
4710 if {[winfo exists .s
]} {
4711 set PlaceSim
[wm geometry .s
]
4716 catch { .c
$sbox.run configure
\
4717 -text "Run" -command "Runsim" }
4722 global Depth s_typ whichsim trail_file
4724 global seed jumpsteps simruns
4725 global hide_q1 hide_q2 hide_q3 trail_file
4727 catch { set jumpsteps
[.s.u.r.sim.skipstep.
entry get
] }
4728 catch { set hide_q1
[.s.u.r.hq.q1.
entry get
] }
4729 catch { set hide_q2
[.s.u.r.hq.q2.
entry get
] }
4730 catch { set hide_q3
[.s.u.r.hq.q3.
entry get
] }
4733 catch { set seed
[.s.u.r.sim.seedvalue.
entry get
] }
4739 foreach el
[array names Spbox
] {
4740 set Sdbox
$Spbox($el)
4741 .c
$Sdbox.z.t tag remove Rev
1.0 end
4743 if {$whichsim == 1} {
4745 catch {set trail_file
[.s.u.r.sim.guided_type.radios.trail_other.
entry get
]}
4755 global stepper stepped sbox
4757 catch { .c
$sbox.run configure
\
4758 -text "Suspend" -command "Step_forw" }
4763 proc BreakPoint
{} {
4767 catch { .c
$sbox.run configure
\
4768 -text "BreakPoint" -command "Runsim" }
4772 global Unix SPIN tk_major
4773 global s_options s_typ dbox2
4774 global stepper stepped
4775 global simruns m_typ
4777 global fd stop Depth Seq
4778 global Sdbox Spbox pbox howmany Choice
4779 global sbox VERBOSE SYMBOLIC msc ebc vv tsc
4780 global Blue Yellow White Red Green
4781 global SmallFont BigFont Sticky SparseMsc
4782 global FG BG qv gvars lvars PlaceBox
4784 global whichsim trail_num
4797 # catch { unset Spbox(0) }
4799 foreach el
[array names pbox
] {
4800 catch { destroy .c
$pbox($el) }
4801 catch { unset pbox
($el) }
4803 foreach el
[array names Spbox
] {
4804 catch { destroy .c
$Spbox($el) }
4805 catch { unset Spbox
($el) }
4808 if ![bld_s_options
] {
4812 add_log
"<starting simulation>"
4813 add_log
"$SPIN $s_options pan_in"
4815 set s_options
[format "%s pan_in" $s_options]
4819 set sbox
[mkbox
"Simulation Output" "SimOut" "sim.out" 71 11 100 100]
4821 pack append .c
$sbox [button .c
$sbox.stepf
-text "Single Step" \
4822 -command "Step_forw" ] {left
frame w
}
4823 pack append .c
$sbox [button .c
$sbox.run
-text "Run" \
4824 -command "Runsim" ] {left
frame w
}
4826 .c
$sbox.b configure
-text "Cancel" -command "Stopsim"
4840 set lastexecutable
0
4845 [mkbox
"Time Sequence" "Sequence" "seq.out" 80 10 100 325]
4849 if {[hasWord
"!!"] ||
[hasWord
"\\?\\?"]} {
4853 set maxx
[expr [winfo screenwidth .
] - 400] ;# button widths
4854 set maxh
[expr [winfo screenheight .
] - (5+120)] ;# borders+buttons
4856 [mkcanvas
"Sequence Chart" "msc" $maxx 5 1]
4857 .f
$dbox2.c configure
-height $maxh \
4858 -scrollregion "[expr -$XSZ/2] 0 \
4859 [expr $NPR*$XSZ] [expr 100+$SMX*$YSZ]"
4870 set filen
"pan_in${trail_num}.trail"
4871 if [file exists
$filen] {
4875 if {[file exists pan_in.trail
] ||
[file exists pan_in.tra
]} {
4880 catch { .c
$sbox.z.t insert end
"preparing trail, please wait..." }
4883 catch {eval exec $SPIN $s_options >&trail.out
} errmsg
4885 set errmsg
"error: no trail file for guided simulation"
4888 if {[string length
$errmsg]>0} {
4891 tk_messageBox -icon info -message $errmsg
4894 set fd
[open trail.out r
]
4895 while {[gets $fd line
] > -1} {
4901 catch { destroy .c
$sbox }
4902 catch { destroy .c
$dbox }
4907 set fd
[open trail.out r
]
4908 catch { .c
$sbox.z.t insert end
"done\n" }
4911 set fd
[open "|$SPIN $s_options" r
+]
4920 if {$ebc} { startbar
"Xspin Bar Chart" }
4930 while {$stop == 0 && [eof $fd] == 0} {
4931 if {$bailout == 0 && [gets $fd line
] > -1} {
4943 if {[string first
"processes created" $line] > 0} {
4946 if {[string first
"type return to proceed" $line] > 0} {
4953 set i
[string first
"<merge" $line]
4955 set line
[string range
$line 0 $i]
4959 set pmtch
[scan $line \
4960 "%d: proc %d (%s line %d \"%s\" " \
4961 pstp pno pname pln Fnm
]
4963 set i
[string first
"\[" $line]
4966 set j
[string length
$line]
4968 set stmnt
[string range
$line $i $j]
4973 set pmtch
[scan $line \
4974 " proc %d (%s line %d \"%s\" " \
4978 if {[string first
"spin: line" $line] == 0 } {
4979 scan $line "spin: line %d \"%s\" " pln Fnm
4980 if {[string first
"pan_in" $Fnm] >= 0} {
4981 .inp.t tag add Rev
$pln.0 $pln.end
4982 .inp.t tag configure Rev
\
4983 -background $FG -foreground $BG
4984 .inp.t yview
-pickplace $pln.0
4986 if {[string first
"assertion viol" $line] < 0} {
4990 if {[string first
"Error: " $line] >= 0 \
4991 ||
[string first
"warning: " $line] >= 0 } {
4995 if {$pmtch != 4 && $syntax == 0} {
4996 set pmtch
[scan $line \
4997 "%d: proc - (%s line %d \"%s\" " \
4999 if { $pmtch == 4 } {
5003 # set Fnm [string trim $Fnm "\""]
5004 set pname
[string trim
$pname "()"]
5006 if {[string first
"TRACK" $pname] >= 0} {
5007 set nwcol
([expr $pno+1]) 1
5008 } elseif
{[string length
$pname] > 0} {
5009 if {[info exists nwcol
([expr $pno+1])] \
5010 && $nwcol([expr $pno+1])} {
5013 set TMP1
[expr ($pno + 1)*$XSZ]
5014 set TMP2
[expr $Pstp*$YSZ]
5015 .f
$dbox2.c create line
\
5016 [expr $TMP1 - 20] $TMP2 \
5017 [expr $TMP1 + 20] $TMP2 \
5021 .f
$dbox2.c create line
\
5022 [expr $TMP1 - 20] $TMP2 \
5023 [expr $TMP1 + 20] $TMP2 \
5028 set nwcol
([expr $pno+1]) 0
5030 if {$pmtch == 4 && $syntax == 0} {
5032 if {[string first
"values:" $line] < 0} {
5035 if {$m_typ == 1 && $tsc} {
5036 if { [info exists pbox
($pno)] == 0 } {
5037 set pbox
($pno) [mkbox
\
5038 "Proc $pno ($pname)" \
5039 "Proc$pno" "proc.$pno.out" \
5041 [expr 100+$pno*25] \
5042 [expr 325+$pno*35] ]
5044 set dbox
$pbox($pno)
5045 } elseif
{$m_typ == 0 && $tsc} {
5046 if { [info exists Spbox
($pno)] == 0 } {
5048 [mkbox
"$pname (proc $pno)" \
5051 [expr 100+$pno*25] \
5052 [expr 325+$pno*35] ]
5053 readinfile .c
$Spbox($pno).z.t
"pan_in"
5055 set Sdbox
$Spbox($pno)
5057 } elseif
{ [string first
"..." $line] > 0 && \
5058 [regexp "^\\\t*MSC: (.*)" $line] == 0 } {
5062 } elseif
{$s_typ == 2 \
5063 && [string first
"Select " $line] == 0 } {
5067 set lastexecutable
0
5069 } elseif
{$s_typ == 2 \
5070 && [string first
"choice" $line] >= 0 } {
5071 scan $line " choice %d" howmany
5072 set NN
[string first
":" $line]; incr NN
2
5073 set Choice
($howmany) [string range
$line $NN end
]
5074 if {[string first
"timeout" $Choice($howmany)] > 0} {
5077 if {[string first
"unexecutable," $line] >= 0} {
5080 set lastexecutable
$howmany
5083 } elseif
{$s_typ == 2 \
5084 && [string first
"Make Selection" $line] >= 0 } {
5085 scan $line "Make Selection %d" howmany
5086 if {$notexecutable == $howmany-1 && $has_timeout == 0} {
5087 set howmany
$lastexecutable
5088 add_log
"selected: $howmany (forced)"
5090 foreach el
[array names Choice
] {
5095 add_log
"selected: $howmany"
5101 } elseif
{ [regexp "^\\\t*MSC: (.*)" $line mch rstr
] != 0 } {
5102 if {$realstring != ""} {
5103 set realstring
"$realstring $rstr"
5105 set realstring
$rstr
5107 # picked up in next cycle
5108 } elseif
{ [string first
"processes" $line] > 0 \
5109 ||
[string first
"timeout" $line] == 0 \
5110 ||
[string first
"=s==" $line] > 0 \
5111 ||
[string first
"=r==" $line] > 0 } {
5113 if { $m_typ == 1 && $tsc} {
5115 } elseif
{ $m_typ == 0 && $tsc} {
5116 if { [info exists Spbox
($pno)] == 0 } {
5118 [mkbox
"$pname (proc $pno)" \
5121 [expr 100+$pno*25] \
5122 [expr 325+$pno*35] ]
5123 readinfile .c
$Spbox($pno).z.t
"pan_in"
5125 set Sdbox
$Spbox($pno)
5127 set pln
0; # prevent tag update
5128 } elseif
{$syntax == 0 && [string first
" = " $line] > 0 } {
5129 set isvar
[string first
"=" $line]
5130 set isvar
[expr $isvar + 1]
5131 set varvl
[string range
$line $isvar end
]
5132 set isvar
[expr $isvar - 2]
5133 set varnm
[string range
$line 0 $isvar]
5134 set varnm
[string trim
$varnm " "]
5135 set Varnm
($varnm) $varvl
5137 } elseif
{ [scan $line " %s %d " varnm qnr
] == 2} {
5138 if {$syntax == 0 && [string compare
$varnm "queue"] == 0} {
5139 set isvar
[string last
":" $line]
5140 set isvar
[expr $isvar + 1]
5141 set varvl
[string range
$line $isvar end
]
5142 set XX
[string first
"(" $line]
5143 set YY
[string last
")" $line]
5144 set ZZ
[string range
$line $XX $YY]
5145 set Queues
($qnr) $varvl
5146 if {[info exists Alias
($qnr)]} {
5147 if {[string first
$ZZ $Alias($qnr)] < 0} {
5148 set Alias
($qnr) "$Alias($qnr), $ZZ"
5155 } elseif
{[string length
$line] == 0} {
5156 if {$dontwait == 0} { set stepper
0 }
5158 set Depth
[expr $Depth + 1]
5159 set Seq
($Depth) [tell $fd]
5165 if {[string first
"terminates" $line] > 0} {
5170 if {$pln > 0 && [string first
"pan_in" $Fnm] >= 0} {
5171 .inp.t tag remove hilite
0.0 end
5176 if {$pln > 0 && [string first
"pan_in" $Fnm] >= 0} {
5178 .c
$Sdbox.z.t yview
-pickplace $pln.0
5179 .c
$Sdbox.z.t tag remove Rev
1.0 end
5180 .c
$Sdbox.z.t tag add Rev
$pln.0 $pln.end
5181 .c
$Sdbox.z.t tag configure Rev
\
5182 -background $FG -foreground $BG
5184 } elseif
{$m_typ == 1} {
5185 if { [info exists pbox
($pno)] == 0 } {
5186 set pbox
($pno) [mkbox
\
5187 "Proc $pno ($pname)" \
5188 "Proc$pno" "proc.$pno.out" \
5190 [expr 100+$pno*25] \
5191 [expr 325+$pno*35] ]
5193 set dbox
$pbox($pno)
5195 .c
$dbox.z.t yview
-pickplace end
5196 .c
$dbox.z.t insert end
"$line\n"
5198 } elseif
{$m_typ == 2 && $pln != 0 \
5199 && [string first
"unexecutable, " $line] < 0} {
5200 catch { .c
$dbox.z.t yview
-pickplace end
}
5201 catch { .c
$dbox.z.t insert end
"$pno:$pln" }
5202 for {set i
$pno} {$i > 0} {incr i
-1} {
5203 catch { .c
$dbox.z.t insert end
"\t|" }
5205 catch { .c
$dbox.z.t insert end
"\t|>$stmnt\n" }
5207 if {$msc && $pln != 0} {
5210 if { [scan $stmnt "values: %d!%d" inq inp1
] == 2 \
5211 ||
[scan $stmnt "values: %d!%s" inq inp2
] == 2 } {
5212 set HAS
[string first
"!" $stmnt]
5214 set Mcont
[string range
$stmnt $HAS end
]
5216 } elseif
{ [scan $stmnt "values: %d?%d" inq inp1
] == 2 \
5217 ||
[scan $stmnt "values: %d?%s" inq inp2
] == 2 } {
5218 set HAS
[string first
"?" $stmnt]
5220 set Mcont
[string range
$stmnt $HAS end
]
5222 } elseif
{ [string first
"-" $stmnt] == 0} {
5225 set stmnt
[format "Cycle>>"]
5227 set stmnt
[format "<waiting>"]
5229 } elseif
{ [string first
"<stop>" $stmnt] == 0} {
5231 set stmnt
[format "<stopped>"]
5233 if {$pno+1 > $Seenpno} { set Seenpno
[expr $pno+1] }
5234 set XLOC
[expr (1+$pno)*$XSZ]
5235 set YLOC
[expr $Pstp*$YSZ]
5236 if {[string first
"printf('MSC: " $stmnt] == 0} {
5238 set stmnt
$realstring
5239 if {[string first
"BREAK" $realstring] >= 0} {
5249 ||
[info exists R
($pstp,$pno)]} {
5251 if { $SparseMsc == 1 \
5252 ||
[info exists Plabel
($pno)] == 0 \
5253 ||
([info exists R
($pstp,$pno)] == 0 \
5255 ||
[info exists HasBox
($YLOC,[expr 1+$pno])])) } {
5258 {$Pstp > 1 && $i <= $Seenpno} \
5260 if {[info exists HasBox
($YLOC,$i)]} {
5263 set TMP1
[expr $i*$XSZ]
5271 .f
$dbox2.c create line
\
5277 if {[info exists HasBox
($YLOC,[expr 1+$pno])]} {
5278 set YLOC
[expr $Pstp*$YSZ]
5280 if {$HAS == 1 ||
$HAS == 2} {
5281 set stmnt
[string range
$stmnt 8 end
]
5283 if { [info exists Plabel
($pno)] == 0} {
5285 if {$SparseMsc == 0} {
5286 set HasBox
($YLOC,[expr 1+$pno]) 1
5288 .f
$dbox2.c create rectangle
\
5289 [expr $XLOC-20] $YLOC \
5292 -outline $Red -fill $Yellow
5294 if {$pname != "TRACK"} {
5295 .f
$dbox2.c create
text $XLOC \
5296 [expr $YLOC+$YSZ/2] \
5300 .f
$dbox2.c create
text $XLOC \
5301 [expr $YLOC+$YSZ/2] \
5306 set YLOC
[expr $Pstp*$YSZ]
5309 {$Pstp > 1 && $i <= $Seenpno} \
5311 set TMP1
[expr $i*$XSZ]
5319 .f
$dbox2.c create line
\
5326 if {(1+$pno) > $NPR} {
5327 set NPR
[expr $pno+2]
5328 .f
$dbox2.c configure
\
5331 [expr $NPR*$XSZ] [expr $SMX*$YSZ]"
5333 if {$Pstp > $SMX-2} {
5334 set SMX
[expr 2*$SMX]
5335 .f
$dbox2.c configure
\
5338 [expr $NPR*$XSZ] [expr $SMX*$YSZ]"
5341 if { [info exists R
($pstp,$pno)] == 0 } {
5342 if {$VERBOSE == 1} {
5343 if {[string first
"~W " $stmnt] == 0} {
5345 set stmnt
[string range
$stmnt 3 end
]
5346 } else { if {[string first
"~G " $stmnt] == 0} {
5348 set stmnt
[string range
$stmnt 3 end
]
5349 } else { if {[string first
"~R " $stmnt] == 0} {
5351 set stmnt
[string range
$stmnt 3 end
]
5352 } else { if {[string first
"~B " $stmnt] == 0} {
5354 set stmnt
[string range
$stmnt 3 end
]
5355 } else { set BoxFil
$Yellow } } } }
5357 if {[string first
"line " $stmnt] == 0} {
5358 scan $stmnt "line %d" pln
5359 set Fnm
"pan_in" ;# not necessarily right...
5365 if {$SparseMsc == 0} {
5366 set HasBox
($YLOC,[expr 1+$pno]) 1
5369 [.f
$dbox2.c create rectangle
\
5370 [expr $XLOC-20] $YLOC \
5373 -outline $Blue -fill $BoxFil]
5375 [.f
$dbox2.c create
text \
5377 [expr $YLOC+$YSZ/2] \
5380 #if {$Pstp > $YNR-2} {
5381 # .f$dbox2.c yview \
5382 # [expr ($Pstp-$YNR)]
5386 .f
$dbox2.c itemconfigure
\
5388 -outline $Red -fill $Yellow
5392 .f
$dbox2.c itemconfigure
$T($pstp,$pno) \
5393 -font $SmallFont -text "$stmnt"
5395 if {$VERBOSE == 0 } {
5396 .f
$dbox2.c
bind $T($pstp,$pno) <Any-Enter
> "
5397 .f$dbox2.c itemconfigure $T($pstp,$pno) \
5398 -font $BigFont -text {$stmnt}
5399 .inp.t tag remove hilite 0.0 end
5400 if {[string first "pan_in
" $Fnm] >= 0} {
5404 .f
$dbox2.c
bind $T($pstp,$pno) <Any-Leave
> "
5405 .f$dbox2.c itemconfigure $T($pstp,$pno) \
5406 -font $SmallFont -text {$pstp}
5409 .f
$dbox2.c
bind $T($pstp,$pno) <Any-Enter
> "
5410 .inp.t tag remove hilite 0.0 end
5411 if {[string first "pan_in
" $Fnm] >= 0} {
5419 set YLOC
[expr $YLOC+$YSZ/2]
5421 if { [info exists Q_add
($inq)] == 0 } {
5425 set Slot
$Q_add($inq)
5428 set Mesg_y
($inq,$Slot) $YLOC
5429 set Mesg_x
($inq,$Slot) $XLOC
5430 set Q_val
($inq,$Slot) $Mcont
5432 set Rem
($inq,$Slot) \
5433 [.f
$dbox2.c create
text \
5434 [expr $XLOC-40] $YLOC \
5435 -font $SmallFont -text $stmnt]
5436 } elseif
{ $HAS == 2 } {
5438 set Slot
$Q_del($inq)
5441 for {set Slot
$Q_del($inq)} \
5442 {$Slot < $Q_add($inq)} \
5444 if {$Q_val($inq,$Slot) == "_X_"} {
5450 for {set Slot
$Q_del($inq)} \
5451 {$Slot < $Q_add($inq)} \
5453 if {$Mcont == $Q_val($inq,$Slot)} {
5454 set Q_val
($inq,$Slot) "_X_"
5458 if {$Slot >= $Q_add($inq)} {
5459 add_log
"<<error: cannot match $stmnt>>"
5461 set TMP1
$Mesg_x($inq,$Slot)
5462 set TMP2
$Mesg_y($inq,$Slot)
5463 if {$XLOC < $TMP1} {
5468 .f
$dbox2.c create line
\
5469 [expr $TMP1+$Delta] $TMP2 \
5470 [expr $XLOC-$Delta] $YLOC \
5471 -fill $Red -width 2 \
5472 -arrow last
-arrowshape {5 5 5}
5474 if {$SparseMsc == 0} {
5480 .f
$dbox2.c coords
$Rem($inq,$Slot) \
5481 [expr ($TMP1 + $XLOC)/2] \
5482 [expr ($TMP2 + $YLOC)/2 - $TMP3]
5483 .f
$dbox2.c
raise $Rem($inq,$Slot)
5487 if {$pln == 0 && ($gvars ||
$lvars ||
$qv)} {
5489 if {$vv} { set Vvbox
[mkbox
"Data Values" \
5490 "Vars" "var.out" 71 19 100 350] }
5492 catch { .c
$Vvbox.z.t delete
0.0 end
}
5495 if {$gvars ||
$lvars} {
5497 foreach el
[lsort [array names Varnm
]] {
5498 if {[string length
$Varnm($el)] > 0} {
5499 catch { .c
$Vvbox.z.t insert
\
5500 end
"$el = $Varnm($el)\n" }
5504 foreach el
[lsort [array names Queues
]] {
5506 .c
$Vvbox.z.t insert end
"queue $el ($Alias($el))\n"
5507 .c
$Vvbox.z.t insert end
" $Queues($el)\n"
5516 if {[string first
"..." $line] < 0} {
5518 catch { .c
$sbox.z.t insert end
"$line\n" }
5519 catch { .c
$sbox.z.t yview
-pickplace end
}
5522 if {[string length
$line] > 0} {
5523 catch { .c
$sbox.z.t insert end
"$line\n" }
5524 catch { .c
$sbox.z.t yview
-pickplace end
}
5526 if {$m_typ == 2 && \
5527 [string first
"START OF CYCLE" $line] > 0} {
5528 catch { .c
$dbox.z.t yview
-pickplace end
}
5529 catch { .c
$dbox.z.t insert end
"$line\n" }
5531 set XLOC
[expr $Seenpno*$XSZ+$XSZ/2]
5532 set YLOC
[expr $Pstp*$YSZ+$YSZ/2]
5534 .f
$dbox2.c create
text \
5535 [expr $XLOC+$XSZ] $YLOC \
5537 -text "Cycle/Waiting" \
5540 .f
$dbox2.c create line
\
5542 [expr $XLOC+$XSZ/2] $YLOC \
5544 -arrow first
-arrowshape {5 5 5}
5546 set HAS_CYCLE
[expr $YLOC+1]
5548 if {$m_typ == 2 && $HAS == 3 && $HAS_CYCLE != 0} {
5550 set YLOC
[expr $Pstp*$YSZ+$YSZ/2]
5551 set XLOC0
[expr $pno*$XSZ+$XSZ]
5552 set XLOC
[expr $Seenpno*$XSZ+$XSZ]
5553 .f
$dbox2.c create line
\
5554 $XLOC0 [expr $YLOC-$YSZ/2] \
5557 .f
$dbox2.c create line
\
5558 $XLOC0 $YLOC $XLOC $YLOC \
5561 set XLOC
[expr $Seenpno*$XSZ+$XSZ]
5563 .f
$dbox2.c create line
\
5565 [expr $HAS_CYCLE-1] \
5569 if {$tk_major >= 4 ||
$m_typ != 1} {
5570 update ;# tk 3.x can crash on this
5577 && $dontwait == 0} {
5578 update ;# here it is harmless also with tk 3.x
5579 tkwait variable stepper
5582 if {$s_typ == 0 ||
$s_typ == 2} {
5583 add_log
"<at end of run>"
5585 add_log
"<at end of trail>"
5587 catch { addscales
$dbox2 }
5588 if {$ebc} { barscales
}
5590 tkwait variable stepper
5593 # end of guided trail
5595 while {$stepper == 1} {
5596 tkwait variable stepper
5607 global m_typ pbox sbox dbox Spbox Vvbox
5608 global simruns stop stepped stepper howmany
5614 catch { set howmany
0 }
5616 if { $m_typ == 1 } {
5617 foreach el
[array names pbox
] {
5618 catch { destroy .c
$pbox($el) }
5619 catch { unset pbox
($el) }
5621 } elseif
{ $m_typ == 0 } {
5622 foreach el
[array names Spbox
] {
5623 catch { destroy .c
$Spbox($el) }
5624 catch { unset Spbox
($el) }
5627 if {[winfo exists .c
$sbox]} {
5628 set x
"Simulation Output"
5629 set PlaceBox
($x) [wm geometry .c
$sbox]
5630 set k
[string first
"\+" $PlaceBox($x)]
5632 set PlaceBox
($x) [string range
$PlaceBox($x) $k end
]
5636 catch { destroy .c
$dbox }
5637 if {[winfo exists .c
$Vvbox]} {
5639 set PlaceBox
($x) [wm geometry .c
$Vvbox]
5640 set k
[string first
"\+" $PlaceBox($x)]
5642 set PlaceBox
($x) [string range
$PlaceBox($x) $k end
]
5648 set PlaceMenu
"+150+150"
5650 proc pickoption
{nm
} {
5651 global howmany Choice PlaceMenu
5653 catch {destroy .prompt
}
5655 wm title .prompt
"Select"
5656 wm iconname .prompt
"Select"
5657 wm geometry .prompt
$PlaceMenu
5659 text .prompt.t
-relief raised
-bd 2 \
5660 -width [string length
$nm] -height 1 \
5662 pack append .prompt .prompt.t
{ top expand fillx
}
5663 .prompt.t insert end
"$nm"
5664 for {set i
0} {$i <= $howmany} {incr i
} {
5665 if {[info exists Choice
($i)] \
5666 && $Choice($i) != 0 \
5667 && [string first
"outside range" $Choice($i)] < 0 \
5668 && [string first
"unexecutable," $Choice($i)] <= 0} {
5669 pack append .prompt
\
5670 [button .prompt.b
$i -text "$i: $Choice($i)" \
5672 -command "set howmany $i" ] \
5675 set j
[string first
"line " $Choice($i)]
5677 set k
[string range
$Choice($i) $j end
]
5679 bind .prompt.b
$i <Enter
> "report $k"
5680 bind .prompt.b
$i <Leave
> "report 0"
5681 bind .prompt.b
$i <ButtonRelease-1
> "set howmany $i"
5683 tkwait variable howmany
5684 set PlaceMenu
[wm geometry .prompt
]
5685 set k
[string first
"\+" $PlaceMenu]
5687 set PlaceMenu
[string range
$PlaceMenu $k end
]
5689 catch { foreach el
[array names Choice
] { unset Choice
($el) } }
5694 .inp.t tag remove hilite
0.0 end
5695 if {$n > 0} { src_line
$n }
5698 # validation options panel
5700 set an_typ
-1; set cp_typ
0; set cyc_typ
0
5701 set as_typ
-1; set ie_typ
1; set ebc
0
5702 set ct_typ
0; set et_typ
1
5703 set st_typ
0; set se_typ
0; set bf_typ
0
5704 set oct_typ
-1; # remembers last setting used for compilation
5706 set po_typ
-1; set cm_typ
0; set vb_typ
0
5707 set pr_typ
0; set where
0
5708 set vr_typ
0; set xu_typ
-1
5709 set ur_typ
1; set vbox
0
5710 set killed
0; set Job_Done
0; set tcnt
0
5712 set not_warned_yet
1
5718 proc syntax_check
{a T
} {
5722 add_log
"$SPIN $a pan_in"
5723 catch {exec $SPIN $a pan_in
>&pan.tmp
} err
;# added -v
5726 set ef
[open pan.tmp r
]
5727 .inp.t tag remove hilite
0.0 end
5728 .inp.t tag remove sel
0.0 end
5731 while {[gets $ef line
] > -1} {
5733 set allmsg
"$allmsg\n$line"
5734 if {[string first
"spin: line" $line] >= 0} {
5735 scan $line "spin: line %d" pln
5738 if {[string first
"spin: warning, line" $line] >= 0} {
5739 scan $line "spin: warning, line %d" pln
5745 if {$cnt == 0} { add_log
"no syntax errors" } else {
5746 warner
$T "$allmsg" 800
5752 global an_typ cp_typ nv_typ po_typ
5753 global xu_typ as_typ ie_typ
5757 if {$an_typ == -1} {
5759 set nv_typ
[hasWord
"never"]
5760 if {[hasWord
"accept.*:"]} {
5763 } elseif
{[hasWord
"progress.*:"]} {
5768 if {$po_typ == -1} {
5769 if {[hasWord
"_last"] \
5770 ||
[hasWord
"provided.*\\("] \
5771 ||
[hasWord
"enabled\\("]} {
5777 if {$xu_typ == -1} {
5778 if {[hasWord
"xr"] ||
[hasWord
"xs"]} {
5784 if {$as_typ == -1} {
5786 set as_typ
[hasWord
"assert"]
5796 global e ival expl HelvBig PlaceSim
5797 global an_typ cp_typ nv_typ firstime
5798 global cyc_typ ct_typ lt_typ
5799 global et_typ st_typ se_typ bf_typ stop
5800 global vb_typ pr_typ vr_typ ur_typ xu_typ
5808 catch { .
menu.run.m entryconfigure
8 -state normal
}
5809 catch { .tl.results.top.rv configure
-state normal
}
5817 set k
[string first
"\+" $PlaceSim]
5819 set PlaceSim
[string range
$PlaceSim $k end
]
5822 wm title .v
"LTL Verification Options"
5823 wm iconname .v
"VAL"
5824 wm geometry .v
$PlaceSim
5828 frame .v.correct
-relief flat
-borderwidth 1m
5829 frame .v.cframe
-relief raised
-borderwidth 1m
5833 frame $z.rframe
-relief raised
-borderwidth 1m
5835 label $z.rframe.lb
\
5838 -relief sunken
-borderwidth 1m
5840 checkbutton $z.rframe.fc
-text "With Weak Fairness" \
5843 checkbutton $z.rframe.xu
-text "Check xr/xs Assertions" \
5847 pack append $z.rframe
\
5848 $z.rframe.lb
{top pady
4 frame w fillx
} \
5849 $z.rframe.fc
{top pady
4 frame w
} \
5850 $z.rframe.xu
{top pady
4 frame w filly
}
5852 pack append $z $z.rframe
{top
frame nw filly
}
5854 label .v.cframe.lb
\
5856 -text "Verification" \
5857 -relief sunken
-borderwidth 1m
5859 radiobutton .v.cframe.ea
-text "Exhaustive" \
5860 -variable ct_typ
-value 0 \
5862 radiobutton .v.cframe.sa
-text "Supertrace/Bitstate" \
5863 -variable ct_typ
-value 1 \
5865 radiobutton .v.cframe.hc
-text "Hash-Compact" \
5866 -variable ct_typ
-value 2 \
5869 pack append .v.cframe .v.cframe.lb
{top pady
4 frame nw fillx
} \
5870 .v.cframe.ea
{top pady
4 frame nw
} \
5871 .v.cframe.sa
{top pady
4 frame nw
} \
5872 .v.cframe.hc
{top pady
4 frame nw
}
5874 frame .v.pf
-relief raised
-borderwidth 1m
5875 frame .v.pf.mesg
-borderwidth 1m
5877 label .v.pf.mesg.loss0
\
5879 -text "A Full Queue" \
5880 -relief sunken
-borderwidth 1m
5881 radiobutton .v.pf.mesg.loss1
-text "Blocks New Msgs" \
5882 -variable l_typ
-value 0 \
5884 radiobutton .v.pf.mesg.loss2
-text "Loses New Msgs" \
5885 -variable l_typ
-value 1 \
5887 pack append .v.pf.mesg
\
5888 .v.pf.mesg.loss0
{top pady
4 frame w expand fillx
} \
5889 .v.pf.mesg.loss1
{top pady
4 frame w
} \
5890 .v.pf.mesg.loss2
{top pady
4 frame w
}
5892 .v.pf.mesg
{left
frame w expand fillx
}
5895 .v.cframe
{top
frame w fill
}\
5896 .v.correct
{top
frame w fill
}\
5897 .v.pf
{top
frame w expand fill
}
5899 pack append .v
[button .v.adv
-text "\[Set Advanced Options]" \
5900 -command "advanced_val" ] {top fillx
}
5901 pack append .v
[button .v.run
-text "Run" \
5902 -command {runval
".tl.results.t"} ] {right
frame se
}
5903 pack append .v
[button .v.
exit -text "Cancel" \
5904 -command "set PlaceSim [wm geometry .v]; \
5905 set stop 1; destroy .v"] {right
frame se
}
5906 pack append .v
[button .v.help
-text "Help" -fg red
\
5907 -command "roadmap2f" ] {right
frame se
}
5909 tkwait visibility .v
5913 set PlaceBasic
"+200+10"
5914 set PlaceAdv
"+150+10"
5917 global e ival expl HelvBig PlaceBasic
5918 global an_typ nv_typ firstime as_typ ie_typ
5919 global cyc_typ ct_typ lt_typ as_typ ie_typ
5920 global et_typ st_typ se_typ bf_typ stop
5921 global vb_typ pr_typ vr_typ ur_typ xu_typ
5923 catch { .
menu.run.m entryconfigure
8 -state normal
}
5924 catch { .tl.results.top.rv configure
-state normal
}
5932 wm title .v
"Basic Verification Options"
5933 wm iconname .v
"VAL"
5934 wm geometry .v
$PlaceBasic
5938 frame .v.correct
-relief flat
-borderwidth 1m
5939 frame .v.cframe
-relief raised
-borderwidth 1m
5943 frame $z.rframe
-relief raised
-borderwidth 1m
5945 label $z.rframe.lb
\
5947 -text "Correctness Properties" \
5948 -relief sunken
-borderwidth 1m
5949 radiobutton $z.rframe.sp
-text "Safety (state properties)" \
5950 -variable an_typ
-value 0 \
5952 -command { set cyc_typ
0; set cp_typ
0
5954 set as_typ
[hasWord
"assert"]
5959 checkbutton $z.rframe.sf.as
-text "Assertions" \
5964 if {![hasWord
"assert"] && $as_typ==1} then
{
5968 checkbutton $z.rframe.sf.ie
-text "Invalid Endstates" \
5971 -command { set an_typ
0 }
5973 frame $z.rframe.sf.fill
-width 15
5974 pack append $z.rframe.sf
\
5975 $z.rframe.sf.fill
{left
frame w
} \
5976 $z.rframe.sf.as
{top pady
4 frame w
} \
5977 $z.rframe.sf.ie
{top pady
4 frame w
}
5979 radiobutton $z.rframe.cp
-text "Liveness (cycles/sequences)" \
5980 -variable an_typ
-value 1 \
5983 set as_typ
0; set ie_typ
0
5984 if {[hasWord
"accept"]} then
{ set cp_typ
2 }\
5985 elseif
{[hasWord
"progress"]} then
{ set cp_typ
1 } \
5990 radiobutton $z.rframe.sub.np
-text "Non-Progress Cycles" \
5991 -variable cp_typ
-value 1 \
5995 if {![hasWord
"progress"] && $cp_typ==1} then
{
5999 radiobutton $z.rframe.sub.ac
-text "Acceptance Cycles" \
6000 -variable cp_typ
-value 2 \
6004 if {![hasWord
"accept"] && $cp_typ==2} then
{
6008 checkbutton $z.rframe.sub.fc
-text "With Weak Fairness" \
6011 -command { if {$an_typ==0} then
"set cyc_typ 0; complain3" }
6013 checkbutton $z.rframe.nv
-text "Apply Never Claim (If Present)" \
6016 -command { if {![hasWord
"never"] && $nv_typ==1} then
"complain2" }
6017 checkbutton $z.rframe.ur
-text "Report Unreachable Code" \
6020 checkbutton $z.rframe.xu
-text "Check xr/xs Assertions" \
6024 frame $z.rframe.sub.fill
-width 15
6025 pack append $z.rframe.sub
\
6026 $z.rframe.sub.fill
{left
frame w
} \
6027 $z.rframe.sub.np
{top pady
4 frame w
} \
6028 $z.rframe.sub.ac
{top pady
4 frame w
} \
6029 $z.rframe.sub.fc
{top pady
4 frame w
}
6031 pack append $z.rframe
\
6032 $z.rframe.lb
{top pady
4 frame w fillx
} \
6033 $z.rframe.sp
{top pady
4 frame w
} \
6034 $z.rframe.sf
{top pady
4 frame w
} \
6035 $z.rframe.cp
{top pady
4 frame w
} \
6036 $z.rframe.sub
{top pady
4 frame w
} \
6037 $z.rframe.nv
{top pady
4 frame w
} \
6038 $z.rframe.ur
{top pady
4 frame w
} \
6039 $z.rframe.xu
{top pady
4 frame w filly
}
6041 pack append $z $z.rframe
{top
frame nw filly
}
6043 label .v.cframe.lb
\
6045 -text "Search Mode" \
6046 -relief sunken
-borderwidth 1m
6048 radiobutton .v.cframe.ea
-text "Exhaustive" \
6049 -variable ct_typ
-value 0 \
6051 radiobutton .v.cframe.sa
-text "Supertrace/Bitstate" \
6052 -variable ct_typ
-value 1 \
6054 radiobutton .v.cframe.hc
-text "Hash-Compact" \
6055 -variable ct_typ
-value 2 \
6058 pack append .v.cframe .v.cframe.lb
{top pady
4 frame nw fillx
} \
6059 .v.cframe.ea
{top pady
4 frame nw
} \
6060 .v.cframe.sa
{top pady
4 frame nw
} \
6061 .v.cframe.hc
{top pady
4 frame nw
}
6063 frame .v.pf
-relief raised
-borderwidth 1m
6064 frame .v.pf.mesg
-borderwidth 1m
6066 label .v.pf.mesg.loss0
\
6068 -text "A Full Queue" \
6069 -relief sunken
-borderwidth 1m
6070 radiobutton .v.pf.mesg.loss1
-text "Blocks New Msgs" \
6071 -variable l_typ
-value 0 \
6073 radiobutton .v.pf.mesg.loss2
-text "Loses New Msgs" \
6074 -variable l_typ
-value 1 \
6076 pack append .v.pf.mesg
\
6077 .v.pf.mesg.loss0
{top pady
4 frame w fillx
} \
6078 .v.pf.mesg.loss1
{top pady
4 frame w
} \
6079 .v.pf.mesg.loss2
{top pady
4 frame w
}
6081 .v.pf.mesg
{left
frame nw expand fill
}
6085 .v.cframe
{top
frame n expand fill
}\
6086 .v.pf
{top
frame n expand fill
}
6088 pack append .v
[button .v.nvr
-text "\[Add Never Claim from File]" \
6089 -command "call_nvr" ] {top fillx
}
6090 pack append .v
[button .v.ltl
-text "\[Verify an LTL Property]" \
6091 -command "destroy .v; call_tl" ] {top fillx
}
6092 pack append .v
[button .v.adv
-text "\[Set Advanced Options]" \
6093 -command "advanced_val" ] {top fillx
}
6094 pack append .v
[button .v.run
-text "Run" \
6095 -command {set PlaceBasic
[wm geometry .v
]; runval
"0"} ] {right
frame se
}
6096 pack append .v
[button .v.
exit -text "Cancel" \
6097 -command {set PlaceBasic
[wm geometry .v
]; \
6098 set stop
1; destroy .v
}] {right
frame se
}
6099 pack append .v
[button .v.help
-text "Help" -fg red
\
6100 -command "roadmap2e" ] {right
frame se
}
6102 tkwait visibility .v
6110 global xversion Fname nv_typ
6112 switch [info commands
tk_getOpenFile] "" {
6113 set fileselect
"FileSelect open"
6115 set fileselect
"tk_getOpenFile \
6117 { { Aut files } .aut } \
6118 { { Nvr files } .nvr } \
6119 { { All Files } * } \
6123 set HasNever
[eval $fileselect]
6125 if {$HasNever == ""} {
6126 wm title .
"SPIN CONTROL $xversion -- File: $Fname"
6130 set z
[string last
"\/" $HasNever]
6133 set HsN
[string range
$HasNever $z end
]
6137 wm title .
"SPIN CONTROL $xversion -- File: $Fname Claim: $HsN"
6141 proc advanced_val
{} {
6142 global e ival expl HelvBig
6143 global nv_typ firstime PlaceAdv
6144 global cyc_typ ct_typ
6145 global et_typ st_typ se_typ bf_typ stop po_typ cm_typ
6146 global vb_typ pr_typ vr_typ ur_typ xu_typ
6148 catch { .
menu.run.m entryconfigure
8 -state normal
}
6149 catch { .tl.results.top.rv configure
-state normal
}
6156 wm title .av
"Advanced Verification Options"
6157 wm iconname .av
"VAL"
6158 wm geometry .av
$PlaceAdv
6161 frame .av.pans.correct
-relief flat
6162 frame .av.memopts
-relief flat
; # memory options panel
6163 frame .av.oframe
-relief raised
-borderwidth 1m
;# error trail options
6164 frame .av.recomp
-relief raised
-borderwidth 1m
;# recompilation
6168 for {set x
0} {$x<=2} {incr x
} {
6169 frame .av.memopts.choice
$x -relief flat
6170 entry .av.memopts.choice
$x.e1
-relief sunken
-width 20
6171 label .av.memopts.choice
$x.e2
-text $e($x) -relief flat
6172 .av.memopts.choice
$x.e1 insert end
$ival($x)
6174 pack append .av.memopts.choice
$x \
6175 .av.memopts.choice
$x.e2
{left
frame w fillx
} \
6176 [button .av.memopts.choice
$x.e3
-text $expl($x) \
6177 -command "d_list $x" ] {right
frame e
} \
6178 .av.memopts.choice
$x.e1
{right
frame e fillx
}
6180 pack append .av.memopts
\
6181 .av.memopts.choice
$x { top
frame w pady
5 fillx
}
6183 for {set x
7} {$x<=7} {incr x
} {
6184 frame .av.memopts.choice
$x -relief flat
6185 entry .av.memopts.choice
$x.e1
-relief sunken
-width 20
6186 label .av.memopts.choice
$x.e2
-text $e($x) -relief flat
6187 .av.memopts.choice
$x.e1 insert end
$ival($x)
6189 pack append .av.memopts.choice
$x \
6190 .av.memopts.choice
$x.e2
{left
frame w fillx
} \
6191 [button .av.memopts.choice
$x.e3
-text $expl($x) \
6192 -command "d_list $x" ] {right
frame e
} \
6193 .av.memopts.choice
$x.e1
{right
frame e fillx
}
6195 pack append .av.memopts
\
6196 .av.memopts.choice
$x { top
frame w pady
5 fillx
}
6198 for {set x
3} {$x<=5} {incr x
} {
6199 frame .av.memopts.choice
$x -relief flat
6200 entry .av.memopts.choice
$x.e1
-relief sunken
-width 20
6201 label .av.memopts.choice
$x.e2
-text $e($x) -relief flat
6202 .av.memopts.choice
$x.e1 insert end
$ival($x)
6204 pack append .av.memopts.choice
$x \
6205 .av.memopts.choice
$x.e2
{left
frame w fillx
} \
6206 [button .av.memopts.choice
$x.e3
-text $expl($x) \
6207 -command "d_list $x" ] {right
frame e
} \
6208 .av.memopts.choice
$x.e1
{right
frame e fillx
}
6210 pack append .av.memopts
\
6211 .av.memopts.choice
$x { top
frame w pady
5 fillx
}
6213 set z .av.pans.correct
6214 frame $z.rframe
-relief raised
-borderwidth 1m
6215 label $z.rframe.lb3
\
6217 -text " Error Trapping " \
6218 -relief sunken
-borderwidth 1m
6219 radiobutton $z.rframe.c0
-text "Don't Stop at Errors" \
6220 -variable et_typ
-value 0 \
6222 checkbutton $z.rframe.c0a
-text "Save All Error-trails" \
6225 checkbutton $z.rframe.c0b
-text "Find Shortest Trail (iterative)" \
6228 checkbutton $z.rframe.c0c
-text "Use Breadth-First Search" \
6231 frame $z.rframe.basic1
6234 radiobutton $z.rframe.cc.c1
-text "Stop at Error Nr:" \
6235 -variable et_typ
-value 1 \
6237 entry $z.rframe.cc.c2
-relief sunken
-width 8
6238 $z.rframe.cc.c2 insert end
"$ival(6)"
6239 pack append $z.rframe.cc
\
6240 $z.rframe.cc.c1
{left
}\
6241 $z.rframe.cc.c2
{right expand fillx
}
6243 pack append $z.rframe
\
6244 $z.rframe.lb3
{ top expand fillx
frame nw
} \
6245 $z.rframe.cc
{top pady
4 frame w
} \
6246 $z.rframe.c0
{top pady
4 frame w
} \
6247 $z.rframe.c0a
{top pady
4 frame w
} \
6248 $z.rframe.c0b
{top pady
4 frame w
} \
6249 $z.rframe.c0c
{top pady
4 frame w
} \
6250 $z.rframe.basic1
{top
frame w
}
6251 pack append $z $z.rframe
{top
frame nw expand fill
}
6253 frame .av.pans.pf
-relief flat
6255 frame $z.mesg
-relief raised
-borderwidth 1m
; # queue loss options
6256 frame $z.pframe
-relief raised
-borderwidth 1m
6257 label $z.pframe.lb2
\
6259 -text " Type of Run " \
6260 -relief sunken
-borderwidth 1m
6261 checkbutton $z.pframe.po
-text "Use Partial Order Reduction" \
6264 checkbutton $z.pframe.cm
-text "Use Compression" \
6267 # checkbutton $z.pframe.vb -text "Verbose (For Debugging Only)" \
6268 # -variable vb_typ \
6270 checkbutton $z.pframe.pr
-text "Add Complexity Profiling" \
6273 checkbutton $z.pframe.vr
-text "Compute Variable Ranges" \
6277 pack append $z.pframe
\
6278 $z.pframe.lb2
{top fillx pady
4 frame w
} \
6279 $z.pframe.po
{top pady
4 frame w
} \
6280 $z.pframe.cm
{top pady
4 frame w
} \
6281 $z.pframe.pr
{top pady
4 frame w
} \
6282 $z.pframe.vr
{top pady
4 frame w
}
6284 pack append .av.pans.pf
\
6285 .av.pans.pf.pframe
{top
frame nw expand fill
}
6286 pack append .av.pans
\
6287 .av.pans.correct
{left
frame nw expand fillx
}\
6288 .av.pans.pf
{left
frame nw expand fillx
}
6290 button .av.help
-text "Help" -fg red
-command "roadmap2d"
6291 button .av.basic1
-text "Set" -fg red
-command "stopval 1"
6292 button .av.basic0
-text "Cancel" -command "stopval 0"
6295 .av.memopts
{top
frame w
} \
6296 .av.pans
{top fillx
} \
6297 .av.help
{left
frame w
} \
6298 .av.basic1
{right
frame e
} \
6299 .av.basic0
{right
frame e
}
6310 wm title .r
"Options"
6311 wm iconname .r
"Options"
6314 listbox .r.top.
list -width 6 -height 3 -relief raised
6315 listbox .r.top.expl
-width 40 -height 3 -relief flat
6316 pack append .r.top
\
6320 text .r.bot.
text -width 40 -height 1 -relief flat
6321 .r.bot.
text insert end
"(Double-Click option or Cancel)"
6322 button .r.bot.quit
-text "Cancel" -command "destroy .r"
6323 pack append .r.bot
\
6325 .r.bot.quit
{frame s
}
6328 text .r.caps.cap1
-width 6 -height -1 -fg blue
6329 text .r.caps.cap2
-width 30 -height -1 -fg blue
6330 .r.caps.cap1 insert end
"Option:"
6331 .r.caps.cap2 insert end
"Meaning:"
6332 pack append .r.caps
\
6333 .r.caps.cap1
{left
} \
6338 .r.top
{top expand
} \
6339 .r.bot
{bottom expand
}
6341 foreach i
{ "-o1" "-o2" "-o3" } {
6342 .r.top.
list insert end
$i
6346 "disable dataflow-optimizations" \
6347 "disable dead variables elimination" \
6348 "disable statement merging" } {
6349 .r.top.expl insert end
$i
6351 bind .r.top.
list <Double-Button-1
> {
6352 set extra
[selection get
]
6353 .av.memopts.choice5.e1 insert end
" $extra"
6364 wm title .r
"Options"
6365 wm iconname .r
"Options"
6368 listbox .r.top.
list -width 6 -height 8 -relief raised
6369 listbox .r.top.expl
-width 40 -height 8 -relief flat
6370 pack append .r.top
\
6374 text .r.bot.
text -width 40 -height 1 -relief flat
6375 .r.bot.
text insert end
"(Double-Click option or Cancel)"
6376 button .r.bot.quit
-text "Cancel" -command "destroy .r"
6377 pack append .r.bot
\
6379 .r.bot.quit
{frame s
}
6382 text .r.caps.cap1
-width 6 -height -1 -fg blue
6383 text .r.caps.cap2
-width 30 -height -1 -fg blue
6384 .r.caps.cap1 insert end
"Option:"
6385 .r.caps.cap2 insert end
"Meaning:"
6386 pack append .r.caps
\
6387 .r.caps.cap1
{left
} \
6392 .r.top
{top expand
} \
6393 .r.bot
{bottom expand
}
6395 foreach i
{ "-d" "-q" "-I" "-h?" "-s" "-A" "-E" "-w?" } {
6396 .r.top.
list insert end
$i
6400 "print state tables and stop" \
6401 "require all chans to be empty in valid endstates" \
6402 "try to find shortest trail" \
6403 "choose another seed for hash 1..32 (default 1)" \
6404 "use 1-bit hashing (default is 2-bit)" \
6405 "ignore assertion violation errors" \
6406 "ignore invalid endstate errors" \
6407 "set explicit -w parameter" \
6409 .r.top.expl insert end
$i
6411 bind .r.top.
list <Double-Button-1
> {
6412 set extra
[selection get
]
6413 .av.memopts.choice4.e1 insert end
" $extra"
6420 if {$nr == 0} { roadmap2a
; return }
6421 if {$nr == 1} { roadmap2b
; return }
6422 if {$nr == 2} { roadmap2c
; return }
6423 if {$nr == 4} { r_list
; return }
6424 if {$nr == 5} { g_list
; return }
6425 if {$nr == 7} { roadmap2k
; return }
6426 # if {$nr != 3} { roadmap2; return }
6431 wm title .b
"Options"
6432 wm iconname .b
"Options"
6435 scrollbar .b.top.scroll
-command ".b.top.list yview"
6436 listbox .b.top.
list -yscroll ".b.top.scroll set" -relief raised
6437 pack append .b.top
\
6438 .b.top.scroll
{right filly
}\
6439 .b.top.
list {left expand
}
6442 text .b.bot.
text -width 21 -height 1 -relief flat
6443 .b.bot.
text insert end
"(Double-Click option)"
6444 button .b.bot.quit
-text "Cancel" -command "destroy .b"
6445 button .b.bot.expl
-text "Explanations" -command "roadmap6"
6446 pack append .b.bot
\
6447 .b.bot.
text {top
frame nw
}\
6453 .b.top
{top
frame nw expand
} \
6477 .b.top.
list insert end
$i
6479 bind .b.top.
list <Double-Button-1
> {
6480 set directive
[selection get
]
6481 .av.memopts.choice3.e1 insert end
" $directive"
6487 set m
"warning: there are no accept labels"
6489 catch { tk_messageBox -icon info -message $m }
6493 set m
"warning: there is no never claim"
6495 catch { tk_messageBox -icon info -message $m }
6499 set m
"weak fairness is irrelevant to state properties"
6501 catch { tk_messageBox -icon info -message $m }
6505 set m
"warning: there are no progress labels"
6507 catch { tk_messageBox -icon info -message $m }
6512 set m
"warning: there are neither accept nor progress labels"
6515 catch { tk_messageBox -icon info -message $m }
6519 set m
"warning: there are no assert statements in the spec"
6521 catch { tk_messageBox -icon info -message $m }
6525 set m
"warning: Breadth-First Search implies a restriction to Safety properties"
6527 catch { tk_messageBox -icon info -message $m }
6531 set m
"error: cannot combine -DMA and -DBITSTATE"
6533 catch { tk_messageBox -icon info -message $m }
6536 proc stopval
{how
} {
6537 global stop ival PlaceAdv
6540 set ival
(0) "[.av.memopts.choice0.e1 get]"
6541 set ival
(1) "[.av.memopts.choice1.e1 get]"
6542 set ival
(2) "[.av.memopts.choice2.e1 get]"
6543 set ival
(3) "[.av.memopts.choice3.e1 get]"
6544 set ival
(4) "[.av.memopts.choice4.e1 get]"
6545 set ival
(5) "[.av.memopts.choice5.e1 get]"
6546 set ival
(7) "[.av.memopts.choice7.e1 get]"
6547 set ival
(6) "[.av.pans.correct.rframe.cc.c2 get]"
6550 if {[winfo exists .av
]} {
6551 set PlaceAdv
[wm geometry .av
]
6552 set k
[string first
"\+" $PlaceAdv]
6554 set PlaceAdv
[string range
$PlaceAdv $k end
]
6570 proc bld_v_options
{} {
6571 global an_typ cp_typ cyc_typ as_typ ie_typ
6572 global et_typ st_typ se_typ l_typ bf_typ
6573 global ct_typ ival v_options a_options
6574 global c_options po_typ cm_typ vb_typ
6575 global pr_typ vr_typ ur_typ xu_typ
6576 global ol_typ oct_typ nv_typ lt_typ
6581 set a_options
"-a -X"
6582 if {$l_typ==1} { set a_options
[format "%s -m" $a_options] }
6583 if {$lt_typ==1} { set a_options
[format "%s -N pan.ltl" $a_options] }
6586 catch { set Mbytes
[.av.memopts.choice0.e1 get
] }
6588 # the Mstate scale resolution is in thousands: 2^10
6589 set Mstate
[expr 10+[log
$ival(1)]]
6590 catch { set Mstate
[expr 10+[log
[.av.memopts.choice1.e1 get
]]] }
6592 catch { set Mdepth
[.av.memopts.choice2.e1 get
] }
6593 catch { set ival
(0) "[.av.memopts.choice0.e1 get]" }
6594 catch { set ival
(1) "[.av.memopts.choice1.e1 get]" }
6595 catch { set ival
(2) "[.av.memopts.choice2.e1 get]" }
6596 catch { set ival
(3) "[.av.memopts.choice3.e1 get]" }
6597 catch { set ival
(4) "[.av.memopts.choice4.e1 get]" }
6598 catch { set ival
(5) "[.av.memopts.choice5.e1 get]" }
6599 catch { set ival
(7) "[.av.memopts.choice7.e1 get]" }
6601 if {$ct_typ == 2} { ;# hash-compact
6602 set c_options
[format "-DHC -DMEMLIM=%d" $Mbytes]
6604 # in exhaustive mode: #hashtable ~~ #states
6606 set v_options
"-X -m$Mdepth -w$Mstate"
6608 if {$Mstate >= $Mbytes} {
6610 tk_messageBox -icon info \
6611 -message "The Estimated Statespace size exceeds \
6612 the maximum that the Memory limit you set would allow."
6616 } elseif
{$ct_typ==1} {
6617 set c_options
[format "-DBITSTATE -DMEMLIM=%d" $Mbytes]
6619 # in supertrace mode: #bits ~~ 128x #states
6620 # (effectively the #bytes will be ~~ 16x #states)
6622 set Mstate
[expr 7+$Mstate]
6623 set v_options
"-X -m$Mdepth -w$Mstate"
6625 if {$Mstate-3 >= $Mbytes} {
6627 tk_messageBox -icon info \
6628 -message "The Estimated Statespace size exceeds \
6629 maximum allowed by the Memory limit that you set would allow."
6634 set c_options
[format "-DMEMLIM=%d" $Mbytes]
6636 # in exhaustive mode: #hashtable ~~ #states
6638 set v_options
"-X -m$Mdepth -w$Mstate"
6640 if {$Mstate >= $Mbytes} {
6642 tk_messageBox -icon info \
6643 -message "The Estimated Statespace size exceeds \
6644 the maximum that the Physical Memory limit allows."
6649 set c_options
[format "-D_POSIX_SOURCE %s" $c_options]
6650 if {$an_typ==0} { set c_options
[format "%s -DSAFETY" $c_options] }
6651 if {$an_typ==1 && $cp_typ==1} { set c_options
[format "%s -DNP" $c_options] }
6652 if {$po_typ==0} { set c_options
[format "%s -DNOREDUCE" $c_options] }
6653 if {$cm_typ==1 && $ct_typ!=1} { set c_options
[format "%s -DCOLLAPSE" $c_options] }
6654 if {$vb_typ==1} { set c_options
[format "%s -DCHECK" $c_options] }
6655 if {$nv_typ==0} { set c_options
[format "%s -DNOCLAIM" $c_options] }
6656 if {$se_typ!=0} { set c_options
[format "%s -DREACH" $c_options] }
6660 set c_options
[format "%s -DBFS -DSAFETY" $c_options]
6662 set c_options
[format "%s -DBFS" $c_options]
6664 if {$xu_typ==0 && $po_typ!=0} { set c_options
[format "%s -DXUSAFE" $c_options] }
6665 if {$pr_typ==1} { set c_options
[format "%s -DPEG" $c_options] }
6666 if {$vr_typ==1} { set c_options
[format "%s -DVAR_RANGES" $c_options] }
6668 set c_options
[format "%s -DNFAIR=3" $c_options]
6670 set c_options
[format "%s -DNOFAIR" $c_options]
6673 catch { set foo
[.av.memopts.choice3.e1 get
] }
6675 if {[string first
"-DBITSTATE" $c_options] > 0 && [string first
"-DMA" $foo] > 0} {
6678 set c_options
[format "%s %s" $c_options $foo ]
6681 catch { set foo
[.av.memopts.choice4.e1 get
] }
6682 set v_options
[format "%s %s" $v_options $foo ]
6685 catch { set foo
[.av.memopts.choice
.5.e1 get
] }
6686 set a_options
[format "%s %s" $a_options $foo ]
6688 if {$an_typ==0 && $as_typ==0} { set v_options
[format "%s -A" $v_options] }
6689 if {$an_typ==0 && $ie_typ==0} { set v_options
[format "%s -E" $v_options] }
6690 if {$an_typ==1 && $cp_typ==1} { set v_options
[format "%s -l" $v_options] }
6691 if {$an_typ==1 && $cp_typ==2} { set v_options
[format "%s -a" $v_options] }
6692 if {$cyc_typ==1} { set v_options
[format "%s -f" $v_options] }
6693 if {$ur_typ==0} { set v_options
[format "%s -n" $v_options] }
6694 if {$st_typ==1} { set v_options
[format "%s -e" $v_options] }
6695 if {$se_typ!=0} { set v_options
[format "%s -i" $v_options] }
6696 if {$et_typ==0} { set v_options
[format "%s -c0" $v_options] }
6697 if {$et_typ==1} { set v_options
[format "%s -c%s" $v_options $ival(6)] }
6698 if {$ct_typ==1 && $ival(7) != 2} { set v_options
[format "%s -k%s" $v_options $ival(7)] }
6705 proc runval
{havedest
} {
6706 global Unix CC SPIN Fname PlaceSim
6707 global v_options a_options notignored
6708 global c_options Job_Done mt skipmax
6709 global stop s_typ vbox waitwhat not_warned_yet
6710 global LastGenerate LastCompile NextCompile
6713 if {[bld_v_options
] == 0} {
6717 if {[winfo exists .v
]} {
6718 set PlaceSim
[wm geometry .v
]
6722 if {[string first
"\?" $c_options] > 0} {
6723 add_log
"error: undefined '?' in optional compiler directives"
6726 if {[string first
"\?" $v_options] > 0} {
6727 add_log
"error: undefined '?' in extra runtime options"
6730 add_log
"<starting verification>"
6731 if {$havedest != "0"} {
6732 $havedest insert end
"<starting verification>\n"
6735 set nochange
[no_change
]
6736 if {$nochange == 0} { set LastGenerate
"" }
6738 if {$LastGenerate == $a_options} {
6739 add_log
"<no code regeneration necessary>"
6740 if {$havedest != "0"} {
6741 $havedest insert end
"<no code regeneration necessary>\n"
6746 add_log
"$SPIN $a_options pan_in"; update
6747 if {$havedest != "0"} {
6748 $havedest insert end
"$SPIN $a_options pan_in\n"
6751 catch {eval exec $SPIN $a_options pan_in
} errmsg
6753 catch {eval exec $SPIN $a_options pan_in
>&pan.tmp
}
6754 set errmsg
[msg_file pan.tmp
0]
6756 if {[string length
$errmsg]>0} {
6757 set foo
[string first
"Exit-Status 0" $errmsg]
6760 if {$havedest != "0"} {
6761 $havedest insert end
"$errmsg\n"
6767 set errmsg
[string range
$errmsg 0 $foo]
6769 if {$havedest != "0"} {
6770 $havedest insert end
"$errmsg\n"
6773 set LastGenerate
$a_options
6775 set NextCompile
"$CC -o pan $c_options pan.c"
6777 if {$havedest != "0"} {
6778 catch { $havedest yview
-pickplace end
}
6780 if {$LastCompile == $NextCompile && [file exists pan
]} {
6781 add_log
"<no recompilation necessary>"
6782 if {$havedest != "0"} {
6783 $havedest insert end
"<no recompilation necessary>\n"
6787 add_log
$NextCompile
6788 if {$havedest != "0"} {
6789 $havedest insert end
"$NextCompile\n"
6792 warner
"Compiling" "Please wait until compilation of the \
6793 executable produced by spin completes." 300
6798 catch {eval exec $NextCompile >pan.tmp
2>pan.err
}
6801 catch {eval exec $NextCompile >pan.tmp
2>pan.err
}
6804 set errmsg
[msg_file pan.tmp
0]
6805 if {[string length
$errmsg] == 0} {
6806 set errmsg
[msg_file pan.err
0]
6808 set errmsg
"$errmsg\n[msg_file pan.err 0]"
6811 catch {destroy .warn
}
6815 if {[auto_execok "./pan"] == "" \
6816 ||
[auto_execok "./pan"] == 0} {
6818 add_log
"compilation failed"
6819 if {$havedest != "0"} {
6820 $havedest insert end
"<compilation failed>\n"
6826 if {[auto_execok "pan"] == "" \
6827 ||
[auto_execok "pan"] == 0} {
6829 add_log
"compilation failed"
6830 if {$havedest != "0"} {
6831 $havedest insert end
"<compilation failed>\n"
6837 set LastCompile
$NextCompile
6841 set PREFIX
"time ./pan -v"
6845 add_log
"$PREFIX $v_options"; update
6846 if {$havedest != "0"} {
6847 $havedest insert end
"$PREFIX $v_options\n"
6848 catch { $havedest yview
-pickplace end
}
6853 set errmsg
[catch {eval exec $PREFIX $v_options >&pan.out
&}]
6856 add_log
"could not run verification"
6857 if {$havedest != "0"} {
6858 $havedest insert end
"<could not run verification>\n"
6864 set not_warned_yet
1
6865 if {$havedest != "0"} {
6868 set vv
[mkbox
"Verification Output" "VerOut" "$Fname.out" 80 20]
6873 after 5000 outcheck
$vbox
6877 proc outcheck
{vbox
} {
6878 global stop where not_warned_yet runtime mt Unix Fname FG skipmax
6884 if {[winfo exists
$vbox] == 0} {
6885 add_log
"<verification output panel $vbox was closed>"
6889 set erline
0; set lnr
0
6890 set nomem
0; set nerr
0
6893 catch { set nt
[file mtime pan.out
] }
6894 if {$mt == $nt && $skipmax > 0} {
6899 set fd
[open pan.out r
]
6900 while {[gets $fd line
] > -1} {
6906 .inp.t tag remove hilite
0.0 end
6907 catch { $vbox delete
0.0 end
}
6910 catch { $vbox insert end
"$line\n" }
6912 catch { $vbox yview
-pickplace end
}
6915 if {[string first
"line" $line]>=0} {
6916 scan $line "\tline %d" where
6917 catch { src_line
$where }
6919 if {[string first
"State-vector" $line] == 0 \
6920 ||
([string first
"error:" $line] == 0 \
6921 && [string first
"error: max search depth too small" $line] != 0)} {
6922 set stop
1 ;# run must have completed
6923 set nerr
[string first
"errors:" $line]
6925 set part
[string range
$line $nerr end
]
6926 scan $part "errors: %d" nerr
6928 catch { .tl.results.top.title configure
\
6929 -text "Verification Result: valid" -fg $FG
6932 catch { .tl.results.top.title configure
\
6933 -text "Verification Result: not valid" -fg red
6940 if {[string first
"search depth too small" $line]>0} {
6943 if {[string first
"wrote pan_in.trail" $line]>0} {
6946 if {[string first
"violated: access to chan" $line]>0} {
6949 if {[string first
"out of memory" $line]>0} {
6952 if {[string first
"A=atomic;" $line]>0} {
6959 if {$nomem ||
$po_red_viol} { set erline
0 }
6961 if {$stop ||
($have_trail && $po_red_viol==0 && ($nerr>0 ||
$trunc>0))} {
6962 catch { $vbox yview
0.0 }
6963 add_log
"<verification done>"
6964 if {$nerr > 0 ||
$trunc == 1 ||
$nomem == 1} {
6965 if {[file exists pan_in.trail
]} {
6966 cpfile pan_in.trail
$Fname.trail
6967 } elseif
{[file exists pan_in.tra
]} {
6968 cpfile pan_in.tra
$Fname.trail
6970 catch { repeatbox
$nerr $trunc $nomem }
6973 if {$not_warned_yet} {
6976 set line
"Running verification -- waiting for output"
6977 catch { $vbox insert end
"$line\n" }
6978 set line
"\t(kill background process 'pan' to abort run)"
6979 catch { $vbox insert end
"$line\n" }
6981 set line
"\t(use ctl-alt-del to kill pan)"
6982 catch { $vbox insert end
"$line\n" }
6984 set line
"\t(use /bin/ps to find pid; then: kill -2 pid)"
6985 catch { $vbox insert end
"$line\n" }
6986 catch { $vbox yview
-pickplace end
}
6988 set not_warned_yet
0
6995 if {$runtime%60 == 0} {
6996 set rt
[expr $runtime / 60]
6997 add_log
"verification now running for approx $rt min.."
7001 after 5000 outcheck
$vbox
7010 .inp.t tag add hilite
$tgt_lnr.0 $tgt_lnr.end
7011 .inp.t tag configure hilite
-background $FG -foreground $BG
7012 if {$tgt_lnr > 10} {
7013 .inp.t yview
-pickplace [expr $tgt_lnr-10]
7015 .inp.t yview
-pickplace [expr $tgt_lnr-1]
7020 proc repeatbox
{ {nerr
} {trunc
} {nomem
}} {
7021 global s_typ PlaceWarn whichsim
7023 if {$nerr <= 0 && $trunc <= 0 && $nomem <= 0} { return }
7025 catch {destroy .rep
}
7028 wm title .rep
"Suggested Action"
7029 wm iconname .rep
"Suggest"
7030 wm geometry .rep
$PlaceWarn
7031 button .rep.b0
-text "Close" -command {destroy .rep
}
7032 button .rep.b1
-text "Run Guided Simulation.." \
7033 -command {destroy .rep
; Rewind
}
7034 button .rep.b2
-text "Setup Guided Simulation.." \
7035 -command {destroy .rep
; simulation
}
7038 message .rep.t
-width 500 -text "\
7039 Optionally, repeat the run with a different search\
7040 depth to find a shorter path to the error.
7042 Or, perform a GUIDED simulation to retrace\
7043 the error found in this run, and skip\
7044 the first series of steps if the error was\
7045 found at a depth greater than about 100 steps)."
7049 pack append .rep .rep.t
{top expand fill
}
7050 pack append .rep .rep.b0
{right
}
7051 pack append .rep .rep.b1
{right
}
7052 pack append .rep .rep.b2
{right
}
7056 message .rep.t
-width 500 -text "\
7057 Make sure the Physical Memory parameter (under Advanced\
7058 Options) is set to the maximum physical memory available.\
7059 If not, repeat the verification with the true maximum.\
7060 (Don't set it higher than the physical limit though.)\
7061 Otherwise, use compression, or switch to a\
7062 Supertrace Verification."
7067 message .rep.t
-width 500 -text "\
7068 If the search was incomplete (truncated)\
7069 because the max search depth was too small,\
7070 try to increase the depth limit (it is set\
7071 in Advanced Options of the Verification Parameters\
7072 Panel), and repeat the verification."
7075 pack append .rep .rep.t
{top expand fill
}
7076 pack append .rep .rep.b0
{right
}
7080 # Main startup and arg processing
7081 # this is at the end - to make sure all
7082 # proc declarations were seen
7086 wm title .
"SPIN CONTROL $xversion -- File: $Fname"
7088 cpfile
$argv.trail pan_in.trail