projects / lttv.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
blame | history | raw | HEAD
convert from svn repository: remove tags directory
[lttv.git] / trunk / verif / Spin / Xspin5.1 / xspin510.tcl
1 #!/bin/sh
2 # the next line restarts using wish \
3 exec wish c:/cygwin/bin/xspin -- $*
4
5 # cd ;# enable to cd to home directory by default
6
7 # on PCs:
8 # adjust the first argument to wish above with the name and
9 # location of this tcl/tk file on your system, if different.
10 #
11 # Cygwin:
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
15 #
16 # on Unix/Linux/Solaris systems
17 # replace the first line with something like
18 # #!/usr/bin/wish -f
19 # using the pathname for the wish executable on your system
20
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"
27
28 # -- Xspin Installation Notes (see also README.html):
29
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
33 #
34 # 2. If you use another C compiler than gcc, change the set CC line below
35 #
36 # 3. Browse the configurable options below if you would like to
37 # change or adjust the visual appearance of the GUI
38 #
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
42
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
46 set CC0 "gcc"
47
48 # set CPP "cpp" ;# the normal default C preprocessor
49 set CPP "gcc -E -x c" ;# c preprocessor, assuming we have gcc
50
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
60
61 set debug_on 0
62 if {$debug_on} {
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
69 }
70 proc debug {txt} {
71 global debug_on
72 if {$debug_on} {
73 catch { .debug.txt insert end "\n$txt" }
74 } }
75
76 if [info exists tcl_platform] {
77 set sys $tcl_platform(platform)
78 # if {$sys == "macintosh"} {
79 # ... no adjustments needed? ...
80 # }
81 if {[string match windows $sys]} {
82 set Unix 0 ;# means Windows95/98/2000/NT/XP
83
84 # if {[auto_execok cl] != ""} {
85 # set CC "cl -w -nologo" ;# Visual Studio compiler, PCs
86 # set CC0 "cl"
87 # }
88
89 if {$tcl_platform(os) == "Windows 95"} {
90 set CMD "command.com" ;# Windows95
91 } else {
92 set CMD "cmd"
93 set NT 1
94 } } }
95
96 #-- GUI configuration options - by Leszek Holenderski <lhol@win.tue.nl>
97 #-- basic text size:
98 set HelvBig -Adobe-Helvetica-Medium-R-Normal--*-120-*-*-*-*-*-*
99 # mscs:
100 if {$NT} { ;# on a windows nt machine
101 set SmallFont "-*-Courier-Bold-R-Normal--*-110-*"
102 set BigFont "-*-Courier-Bold-R-Normal--*-110-*"
103 } else {
104 set SmallFont "-*-Courier-Bold-R-Normal--*-80-*"
105 set BigFont "-*-Courier-Bold-R-Normal--*-80-*"
106 }
107
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).
114
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.
121
122 # When setting configuration options in an .xspinrc file, convert the
123 # settings below to the format of an X11 resource file. For example,
124 #
125 # # width of scrollbars (any Tk dimension, default 15 pixels)
126 # option add *Scrollbar.width 13 startupFile
127 #
128 # should be converted to
129 #
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
134 #
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)
138
139 option add *Scrollbar.side left startupFile
140
141 #--- sizes
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
157 #--- colors
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
170 #--- fonts
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
176
177 #--- widgets
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
182
183 # sections (decorated frames for grouping related buttons)
184 option add *Section*Title.font -*-Helvetica-Bold-R-Normal--*-100-* startupFile
185
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
189
190 ################ end of configurable parameters #######################
191
192 wm title . "SPIN CONTROL $xversion"
193 wm iconname . "SPIN"
194 wm geometry . +41+50
195 wm minsize . 400 200
196
197 set Fname ""
198 set firstime 1
199 set notignored 0
200
201 #### seed the advanced parameters settings
202
203 set e(0) "Physical Memory Available (in Mbytes): "
204 set ival(0) 128
205 set expl(0) "explain"
206
207 set e(1) "Estimated State Space Size (states x 10^3): "
208 set ival(1) 500
209 set expl(1) "explain"
210
211 set e(2) "Maximum Search Depth (steps): "
212 set ival(2) 10000
213 set expl(2) "explain"
214
215 set e(7) "Nr of hash-functions in Bitstate mode: "
216 set ival(7) 2
217 set expl(7) "explain"
218
219 set e(3) "Extra Compile-Time Directives (Optional): "
220 set ival(3) ""
221 set expl(3) "Choose"
222
223 set e(4) "Extra Run-Time Options (Optional): "
224 set ival(4) ""
225 set expl(4) "Choose"
226
227 set e(5) "Extra Verifier Generation Options: "
228 set ival(5) ""
229 set expl(5) "Choose"
230
231 set ival(6) 1 ;# which error is reported, default is 1st
232
233
234 # allow no more than one entry per selection
235 catch { tk_listboxSingleSelect Listbox }
236
237 proc msg_file {f nowarn} {
238 set msg ""
239 set ef [open $f r]
240
241 while {[gets $ef line] > -1} {
242 if {$nowarn} {
243 if {[string first "warning" $line] < 0} {
244 set msg "$msg\n$line"
245 }
246 } else {
247 set msg "$msg\n$line"
248 } }
249 close $ef
250 return $msg
251 }
252
253 scan $tk_version "%d.%d" tk_major tk_minor
254
255 set version ""
256
257 if {[auto_execok $SPIN] == "" \
258 || [auto_execok $SPIN] == 0} {
259 set version "Error: No executable $SPIN found..."
260 } else {
261 if {$Unix} {
262 set version [exec $SPIN -V]
263 } else {
264 catch { exec $SPIN -V >&pan.tmp } err
265 if {$err == ""} {
266 set version [msg_file pan.tmp 1]
267 } else {
268 puts "error: $err"
269 puts "is there a $SPIN and a go32.exe?"
270 exit
271 } }
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"
276 }
277 }
278
279 frame .menu
280 # top level menu bar
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
290
291 set lno 1
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]
300 }
301
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
308 }
309
310 menubutton .menu.help -text "Help" -relief raised \
311 -menu .menu.help.m
312
313 pack append .menu \
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}
324
325 set loglines 5
326 frame .log
327 text .log.t -bd 2 -height $loglines -background $FG -foreground $BG
328 frame .log.b
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}
337
338 proc dopaste {} {
339 global FG BG
340 set from [.inp.t index insert]
341 tk_textPaste .inp.t
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
345 }
346
347 #- fetch the value of user-defined configuration options
348
349 proc fetchOption {name default args} {
350
351 set class Dummy
352 set fullName $name
353
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]
360 }
361
362 # create a unique dummy frame of requested class and get the option's value
363 set dummy .0
364 while {[winfo exists $dummy]} { append dummy 0 }
365 frame $dummy -class $class
366 set value [option get $dummy $name $class]
367 destroy $dummy
368
369 # option not defined ?
370 switch -- $value "" { return $default }
371
372 # check a restriction on option's value
373 switch [llength $args] {
374 0 { # no restriction
375 }
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
381 }
382 }
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 }
388 }
389 default {
390 error "internal error in fetchOption: wrong restriction \"$args\""
391 }
392 }
393
394 return $value
395 }
396
397 # width of borders
398 set BD [fetchOption borderWidth 1 0 4]
399 #option add *Text.highlightThickness $BD startupFile
400
401 # scrollbar's side
402 set scrollbarSide [fetchOption Scrollbar.side right {left right}]
403
404 frame .inp
405 # view of spin input
406 scrollbar .inp.s -command ".inp.t yview"
407 text .inp.t -bd 2 -font $HelvBig -yscrollcommand ".inp.s set" -wrap word
408
409 pack .inp.s -side $scrollbarSide -fill y
410 pack append .inp \
411 .inp.t {left expand fill}
412
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" \
419 -command {dopaste}
420
421 bind .inp.t <ButtonPress-3> {
422 tk_popup .inp.t.edit %X %Y
423 }
424 bind .inp.t <ButtonRelease-1> { setlno }
425
426
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
431
432 menu .menu.file.m
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"
445
446 menu .menu.help.m
447 .menu.help.m add command -label "About Spin" \
448 -command "aboutspin"
449 .menu.help.m add separator
450 .menu.help.m add command -label "Promela Usage" \
451 -command "promela"
452 .menu.help.m add command -label "Xspin Usage" \
453 -command "helper"
454 .menu.help.m add command -label "Simulation" \
455 -command "roadmap1"
456 .menu.help.m add command -label "Verification" \
457 -command "roadmap2"
458 .menu.help.m add command -label "LTL Formulae" \
459 -command "roadmap4"
460 .menu.help.m add command -label "Spin Automata View" \
461 -command "roadmap5"
462 .menu.help.m add command -label "Reducing Complexity" \
463 -command "roadmap3"
464
465 menu .menu.run.m
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.." \
472 -command simulation
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.." \
477 -command "basicval"
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.." \
482 -command call_tl
483 .menu.run.m add separator
484 .menu.run.m add command -label "View Spin Automaton for each Proctype.." \
485 -command fsmview
486
487
488 menu .menu.edit.m
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}
495
496 set FSz 110
497
498 menu .menu.view.m
499 .menu.view.m add command -label "Larger" \
500 -command {
501 incr FSz 10
502 set HelvBig "-Adobe-Helvetica-Medium-R-Normal--*-$FSz-*-*-*-*-*-*"
503 .inp.t configure -font $HelvBig
504 }
505 .menu.view.m add command -label "Default text size" \
506 -command {
507 set FSz 110
508 set HelvBig "-Adobe-Helvetica-Medium-R-Normal--*-$FSz-*-*-*-*-*-*"
509 .inp.t configure -font $HelvBig
510 }
511 .menu.view.m add command -label "Smaller" \
512 -command {
513 incr FSz -10
514 set HelvBig "-Adobe-Helvetica-Medium-R-Normal--*-$FSz-*-*-*-*-*-*"
515 .inp.t configure -font $HelvBig
516 }
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"
522
523 proc setlno {} {
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
528 update
529 }
530
531 proc add_log {{y ""}} {
532
533 if {$y == "\n"} { return }
534 .log.t insert end "\n$y"
535 .log.t yview -pickplace end
536 }
537
538 proc cleanup {how} {
539 global Unix
540 if {$Unix == 0 && $how == 1} {
541 add_log "removing temporary files, please wait.."; update
542 }
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.." }
548 }
549
550
551 pack append . \
552 .log {bot frame w fillx} \
553 .inp {bot frame w expand fill} \
554 .menu {top fillx}
555
556 # simulation parameters - initial settings
557 set fvars 1
558 set msc 1; set svars 1
559 set rvars 1
560 set stop 0; set tsc 0
561 set seed "1"; # random sumulation
562 set jumpsteps "0"; # guided simulation
563
564 set s_typ 0
565 # meaning s_type values:
566 # 0 - Random Simulation (using seed)
567 # 1 - Guided Simulation (using pan.trail)
568 # 2 - Interactive Simulation
569
570 set whichsim 0
571 # meaning of whichsim values:
572 # 0 - use pan_in.tra(il)
573 # 1 - use user specified file
574
575 tkwait visibility .log
576 add_log "SPIN LOG:"
577 add_log " $version"
578 add_log "Xspin Version $xversion"
579 add_log "TclTk Version [info tclversion]/$tk_version\n"
580
581 if {$Unix == 0} {
582 if {[auto_execok $CC0] == "" \
583 || [auto_execok $CC0] == 0} {
584 set m "Error: no C compiler found: $CC"
585 add_log $m
586 catch { tk_messageBox -icon info -message $m }
587 }}
588
589 .inp.t configure -background $BG -foreground $FG
590
591 # process execution barchart
592
593 set Data(0) 0
594 set Name(0) "-"
595 set n 0
596 set bar_handle 0
597 set PlaceBar ""
598
599 proc stopbar {} {
600 global Data Name n PlaceBar
601 for {set i 0} {$i <= $n} {incr i} {
602 set Data($i) 0
603 set Name($i) ""
604 }
605 set n 0
606 set PlaceBar [wm geometry .bar]
607 set k [string first "\+" $PlaceBar]
608 if {$k > 0} {
609 set PlaceBar [string range $PlaceBar $k end]
610 }
611 catch { destroy .bar }
612 }
613
614 proc growbar {v} {
615 global n Data
616 set Data($n) $v
617 incr n
618 catch { fillbar }
619 }
620
621 proc shrinkbar {} {
622 global n
623 incr n -1
624 set Data($n) 0
625 catch { fillbar }
626 }
627
628 proc stepbar {v nm} {
629 global n Data Name
630
631 if {$v >= 0} {
632 if { [info exists Data($v)] } {
633 incr Data($v)
634 } else {
635 set Data($v) 1
636 }
637 if {$v >= $n} {
638 set n [expr $v+1]
639 }
640 if { [string length $nm] > 4} {
641 set Name($v) [string range $nm 0 4]
642 } else {
643 set Name($v) $nm
644 }
645 catch { fillbar }
646 }
647 }
648
649 proc adjustbar {v w} {
650 global Data
651
652 set Data($v) $w
653 catch { fillbar }
654 }
655
656 proc startbar {tl} {
657 global n Data bar_handle Ptype PlaceBar
658
659 catch { destroy .bar }
660 toplevel .bar
661 wm minsize .bar 200 200
662 wm title .bar "$tl"
663
664 set maxy [expr [winfo screenheight .] - 200]
665 if {$PlaceBar == ""} {
666 set PlaceBar "+[expr [winfo rootx .]+150]+$maxy"
667 }
668 wm geometry .bar $PlaceBar
669
670 set bar_handle [canvas .bar.c -height 410 -width 410 -relief raised]
671 frame .bar.buts
672
673 button .bar.buts.s1 -text "Save in: panbar.ps" \
674 -command ".bar.c postscript -file panbar.ps -colormode $Ptype"
675
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}
679 }
680
681 proc fillbar {} {
682 global n Data Name
683
684 .bar.c delete grid
685 .bar.c delete data
686 set sum 0
687 for {set i 0} {$i < $n} {incr i} {
688 if { [info exists Data($i)] } {
689 incr sum $Data($i)
690 } else {
691 set Data($i) 0
692 set Name($i) "-"
693 }
694 }
695 for {set i 0} {$i < $n} {incr i} {
696 .bar.c create line \
697 $i 0 \
698 $i 100 \
699 -fill #222222 -tags grid
700 .bar.c create text $i 105 \
701 -text $i -tags grid
702 .bar.c create text $i 110 \
703 -text "$Name($i)" \
704 -fill blue -tags grid
705
706 if { [info exists Data($i)] } {
707 set y [expr ($Data($i)*100)/$sum]
708 .bar.c create line \
709 $i 100 \
710 $i [expr 100-$y] \
711 -width 35 -fill red -tags data
712 if {$y > 6} {
713 set nrcol "yellow"
714 } else {
715 set nrcol "red"
716 }
717 .bar.c create text $i 95 \
718 -text "$Data($i)" \
719 -fill $nrcol -tags grid
720 }
721 }
722
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
728 if {$n <= 5} {
729 .bar.c move all 100 60
730 } else {
731 .bar.c move all 50 60
732 }
733 }
734
735 proc barscales {} {
736 global bar_handle
737
738 catch {
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}
746 }
747 }
748
749 # Files and Generic Boxes
750
751 set file ""
752 set boxnr 0
753
754 proc rmfile {f} {
755 global Unix CMD tk_major tk_minor
756
757 set err ""
758 catch { eval file delete -force $f } err
759 if {$err == "" } { return }
760
761 if {$Unix} {
762 catch {exec rm -f $f}
763 } else {
764 set n [llength $f]
765 for {set i 0} {$i < $n} {incr i} {
766 set g [lindex $f $i]
767 add_log "rm $g"
768 if {$tk_major >= 4 && $tk_minor >= 2} {
769 catch {exec $CMD /c del $g}
770 } else {
771 catch {exec $CMD >&@stdout /c del $g}
772 }
773 } }
774 }
775
776 proc mvfile {f g} {
777 global Unix CMD tk_major tk_minor
778
779 set err ""
780 catch { file rename -force $f $g } err
781 if {$err == "" } { return }
782
783 if {$Unix} {
784 catch {exec mv $f $g}
785 } else {
786 if {$tk_major >= 4 && $tk_minor >= 2} {
787 catch {exec $CMD /c move $f $g}
788 } else {
789 catch {exec $CMD >&@stdout /c move $f $g}
790 }
791 }
792 }
793
794 proc cpfile {f g} {
795 global Unix CMD tk_major tk_minor
796
797 set err ""
798 catch { file copy -force $f $g } err
799 if {$err == "" } { return }
800
801 if {$Unix} {
802 catch {exec cp $f $g}
803 } else {
804 if {$tk_major >= 4 && $tk_minor >= 2} {
805 catch {exec $CMD /c copy $f $g}
806 } else {
807 catch {exec $CMD >&@stdout /c copy $f $g}
808 } }
809 }
810
811 proc cmpfile {f g} {
812 global Unix
813
814 set err ""
815 if {$Unix} {
816 catch {exec cmp $f $g} err
817 } else {
818 if {[file exists $f] == 0 \
819 || [file exists $g] == 0} {
820 return "error"
821 }
822 set fd1 [open $f r]
823 set fd2 [open $g r]
824 while {1} {
825 set n1 [gets $fd1 line1]
826 set n2 [gets $fd2 line2]
827 if {$n1 != $n2 \
828 || [string compare $line1 $line2] != 0} {
829 set err "files differ"
830 break
831 }
832 if {$n1 < 0} { break }
833 }
834 close $fd1
835 close $fd2
836 }
837 return $err
838 }
839
840 proc file_ok {f} {
841 if {[file exists $f]} {
842 if {![file isfile $f] || ![file writable $f]} {
843 set m "error: file $f is not writable"
844 add_log $m
845 catch { tk_messageBox -icon info -message $m }
846 return 0
847 } }
848 return 1
849 }
850
851 proc mkpan_in {} {
852 global HasNever
853 set fd [open pan_in w]
854
855 fconfigure $fd -translation lf
856 puts $fd [.inp.t get 0.0 end] nonewline
857
858 if {$HasNever != ""} {
859 if [catch {set fdn [open $HasNever r]} errmsg] {
860 add_log $errmsg
861 catch { tk_messageBox -icon info -message $errmsg }
862 } else {
863 while {[gets $fdn line] > -1} {
864 puts $fd $line
865 }
866 catch "close $fdn"
867 } }
868 catch "flush $fd"
869 catch "close $fd"
870 }
871
872 proc no_ltlchange {} {
873
874 if {![file exists pan.ltl]} {
875 return 1
876 }
877 if {![file exists pan.otl]} {
878 cpfile pan.ltl pan.otl
879 return 0 ; first time
880 }
881 set err [cmpfile pan.ltl pan.otl]
882 if {[string length $err] > 0} {
883 cpfile pan.ltl pan.otl
884 return 0 ;# different
885 }
886 return 1 ;# unchanged
887 }
888
889 proc no_change {} {
890 global nv_typ
891
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
896 }
897 set err [cmpfile pan_in pan.oin]
898 if {[string length $err] > 0} {
899 cpfile pan_in pan.oin
900 return 0 ;# different
901 }
902 if {$nv_typ == 0} {
903 return 1
904 }
905 return [no_ltlchange] ;# unchanged
906 }
907
908 proc mk_exec {} {
909 global Unix CC SPIN notignored
910
911 set nochange [no_change]
912 if {$nochange == 1 && [file exists "pan"]} {
913 add_log "<no recompilation needed>"
914 return 1
915 }
916
917 add_log "<compiling executable>"
918 catch {
919 warner "Compiling" "Please wait until compilation of the \
920 executable produced by spin completes." 300
921 }
922 add_log "$SPIN -a pan_in"
923
924 catch {exec $SPIN -a pan_in >&pan.tmp}
925 set errmsg [msg_file pan.tmp 1]
926
927 if {[string length $errmsg]>0} {
928 add_log "$errmsg"
929 catch { tk_messageBox -icon info -message $errmsg }
930 add_log "<stopped compilation attempt>"
931 catch { destroy .warn }
932 return 0
933 }
934
935 add_log "$CC -o pan -D_POSIX_SOURCE pan.c"; update
936 if {$Unix} {
937 catch { eval exec $CC -o pan -D_POSIX_SOURCE pan.c >pan.tmp 2>pan.err} errmsg
938 } else {
939 catch { eval exec $CC -o pan -D_POSIX_SOURCE pan.c >pan.tmp 2>pan.err}
940 }
941 set errmsg [msg_file pan.tmp 0]
942 set errmsg "$errmsg \n [msg_file pan.err 0]"
943
944 if {[string length $errmsg]>0 && $notignored} {
945 add_log "$errmsg"
946 catch { tk_messageBox -icon info -message $errmsg }
947 catch { destroy .warn }
948 return 0
949 }
950 add_log "<compilation complete>"
951 catch {destroy .warn}
952 return 1
953 }
954
955 set PlaceWarn "+20+20"
956
957 proc warner {banner msg w} {
958 global PlaceWarn
959
960 catch {destroy .warn}
961 toplevel .warn
962
963 wm title .warn "$banner"
964 wm iconname .warn "Info"
965 set k [string first "\+" $PlaceWarn]
966 if {$k > 0} {
967 set PlaceWarn [string range $PlaceWarn $k end]
968 }
969 wm geometry .warn $PlaceWarn
970
971 message .warn.t -width $w -text $msg
972 button .warn.ok -text "Ok" \
973 -command "set PlaceWarn [wm geometry .warn]; destroy .warn"
974
975 pack append .warn .warn.t {top expand fill}
976 pack append .warn .warn.ok {bottom}
977
978 update
979 }
980
981 proc dosave {} {
982 global Fname xversion
983
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
988 catch "flush $fd"
989 catch "close $fd"
990 wm title . "SPIN CONTROL $xversion -- File: $Fname"
991 }
992
993 proc save_spec {{curr 1}} {
994 #-
995 #- Save the input area into a file.
996 #-
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.
1000 #-
1001
1002 global Fname
1003
1004 if $curr {
1005 switch -- $Fname "" {
1006 add_log "no file to save to, try \"Save as ...\""
1007 return
1008 }
1009 writeoutfile .inp.t $Fname
1010 } else {
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"
1015 } default {
1016 set fileselect "tk_getSaveFile"
1017 }
1018
1019 # get the file (return if the file selection dialog canceled)
1020 switch -- [set file [eval $fileselect]] "" return
1021
1022 # write the file and update Fname if the file written successfully
1023 if [writeoutfile .inp.t $file] {
1024 set Fname $file
1025 }
1026 }
1027 }
1028
1029 proc consider_it {} {
1030 global file Fname xversion
1031
1032 if {[file isdirectory $file]} then {
1033 cd $file
1034 fillerup ""
1035 add_log "cd $file"
1036 } else {
1037 if {![file isfile $file]} {
1038 set file ""
1039 } else {
1040 readinfile .inp.t $file
1041
1042 rmfile pan_in.trail
1043 cpfile $file.trail pan_in.trail
1044
1045 set dir [pwd]
1046 set Fname $file
1047 wm title . "SPIN CONTROL $xversion -- File: $Fname"
1048 destroy .b
1049 } }
1050 }
1051
1052 #----------------------------------------------------------------------
1053 # Improvements - by Leszek Holenderski <lhol@win.tue.nl>
1054 # GUI configuration and File Selection dialogs
1055 #----------------------------------------------------------------------
1056
1057 # predefined priorities for options stored in the option data base are
1058 # widgetDefault 20
1059 # startupFile 40
1060 # userDefault 60
1061 # interactive 80
1062
1063 # most of frames are used for layout purposes so they should be invisible
1064 option add *Frame.borderWidth 0 interactive
1065
1066 proc try_with {xspinrc} {
1067
1068 if ![file exists $xspinrc] return
1069
1070 if ![file isfile $xspinrc] {
1071 puts "xspin warning: the resource file \"$xspinrc\" exists but is not\
1072 a normal file"
1073 return
1074 }
1075 if ![file readable $xspinrc] {
1076 puts "xspin warning: the resource file \"$xspinrc\" exists but is not\
1077 readable"
1078 return
1079 }
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"
1083 return
1084 }
1085 }
1086
1087 if [info exists env(HOME)] {
1088 if $Unix {
1089 try_with [file join $env(HOME) .xspinrc]
1090 } else {
1091 try_with [file join $env(HOME) xspinrc]
1092 }
1093 }
1094
1095 proc FileSelect {mode {title ""}} {
1096 switch -- $mode open - save {} default { set mode open }
1097
1098 switch $mode {
1099 open {
1100 set title Open
1101 set okButtonText Open
1102 }
1103 save {
1104 set title Save
1105 set okButtonText Save
1106 }
1107 }
1108
1109 set w .fileselect
1110 upvar #0 $w this
1111
1112 if [winfo exists $w] {
1113 wm title $w $title
1114 $this(okButton) config -text $okButtonText
1115 catch {wm geom $w $this(geom)}
1116 wm deiconify $w
1117 } else {
1118 toplevel $w -class Fileselect
1119 wm title $w $title
1120 # the minimal size is given in characters and lines (setgrid is on)
1121 wm minsize $w 14 7
1122
1123 # layout frames
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
1129
1130 # create ok/cancel buttons
1131 set okButton [button $buttons.ok -text $okButtonText \
1132 -command "FileSelect.Close $w 1"]
1133 pack $okButton -side right
1134
1135 set cancelButton [button $buttons.cancel -text Cancel \
1136 -command "FileSelect.Close $w 0"]
1137 pack $cancelButton -side left
1138
1139 MakeSameWidth "$okButton $cancelButton"
1140
1141 # create path button
1142 set pathButton $path.path
1143 global $w|currDir
1144 set pathMenu [tk_optionMenu $pathButton $w|currDir ""]
1145 pack $pathButton -side top
1146
1147 # create the list of files
1148 global scrollbarSide
1149
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
1156
1157 bind $fileList <ButtonPress-1> "FileSelect.Selected $w %x %y"
1158 bind $fileList <Double-ButtonPress-1> "FileSelect.Chosen $w %x %y"
1159
1160 set fileEntry $name.e
1161 pack [label $name.l -text File:] -side left
1162 pack [entry $fileEntry] -side right -expand yes -fill x
1163
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
1169
1170 foreach widget "$okButton $cancelButton $pathButton $fileList $scrollbar" {
1171 $widget config -highlightthickness 0
1172 }
1173
1174 wm protocol $w WM_DELETE_WINDOW [$cancelButton cget -command]
1175 }
1176
1177 # fill in the list of files
1178 if ![info exists this(path)] { set this(path) [pwd] }
1179 FileSelect.cd $w $this(path)
1180
1181 # make the dialog modal (set a grab and claim the focus)
1182
1183 set oldFocus [focus]
1184 set oldGrab [grab current $w]
1185 if {$oldGrab != ""} { set grabStatus [grab status $oldGrab] }
1186 grab $w
1187 focus $this(fileEntry)
1188
1189 # make the contents of file entry selected (for easy deletion)
1190 $this(fileEntry) select from 0
1191 $this(fileEntry) select to end
1192
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.
1198
1199 global $w|response
1200 tkwait variable $w|response
1201 catch {focus $oldFocus}
1202 grab release $w
1203 set this(geom) [wm geom $w]
1204 wm withdraw $w
1205 if {$oldGrab != ""} {
1206 if {$grabStatus == "global"} {
1207 grab -global $oldGrab
1208 } else {
1209 grab $oldGrab
1210 }
1211 }
1212 return [set $w|response]
1213 }
1214
1215 proc CompareNoCase {s1 s2} {
1216 return [string compare [string tolower $s1] [string tolower $s2]]
1217 }
1218
1219 proc FileSelect.LoadFiles {w} {
1220 upvar #0 $w this
1221
1222 # split all names in the current directory into dirs and files
1223 set dirs ""
1224 set files ""
1225 set filter ""
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
1232 lappend dirs $f
1233 }
1234 if [file isfile $f] {
1235 # filter files
1236 switch -glob -- $f $filter { lappend files $f }
1237 }
1238 }
1239
1240 # Fill in the file list
1241 $this(fileList) delete 0 end
1242 foreach d $dirs {
1243 # append directory mark to the name (tricky)
1244 set d [string trimright [file join $d a] a]
1245 $this(fileList) insert end $d
1246 }
1247 foreach f $files { $this(fileList) insert end $f }
1248 }
1249
1250 proc FileSelect.LoadPath {w} {
1251 upvar #0 $w this
1252
1253 # convert path to list
1254 set dirs [file split $this(path)]
1255
1256 # compute prefix paths
1257 set path ""
1258 set paths ""
1259 foreach d $dirs {
1260 set path [file join $path $d]
1261 lappend paths $path
1262 }
1263
1264 # reverse dirs and paths
1265 set rev_dirs ""
1266 foreach d $dirs { set rev_dirs [concat [list $d] $rev_dirs] }
1267 set rev_paths ""
1268 foreach p $paths { set rev_paths [concat [list $p] $rev_paths] }
1269
1270 # update the path menubutton
1271 global $w|currDir
1272 set $w|currDir [lindex $rev_dirs 0]
1273
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"
1278 }
1279 }
1280
1281 proc FileSelect.Selected {w x y} {
1282 upvar #0 $w this
1283
1284 # determine the selected list element
1285 set elem [$this(fileList) get [$this(fileList) index @$x,$y]]
1286 switch -- $elem "" return
1287
1288 # directories cannot be selected (they can only be chosen)
1289 if [file isdir $elem] return
1290
1291 $this(fileEntry) delete 0 end
1292 $this(fileEntry) insert end $elem
1293 }
1294
1295 proc FileSelect.Chosen {w x y} {
1296 upvar #0 $w this
1297
1298 # determine the selected list element
1299 set elem [$this(fileList) get [$this(fileList) index @$x,$y]]
1300 switch -- $elem "" return
1301
1302 # if directory then cd, otherwise close the dialog
1303 if [file isdir $elem] { FileSelect.cd $w $elem } { FileSelect.Close $w 1 }
1304 }
1305
1306 proc FileSelect.Close {w {ok 1}} {
1307 # trigger the end of dialog
1308 upvar #0 $w this $w|response response
1309 if $ok {
1310 set response [file join $this(path) [$this(fileEntry) get]]
1311 } else {
1312 set response ""
1313 }
1314 }
1315
1316 proc FileSelect.cd {w dir} {
1317 upvar #0 $w this
1318
1319 if [catch {cd $dir} errmsg] {
1320 puts "xspin warning: $errmsg"
1321 return
1322 }
1323
1324 set this(path) [pwd]
1325 FileSelect.LoadFiles $w
1326 FileSelect.LoadPath $w
1327 }
1328
1329 proc open_spec {{curr 1}} {
1330 global Fname
1331
1332 if $curr {
1333 switch -- $Fname "" {
1334 add_log "no file to reopen, try \"Open ...\""
1335 return
1336 }
1337 readinfile .inp.t $Fname
1338 } else {
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"
1343 } default {
1344 set fileselect "tk_getOpenFile"
1345 }
1346 set init_dir [pwd]
1347 # get the file (return if the file selection dialog canceled)
1348 switch -- [set file [eval $fileselect -initialdir { $init_dir } ]] "" return
1349
1350 # load the file and update some items if the file loaded successfully
1351 if [readinfile .inp.t $file] {
1352 rmfile pan_in.trail
1353 cpfile $file.trail pan_in.trail
1354 set Fname $file
1355 set_path $Fname
1356 }
1357 }
1358 }
1359
1360
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
1367 catch {cd $wd}
1368 }
1369
1370 set defname ""
1371
1372 proc loaddefault_tl {} {
1373 global Fname defname
1374
1375 if {$defname ==""} {
1376 set file2 "$Fname.ltl"
1377 } else {
1378 set file2 $defname
1379 }
1380 catch {
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
1386 }
1387 if {![file exists $file2]} {
1388 .tl.notes.t insert end "Use Load to open a file or a template."
1389 return
1390 }
1391 catch {
1392 .tl.notes.title configure -text "Notes \[file $file2]:"
1393 }
1394 readinfile .tl.never.t $file2
1395 catch { extract_defs }
1396 }
1397
1398 set suffix "ltl"
1399
1400 proc browse_tl {} {
1401 global defname suffix
1402
1403 set suffix "ltl"
1404
1405 catch {destroy .b}
1406 toplevel .b
1407 wm iconname .b "Load"
1408
1409 frame .b.top
1410 frame .b.bot
1411 scrollbar .b.top.scroll -command ".b.top.list yview"
1412 listbox .b.top.list -yscroll ".b.top.scroll set" -relief raised
1413
1414 button .b.zap -text "Cancel" -command "destroy .b"
1415 button .b.all -text "Show All Files" \
1416 -command {
1417 set suffix ""
1418 fillerup ""
1419 destroy .b.all
1420 }
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 \
1427 .b.bot.msg {left} \
1428 .b.bot.entry {left}
1429 pack append .b \
1430 .b.top {top fillx} \
1431 .b.all {left} \
1432 .b.zap {left} \
1433 .b.bot {left}
1434
1435 bind .b.bot.entry <Return> {
1436 set nd [.b.bot.entry get]
1437 if {[file isdirectory $nd]} {
1438 cd $nd
1439 fillerup $suffix
1440 add_log "cd $nd"
1441 }
1442 }
1443
1444 fillerup $suffix
1445 bind .b.top.list <Double-Button-1> {
1446 set file2 [selection get]
1447 if {[string first "---" $file2] >= 0} {
1448 # ignore
1449 } elseif {[string first "Invariance" $file2] >= 0} {
1450 catch {
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
1456
1457 .tl.main.e1 insert end "\[\] (p)"
1458 .tl.notes.t insert end "'p' is invariantly true throughout
1459 an execution"
1460 .tl.notes.title configure \
1461 -text "Notes \[template $file2]:"
1462 do_ltl
1463 destroy .b
1464 }
1465 } elseif {[string first "Response" $file2] >= 0} {
1466 catch {
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
1472
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]:"
1479 do_ltl
1480 destroy .b
1481 }
1482 } elseif {[string first "Precedence" $file2] >= 0} {
1483 catch {
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
1489
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]:"
1497 do_ltl
1498 destroy .b
1499 }
1500 } elseif {[string first "Objective" $file2] >= 0} {
1501 catch {
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
1507
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."
1514
1515 .tl.notes.title configure \
1516 -text "Notes \[template $file2]:"
1517 do_ltl
1518 destroy .b
1519 }
1520 } elseif {[file isdirectory $file2]} then {
1521 cd $file2
1522 fillerup $suffix
1523 add_log "cd $file2"
1524 } else {
1525 if {![file isfile $file2]} {
1526 set file2 ""
1527 } else {
1528 catch {
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]:"
1536 }
1537 readinfile .tl.never.t $file2
1538 set defname $file2
1539 catch { extract_defs }
1540 set dir [pwd]
1541 destroy .b
1542 }
1543 }
1544 }
1545 }
1546
1547 proc reopen {} {
1548 global Fname
1549
1550 catch {readinfile .inp.t $Fname} ermsg
1551 if {[string length $ermsg]<=1} { return }
1552 add_log $ermsg
1553 catch { tk_messageBox -icon info -message $ermsg }
1554 }
1555
1556 proc check_xsp {f} {
1557 set ff ${f}.xsp
1558 if [catch {set fd [open $ff r]} errmsg] {
1559 # add_log "no file $ff"
1560 return
1561 }
1562 add_log "reading $ff file"
1563 update
1564 while {[gets $fd line] > -1} {
1565 if {[string first "X:" $line] == 0} {
1566 set C [string range $line 3 end]
1567 add_log "X: $C"
1568 update
1569 catch { eval exec $C } errmsg
1570 if {$errmsg != ""} { add_log $errmsg }
1571 }
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}
1575 }
1576 }
1577 }
1578
1579 proc writeoutfile {from to} {
1580
1581 if ![file_ok $to] { return 0 }
1582
1583 if [catch {set fd [open $to w]} errmsg] {
1584 add_log $errmsg
1585 catch { tk_messageBox -icon info -message $ermsg }
1586 return 0
1587 }
1588
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]
1592 close $fd
1593 return 1
1594 }
1595
1596 proc readinfile {into from} {
1597
1598 if [catch {set fd [open $from r]} errmsg] {
1599 add_log $errmsg
1600 catch { tk_messageBox -icon info -message $ermsg }
1601 return 0
1602 }
1603
1604 $into delete 0.0 end
1605 while {[gets $fd line] > -1} { $into insert end $line\n }
1606 catch { close $fd }
1607 add_log "<open $from>"
1608
1609 global LastGenerate
1610 set LastGenerate "" ;# used in Validation.tcl
1611 return 1
1612 }
1613
1614 proc fillerup {suffix} {
1615 wm title .b [pwd]
1616 .b.top.list delete 0 end
1617
1618 set dotdot 0
1619 set l {}
1620 catch { if {$suffix != ""} {
1621 set l [lsort [glob *.$suffix]]
1622 } else {
1623 set l [lsort [glob *]]
1624 } }
1625 foreach i $l {
1626 .b.top.list insert end $i
1627 if {$i == ".."} { set dotdot 1 }
1628 }
1629 if {$dotdot == 0} {
1630 .b.top.list insert 0 ".."
1631 }
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:-----"
1639 }
1640 }
1641
1642 proc gotoline {} {
1643 global BG FG
1644
1645 catch { destroy .ln }
1646 toplevel .ln
1647 wm title .ln "Goto Line"
1648 wm iconname .ln "Goto"
1649
1650 label .ln.lab -text "Enter line number:"
1651 entry .ln.ent -width 20 -relief sunken -textvariable lno
1652 pack append .ln \
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]
1661 }
1662 focus .ln.ent
1663 }
1664
1665 proc savebox {b} {
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
1671 catch "flush $fd"
1672 catch "close $fd"
1673 }
1674
1675 proc doplace {a b} {
1676 global PlaceBox
1677 set PlaceBox($a) [wm geometry .c$b]
1678 set k [string first "\+" $PlaceBox($a)]
1679 if {$k > 0} {
1680 set PlaceBox($a) [string range $PlaceBox($a) $k end]
1681 }
1682 }
1683
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
1687
1688 incr boxnr
1689
1690 toplevel .c$boxnr
1691 wm title .c$boxnr $n
1692 wm iconname .c$boxnr $m
1693
1694 if {[info exists PlaceBox($n)] == 0} {
1695 set PlaceBox($n) "+$xp+$yp"
1696 }
1697 wm geometry .c$boxnr $PlaceBox($n)
1698
1699 #initialize search parameters
1700 set ind 1.0
1701 set old_ss ""
1702 set old_insert ""
1703 set new_insert ""
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"
1709
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
1714
1715 frame .c$boxnr.z
1716
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}
1727
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}
1736
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}
1748 }
1749
1750 tkwait visibility .c$boxnr
1751 raise .c$boxnr
1752 return $boxnr
1753 }
1754 proc update_insert {t} {
1755 global new_insert
1756 update idletasks
1757 set new_insert [$t index insert]
1758 }
1759
1760 proc search_sim {t e b} {
1761 global ind old_ss old_insert new_insert
1762
1763 set ss [$e get]
1764
1765 if {$ss == ""} {
1766 return
1767 }
1768
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
1774 }
1775 set cur_ind $ind
1776 set ind [$t search $ss $ind]
1777
1778 set old_ss $ss
1779 if {$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]]
1786 set indstart $ind
1787 set indend ""
1788 append indend [lindex $split_ind 0] "." $char
1789 $t tag add hilite $indstart $indend
1790 $t tag configure hilite -foreground white -background black
1791 set ind $indend
1792 } else {
1793 # set ind 1.0
1794 catch { tk_messageBox -icon info -message "no match for $ss" }
1795 set ind $cur_ind ;# restore ind to last good value
1796 raise $b
1797 }
1798
1799 }
1800
1801 # Tcl/Tk book, page 219
1802 proc forAllMatches {w pattern} {
1803 global BG FG lno
1804
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]} {
1810 $w mark set first \
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]
1818 } }
1819
1820 # move to the next line that matches
1821
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]} {
1826 $w mark set first \
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]
1831 set lno $i
1832 return
1833 } }
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]} {
1838 $w mark set first \
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]
1843 set lno $i
1844 return
1845 } }
1846 catch {
1847 tk_messageBox -icon info -message "No Match of \"$pattern\""
1848 }
1849 }
1850
1851 set noprep 0
1852
1853 proc hasWord {pattern} {
1854 global SPIN noprep
1855 set err ""
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>"
1861 }
1862
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]} {
1867 catch "close $fd"
1868 return 1
1869 } }
1870 catch "close $fd"
1871 return 0
1872 }
1873
1874 # else, there were errors, just ignore the include files:
1875 set noprep 1
1876 add_log "$err"
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]} {
1882 return 1
1883 }
1884 }
1885 return 0
1886 }
1887
1888 # FSM view option
1889
1890 set nodeX(0) 0
1891 set nodeY(0) 0
1892 set Label(0) 0
1893 set Transit(0) {}
1894 set TLabel(0) 0
1895 set Lab2Node(0) 0
1896 set Dist(0) 0
1897 set State(0) 0
1898 set Edges(0) {}
1899 set New 0
1900 set MaxDist 0
1901 set Maxx 0
1902 set Maxy 0
1903 set Minx 50
1904 set Miny 50
1905 set reached_end 0
1906 set Scale 1
1907
1908 set cnr 0
1909 set x 0
1910 set y 0
1911
1912 proc fsmview {} {
1913 global Unix
1914
1915 add_log "<fsm view option>"
1916
1917 if {[mk_exec] != 1} { return }
1918
1919 catch {destroy .z}
1920 toplevel .z
1921
1922 wm title .z "Double-Click Proc"
1923
1924 listbox .z.list -setgrid 1
1925 button .z.b -text "Cancel" -command "destroy .z"
1926
1927 pack append .z \
1928 .z.list {top expand fill} \
1929 .z.b {right padx 5}
1930
1931 if {$Unix} {
1932 add_log "./pan -d # find proc names"; update
1933 set fd [open "|./pan -d" w+]
1934 } else {
1935 add_log "pan -d # find proc names"; update
1936 catch { eval exec pan -d >&pan.tmp } err
1937 if {$err != ""} {
1938 add_log "error: $err"
1939 }
1940 set fd [open pan.tmp r]
1941 }
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]]
1946 } }
1947 catch { close $fd }
1948
1949 bind .z.list <Double-Button-1> {
1950 set pfind [selection get]
1951 catch { destroy .z }
1952 findfsm $pfind
1953 }
1954 focus .z.list
1955 }
1956
1957 proc findfsm {pfind} {
1958 global Unix New Dist State Edges Label
1959 global Transit MaxDist reached_end TLabel DOT
1960
1961 if {[mk_exec] != 1} { return }
1962
1963 set src 0; set trn 0; set trg 0
1964 set Want 0; set MaxDist 0; set startstate ""
1965
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) } }
1969
1970 if {$Unix} {
1971 add_log "./pan -d # compute fsm"; update
1972 set fd [open "|./pan -d" w+]
1973 } else {
1974 add_log "pan -d # compute fsm"; update
1975 catch { eval exec pan -d >&pan.tmp }
1976 set fd [open pan.tmp r]
1977 }
1978 while {[gets $fd line] > -1} {
1979 set k [string first "proctype" $line]
1980 if { $k >= 0 } {
1981 if { $Want == 1 } {
1982 break
1983 }
1984 incr k 9
1985 set pname [string range $line $k end]
1986
1987 if { [string first $pfind $line] >= 0 \
1988 && [string length $pfind] == [string length $pname]} {
1989 set Want 1
1990 set reached_end 0
1991 set nsrc "$pname:0"
1992 set Dist($nsrc) 0
1993 set Label($nsrc) "end"
1994 set Edges($nsrc) {}
1995 }
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" \
2000 src trn trg
2001 if {$trg == 0} { set reached_end 1 }
2002
2003 set nsrc "$pname:$src"
2004 set ntrg "$pname:$trg"
2005
2006 if {$startstate == ""} { set startstate $nsrc }
2007
2008 set k [string first "line" $line]
2009 if { $k > 0 } {
2010 set m [string first "=>" $line]
2011 incr m -1
2012 set lbl [string range $line $k $m]
2013 incr m 3
2014 set action [string range $line $m end]
2015 } else {
2016 set lbl "line 0"
2017 set action "line 0"
2018 }
2019 set Label($nsrc) $lbl
2020 if { [info exists Dist($nsrc)] == 0 } {
2021 set Dist($nsrc) 0
2022 set Edges($nsrc) {}
2023 }
2024 if { [info exists Dist($ntrg)] == 0 } {
2025 set Dist($ntrg) [expr $Dist($nsrc) + 1]
2026 set Edges($ntrg) {}
2027 if {$Dist($ntrg) > $MaxDist } {
2028 set MaxDist $Dist($ntrg)
2029 }
2030 } else {
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)
2035 }
2036 } }
2037 if {0 \
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} {
2043 incr z1 -1; incr z2
2044 set a1 [string range $action 0 $z1]
2045 set a2 [string range $action $z2 end]
2046 set action "$a1$a2"
2047 }
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"
2055 } else {
2056 lappend Edges($nsrc) $ntrg
2057 lappend Transit($nsrc) $action
2058 }
2059 }
2060 }
2061 if { $Want == 1 } {
2062 dograph $pfind $startstate
2063 } else {
2064 add_log "sorry, $pfind not found..."
2065 catch {
2066 tk_messageBox -icon info -message "$pfind not found..."
2067 }
2068 }
2069 catch "close $fd"
2070 add_log "<done>"
2071 update
2072 }
2073
2074 proc plunknode {el prefix} {
2075 global State Label TLabel
2076 global x y
2077
2078 set pn [string range $el $prefix end]
2079 set State($el) [mkNode "$Label($el)" $pn $x $y]
2080
2081 if { $x > 250 } {
2082 set x [expr $x - 250]
2083 set x [expr 250 - $x]
2084 } else {
2085 set x [expr 250 - $x]
2086 incr x 75
2087 set x [expr 250 + $x]
2088 }
2089 }
2090
2091 proc dograph {n s} {
2092 global Dist Edges Label Transit MaxDist State ELabel
2093 global cnr lcnr reached_end x y Unix DOT
2094 set count -1
2095
2096 set lcnr [mkcanvas "FSM $n" $n 300 300 0]
2097 set prefix [string length $n]
2098 incr prefix
2099 set y 0
2100
2101 while {$count < $MaxDist} {
2102 incr count
2103 incr y 50
2104 set x 250
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
2110 } }
2111 }
2112 if {$reached_end == 1} {
2113 # force end state at the bottom
2114 incr y 50
2115 set x 250
2116 plunknode "$n:0" $prefix
2117 }
2118
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"
2126 }
2127 } }
2128 addscales $lcnr
2129
2130 .f$cnr.c itemconfigure $State($s) -outline red; update
2131
2132 if {[auto_execok $DOT] != 0 \
2133 && [auto_execok $DOT] != ""} {
2134 dodot $n
2135 # button .f$lcnr.b66 -text "Redraw with Dot" -command "dodot $n"
2136 # pack append .f$lcnr .f$lcnr.b66 {right padx 5}
2137 }
2138 update
2139 }
2140
2141 proc mkNode {n t x y} {
2142 # tcl book p. 213
2143 global cnr NodeWidth NodeHeight HelvBig
2144 global nodeX nodeY New TLabel Lab2Node
2145
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] \
2149 -outline white \
2150 -fill white \
2151 -tags node]
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]
2155 } else {
2156 set New [.f$cnr.c create oval [expr $x-10] [expr $y-10] \
2157 [expr $x+10] [expr $y+10] \
2158 -outline black \
2159 -fill white \
2160 -tags node]
2161 set Lab [.f$cnr.c create text $x $y -font $HelvBig -text $n -tags node]
2162
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} }
2166 "
2167 .f$cnr.c bind $Lab <Any-Leave> "
2168 .f$cnr.c itemconfigure {$Lab} -fill black -text {$n}
2169 "
2170 }
2171 set nodeX($New) $x
2172 set nodeY($New) $y
2173 set TLabel($New) $Lab
2174 set Lab2Node($Lab) $New
2175 set NodeWidth($New) 10
2176 set NodeHeight($New) 10
2177
2178 update
2179 return $New
2180 }
2181
2182 proc set_src {n} {
2183 set where 0
2184 scan $n "line %d" where
2185 .inp.t tag remove hilite 0.0 end
2186 src_line $where
2187 }
2188
2189 proc mkEdge {L a b} {
2190 global cnr Xrem Yrem TransLabel HelvBig
2191 global nodeX nodeY edgeHead edgeTail
2192
2193 if { $nodeY($b) > $nodeY($a) } {
2194 set ydiff -11
2195 } elseif { $nodeY($b) < $nodeY($a) } {
2196 set ydiff 11
2197 } else {
2198 set ydiff 0
2199 }
2200 if { $nodeX($b) > $nodeX($a) } {
2201 set xdiff -6
2202 } elseif { $nodeX($b) < $nodeX($a) } {
2203 set xdiff 6
2204 } else {
2205 set xdiff 0
2206 }
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
2215
2216 set Xrem($edge) $xdiff
2217 set Yrem($edge) $ydiff
2218
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 ]
2223
2224 set TransLabel($a,$b) \
2225 [.f$cnr.c create text $midX $midY -font $HelvBig -tags texttag]
2226
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
2231 "
2232 .f$cnr.c bind $edge <ButtonRelease-1> "
2233 .f$cnr.c itemconfigure $TransLabel($a,$b) \
2234 -fill black -text {}
2235 "
2236 }
2237
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
2242
2243 set x [.f$cnr.c coords $node]
2244 if {[llength $x] == 2} { set node $Lab2Node($node) }
2245
2246 set mx [.f$cnr.c canvasx $mx]
2247 set my [.f$cnr.c canvasy $my]
2248
2249 set wx $NodeWidth($node)
2250 set wy $NodeHeight($node)
2251
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
2256
2257 set nodeX($node) $mx
2258 set nodeY($node) $my
2259 if {$together == 0} { return }
2260 catch {
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 \
2266 $nx $ny \
2267 [lindex $ec 2] [lindex $ec 3]
2268 }}
2269 catch {
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] \
2276 $nx $ny
2277 }}
2278 }
2279
2280 set PlaceCanvas(msc) ""
2281
2282 proc mkcanvas {n m geox geoy placed} {
2283 global cnr tk_version
2284 global Chandle Sticky
2285 global FG BG Ptype PlaceCanvas
2286
2287 incr cnr
2288 toplevel .f$cnr
2289 wm title .f$cnr "$n"
2290 wm iconname .f$cnr $m
2291 if {$placed} {
2292 if {$PlaceCanvas($m) == ""} {
2293 set PlaceCanvas($m) "+$geox+$geoy"
2294 }
2295 set k [string first "\+" $PlaceCanvas($m)]
2296 if {$k > 0} {
2297 set PlaceCanvas($m) [string range $PlaceCanvas($m) $k end]
2298 }
2299 wm geometry .f$cnr $PlaceCanvas($m)
2300 }
2301 wm minsize .f$cnr 100 100
2302
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} \
2307 -background $BG \
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"
2314 } else {
2315 set cv [canvas .f$cnr.c -relief raised -bd 2\
2316 -scrollregion {-15c -5c 30c 40c} \
2317 -background $BG \
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"
2324 }
2325 set Chandle($cnr) $cv
2326 #-width 500 -height 500
2327
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"
2332
2333 pack append .f$cnr \
2334 .f$cnr.vscroll {right filly} \
2335 .f$cnr.hscroll {bottom fillx} \
2336 .f$cnr.c {top expand fill}
2337
2338 if {$m == "msc"} {
2339 set Sticky($cnr) 0
2340 checkbutton .f$cnr.b6 -text "Preserve" \
2341 -variable Sticky($cnr) \
2342 -relief flat
2343 pack append .f$cnr \
2344 .f$cnr.b6 { right padx 5}
2345 }
2346 pack append .f$cnr \
2347 .f$cnr.b1 {right padx 5} \
2348 .f$cnr.b2 {right padx 5}
2349
2350 bind $cv <2> "$cv scan mark %x %y" ;# Geert Janssen, TUE
2351 bind $cv <B2-Motion> "$cv scan dragto %x %y"
2352
2353 .f$cnr.c bind node <B1-Motion> "
2354 moveNode $cnr \[.f$cnr.c find withtag current] %x %y 1
2355 "
2356
2357 # .f$cnr.c bind node <B2-Motion> "
2358 # moveNode $cnr \[.f$cnr.c find withtag current] %x %y 1
2359 # "
2360
2361 tkwait visibility .f$cnr
2362 return $cnr
2363 }
2364
2365 proc addscales {p} {
2366 global Chandle Scale
2367
2368 catch {
2369 set cv $Chandle($p)
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]"
2374 pack append .f$p \
2375 .f$p.b4 {right padx 5} \
2376 .f$p.b5 {right padx 5}
2377 }
2378 }
2379
2380 proc dodot {n} {
2381 global Edges edgeHead edgeTail NodeWidth NodeHeight Maxx Maxy
2382 global State ELabel TransLabel Unix cnr lcnr Xrem Yrem DOT
2383
2384 add_log "<dot graph layout...>"
2385 set fd [open "|$DOT" w+]
2386
2387 puts $fd "digraph dodot {"
2388
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\"; "
2394 }
2395 }}
2396
2397 puts $fd "}"
2398 flush $fd
2399 set ends ""
2400 set nodot 1
2401 while {[gets $fd line] > -1} {
2402 if {[string first "\}" $line] >= 0} {
2403 break;
2404 }
2405 set dd [string length $line]; incr dd -1
2406 while {[string range $line $dd $dd] == "\\"} {
2407 gets $fd more
2408 set line "[string range $line 0 [expr $dd-1]]$more"
2409 set dd [string length $line]; incr dd -1
2410 }
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 " "]
2423 set j [llength $k]
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)
2428 if {$tp == "e"} {
2429 set ends "last"
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] "
2433 if {$i == $j2} {
2434 .f$cnr.c coords \
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"
2440 }
2441 }
2442 scan [lindex $k 0] "%d,%d" x y
2443 set coords " $coords[expr 50 + $x] [expr 50 + $Maxy - $y] "
2444 } else {
2445 set ends "first"
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] "
2449 if {$i == $j2} {
2450 .f$cnr.c coords \
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"
2456 } } }
2457 set coords "$coords -arrow $ends $spline -tags connector"
2458
2459 set ne [eval $coords]
2460 set Xrem($ne) 10
2461 set Yrem($ne) 10
2462
2463 continue
2464 }
2465 if {[string first "node " $line] >= 0 \
2466 || [string first "\{" $line] >= 0} {
2467 continue
2468 }
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]
2477 } else {
2478 set Maxx [lindex $k 0]
2479 set Maxy [lindex $k 1]
2480 }
2481 set nodot 0
2482 } else { ;# a node
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 " \""]
2488
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 ","]
2494 set x [lindex $k 0]
2495 set y [lindex $k 1]
2496
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]]
2501
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]]
2506
2507 catch {
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
2512 } err
2513 #puts $err
2514 }
2515 }
2516 catch { close $fd }
2517
2518 if {$nodot} {
2519 add_log "<cannot find dot>"
2520 catch {
2521 tk_messageBox -icon info -message "<cannot find dot>"
2522 }
2523 return
2524 }
2525
2526 foreach el [array names Edges] {
2527 if { [ string first $n $el ] >= 0 } {
2528 catch {
2529 foreach edge $edgeHead($State($el)) {
2530 .f$cnr.c delete $edge
2531 }
2532 unset edgeHead($State($el))
2533 unset edgeTail($State($el))
2534 }
2535 } }
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}
2544 }
2545
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"
2550 }
2551
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"
2556 }
2557
2558 proc trunc {p} {
2559 set foo [string first "." $p]
2560 if {$foo >= 0} {
2561 incr foo -1
2562 set p [string range $p 0 $foo]
2563 }
2564 return $p
2565 }
2566
2567 # Help menus
2568
2569 proc aboutspin {} {
2570 global FG BG HelvBig version xversion
2571
2572 catch {destroy .h}
2573 toplevel .h
2574
2575 wm title .h "About SPIN"
2576 wm iconname .h "About"
2577 message .h.t -width 600 -background $BG -foreground $FG -font $HelvBig \
2578 -text " $version
2579 Xspin Version $xversion
2580
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.
2584
2585 The master sources for the latest version of
2586 this software can always be found via:
2587
2588 http://spinroot.com/spin/whatispin.html
2589
2590 For help: spin_list@spinroot.com
2591
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.
2598 "
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}
2602 }
2603
2604 proc promela {} {
2605 global FG BG HelvBig
2606
2607 catch {destroy .h}
2608 toplevel .h
2609
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:
2614
2615 http://spinroot.com/spin/Man/index.html
2616
2617 "
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}
2621 }
2622
2623 proc helper {} {
2624 global FG BG HelvBig
2625
2626 catch {destroy .h}
2627 toplevel .h
2628
2629 wm title .h "Help with Xspin"
2630 wm iconname .h "Help"
2631 message .h.t -background $BG -foreground $FG -font $HelvBig \
2632 -text "\
2633 Spin Version Controller - (c) 1993-2004 Bell Laboratories
2634
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.
2639
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.
2644
2645 All run-time options are available through the Run menu.
2646 A typical way of working with Xspin is to use:
2647
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
2655
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.
2659
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
2664 verification run."
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}
2668 }
2669
2670 # LTL interface
2671
2672 set formula ""
2673 set tl_stat 0
2674
2675 proc put_template {s} {
2676 .tl.main.e1 delete 0 end
2677 .tl.main.e1 insert end "$s"
2678 }
2679
2680 set PlaceTL "+100+1"
2681
2682 proc call_tl {} { ;# expanded interface
2683 global formula tl_stat nv_typ an_typ cp_typ
2684 global FG BG Fname firstime PlaceTL
2685
2686 catch {destroy .tl}
2687 toplevel .tl
2688
2689 set k [string first "\+" $PlaceTL]
2690 if {$k > 0} {
2691 set PlaceTL [string range $PlaceTL $k end]
2692 }
2693
2694 wm title .tl "Linear Time Temporal Logic Formulae"
2695 wm iconname .tl "LTL"
2696 wm geometry .tl $PlaceTL
2697
2698 frame .tl.main
2699 entry .tl.main.e1 -relief sunken \
2700 -background $BG -foreground $FG
2701 label .tl.main.e2 -text "Formula: "
2702
2703 frame .tl.op
2704 set alw {\[\] }
2705 set eve {\<\> }
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}
2722
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
2729 pack append .tl.b \
2730 .tl.b.s0 {left} \
2731 .tl.b.s1 {left} \
2732 .tl.b.s2 {left}
2733
2734 .tl.main.e1 insert end $formula
2735
2736 button .tl.main.file -text "Load..." \
2737 -command "browse_tl"
2738
2739 bind .tl.main.e1 <Return> { do_ltl }
2740
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}
2745
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}
2749
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 \
2757 -setgrid 1 \
2758 -wrap word
2759
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}
2764
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 \
2772 -setgrid 1 \
2773 -wrap word
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}
2778
2779 frame .tl.never
2780 frame .tl.never.top
2781 label .tl.never.top.title -text "Never Claim:"\
2782 -relief flat
2783 button .tl.never.top.gc -text "Generate" \
2784 -command "do_ltl"
2785 pack append .tl.never.top \
2786 .tl.never.top.gc {right}\
2787 .tl.never.top.title {left}
2788
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" \
2793 -setgrid 1 \
2794 -wrap word
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}
2799
2800 frame .tl.results
2801 frame .tl.results.top
2802
2803 button .tl.results.top.svp -text "Run Verification" \
2804 -command "do_ltl; basicval2"
2805 label .tl.results.top.title -text "Verification Result:"\
2806 -relief flat
2807 pack append .tl.results.top \
2808 .tl.results.top.svp {right}\
2809 .tl.results.top.title {left}
2810
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" \
2815 -setgrid 1 \
2816 -wrap word
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}
2821
2822 pack append .tl \
2823 .tl.notes {top expand fill} \
2824 .tl.macros {top expand fill} \
2825 .tl.never {top expand fill} \
2826 .tl.results {top expand fill} \
2827
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}
2832
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}
2837
2838 loaddefault_tl
2839 focus .tl.main.e1
2840 }
2841
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]
2846 set kk [expr $k+1]
2847 .tl.never.t delete $k.0 $kk.0
2848 }
2849 }
2850
2851 proc grab_nvr {inp target} {
2852
2853 set pattern $inp
2854 scan [.tl.never.t index end] %d numLines
2855 set foo {}
2856 set yes 0
2857
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]} {
2862 lappend foo $i
2863 set yes [expr 1 - $yes]
2864 if {$yes} {
2865 set pattern "#endif"
2866 } else {
2867 set pattern $inp
2868 }
2869 }
2870 if {$yes && [string first $inp $have] != 0} {
2871 $target insert end "$have"
2872 lappend foo $i
2873 }
2874 }
2875 purge_nvr $foo
2876 }
2877
2878 proc extract_defs {} {
2879 global tl_stat
2880
2881 set pattern "#define "
2882 scan [.tl.never.t index end] %d numLines
2883 set foo {}
2884 set tl_stat 1
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"
2890 lappend foo $i
2891 }
2892 set have [.tl.never.t get last "last lineend"]
2893 set k [string first "Formula As Typed: " $have]
2894 if {$k > 0} {
2895 set ff [string range $have [expr $k+18] end]
2896 .tl.main.e1 insert end $ff
2897 }
2898 if {[string first "To The Negated Formula " $have] > 0} {
2899 set tl_stat 0
2900 }
2901 }
2902 purge_nvr $foo
2903
2904 grab_nvr "#ifdef NOTES" .tl.notes.t
2905 grab_nvr "#ifdef RESULT" .tl.results.t
2906 }
2907
2908 proc inspect_ltl {} {
2909 global formula
2910 set formula "[.tl.main.e1 get]"
2911
2912 set x $formula
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
2927
2928 set predefs " np_ true false "
2929
2930 set k [split $x " "]
2931 set j [llength $k]
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} {
2938 catch {
2939 .tl.macros.t insert end "$pattern\t?\n"
2940 }
2941 set line [.tl.macros.t get 0.0 end]
2942 } } }
2943 }
2944
2945 proc do_ltl {} {
2946 global formula tl_stat SPIN tk_major tk_minor
2947
2948 set formula "[.tl.main.e1 get]"
2949 .tl.never.t delete 0.0 end
2950 update
2951
2952 catch { inspect_ltl }
2953
2954 set MostSystems 1 ;# change to 0 only if there are problems
2955 ;# see below
2956
2957 if {$tl_stat == 0} {
2958 add_log "$SPIN -f \"!( $formula )\""
2959 if {$MostSystems} {
2960 catch {exec $SPIN -f "!($formula)" >&pan.ltl} err
2961 } else {
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
2965 }
2966 } else {
2967 add_log "$SPIN -f \"( $formula )\""
2968 if {$MostSystems} {
2969 catch {exec $SPIN -f "($formula)" >&pan.ltl} err
2970 } else {
2971 # see above
2972 catch {exec $SPIN -f \"($formula)\" >&pan.ltl} err
2973 }
2974 }
2975 set lno 0
2976
2977 if {$err != ""} {
2978 add_log "<error: $err>"
2979 add_log "hint: check the Help Button for syntax rules"
2980 } else {
2981 .tl.never.t insert end \
2982 " /*\n"
2983 .tl.never.t insert end \
2984 " * Formula As Typed: $formula\n"
2985 incr lno 2
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"
2993 incr lno 3
2994 }
2995 .tl.never.t insert end \
2996 " */\n\n"
2997 incr lno 2
2998 }
2999 catch {
3000 set fd [open pan.ltl r]
3001 while {[gets $fd line] > -1} {
3002 .tl.never.t insert end "$line\n"
3003 }
3004 close $fd
3005 }
3006 rmfile pan.ltl
3007 }
3008
3009 proc dump_tl {bb} {
3010
3011 if {$bb != ""} {
3012 set fnm $bb
3013 } else {
3014 set fnm [.sv_tl.ent get]
3015 }
3016
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 }
3021
3022 puts $fd "[.tl.never.t get 0.0 end]" nonewline
3023
3024 catch { puts $fd "#ifdef NOTES"
3025 puts $fd "[.tl.notes.t get 0.0 end]" nonewline
3026 puts $fd "#endif"
3027 }
3028 catch { puts $fd "#ifdef RESULT"
3029 puts $fd "[.tl.results.t get 0.0 end]" nonewline
3030 puts $fd "#endif"
3031 }
3032
3033 catch "flush $fd"
3034 catch "close $fd"
3035 catch "destroy .sv_tl"
3036 catch "focus .tl.main.e1"
3037 }
3038
3039 proc save_tl {} {
3040 global Fname PlaceWarn
3041 catch {destroy .sv_tl}
3042 toplevel .sv_tl
3043
3044 wm title .sv_tl "Save Claim"
3045 wm iconname .sv_tl "Save"
3046 wm geometry .sv_tl $PlaceWarn
3047
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 "" }
3053
3054 set fnm [.sv_tl.ent get]
3055 if {$fnm == ""} {
3056 .sv_tl.ent insert end "$Fname.ltl"
3057 }
3058
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}
3064 focus .sv_tl.ent
3065 }
3066
3067 proc add_tl {} {
3068 global BG FG HelvBig PlaceWarn
3069 catch {destroy .warn}
3070 toplevel .warn
3071 set k [string first "\+" $PlaceWarn]
3072 if {$k > 0} {
3073 set PlaceWarn [string range $PlaceWarn $k end]
3074 }
3075
3076 wm title .warn "Accept"
3077 wm iconname .warn "Accept"
3078 wm geometry .warn $PlaceWarn
3079
3080 message .warn.t -width 300 \
3081 -background $BG -foreground $FG -font $HelvBig \
3082 -text " \
3083 Instructions:
3084
3085 1. Save the Never Claim in a file, \
3086 for instance a file called 'never', \
3087 using the <Save> button.
3088
3089 2. Insert the line
3090
3091 #include \"never\"
3092
3093 (the name of the file with the claim) \
3094 at the end of the main specification.
3095
3096 3. Insert macro definitions (#define's) for all \
3097 propositional symbols used in the formula.
3098
3099 For instance, with LTL formula
3100 '[] p -> <> q' add the macro defs:
3101
3102 #define p (cnt == 1)
3103 #define q (cnt > 1)
3104
3105 These macros must be defined just above the line \
3106 with the #include \"never\" directive
3107
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.
3114
3115 5. Never claims have no effect during simulation runs.
3116
3117 6. See the HELP->LTL menu for more information.
3118
3119 "
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}
3124 }
3125
3126 proc roadmap4 {} {
3127 global FG BG
3128
3129 catch {destroy .h}
3130 toplevel .h
3131
3132 wm title .h "LTL Help"
3133 wm iconname .h "Help"
3134 frame .h.z
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
3140 pack append .h.z \
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.
3147
3148 Define a new LTL formula using lowercase names for the
3149 propositional symbols, for instance:
3150 [] (p U q)
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).
3157
3158 When you type a <Return> or hit the <Generate> button,
3159 the formula is translated into an equivalent never-claim.
3160
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:
3168
3169 #define p (a > b)
3170 #define q (len(q) < 5)
3171
3172 Valid temporal logic operators are:
3173 \[\] Always (no space between \[ and \])
3174 <> Eventually (no space between < and >)
3175 U (Strong) Until
3176 V The Dual of Until: (p V q) == !(!p U !q)
3177
3178 All operators are left-associative (incl. U and V).
3179
3180 Boolean Operators:
3181 && Logical And (alternative form: /\\, no spaces)
3182 ! Logical Negation
3183 || Logical Or (alternative form: \\/, no spaces)
3184 -> Logical Implication
3185 <-> Logical Equivalence
3186
3187 Boolean Predicates:
3188 true, false
3189 any name that starts with a lowercase letter
3190
3191 Examples:
3192 \[\] p
3193 !( <> !q )
3194 p U q
3195 p U (\[\] (q U r))
3196
3197 Generic properties/Templates:
3198 Invariance: \[\] p
3199 Response: p -> \<\> q
3200 Precedence: p -> (q U r)
3201 Objective: p -> \<\> (q || r)
3202
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).
3215 "
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
3221 focus .h.z.t
3222 }
3223
3224
3225
3226 # Specific Help
3227
3228 proc roadmap1 {} {
3229 global FG BG
3230
3231 catch {destroy .road1}
3232 toplevel .road1
3233
3234 wm title .road1 "Help with Simulation"
3235 wm iconname .road1 "SimHelp"
3236 frame .road1.z
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.
3248
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.
3257
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.
3262
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 .
3268
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.
3273
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;'"
3278
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
3284 focus .road1.z.t
3285 }
3286
3287 proc roadmap2a {} {
3288 global FG BG
3289
3290 catch {destroy .road2}
3291 toplevel .road2
3292
3293 wm title .road2 "Help with Verification Parameters"
3294 wm iconname .road2 "ValHelp"
3295 frame .road2.z
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.
3307
3308 When the limit is reached, the verification is stopped to
3309 avoid trashing.
3310
3311 The number entered here is the number of MegaBytes directly
3312 (not a power of two, as in previous versions of xspin).
3313
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."
3317
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
3323 focus .road2.z.t
3324 }
3325 proc roadmap2b {} {
3326 global FG BG
3327
3328 catch {destroy .road2}
3329 toplevel .road2
3330
3331 wm title .road2 "Help with Verification"
3332 wm iconname .road2 "ValHelp"
3333 frame .road2.z
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
3349 hash collisions.
3350
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.
3357
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).
3362
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."
3366
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
3372 focus .road2.z.t
3373 }
3374 proc roadmap2c {} {
3375 global FG BG
3376
3377 catch {destroy .road2}
3378 toplevel .road2
3379
3380 wm title .road2 "Help with Verification"
3381 wm iconname .road2 "ValHelp"
3382 frame .road2.z
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.
3400
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."
3405
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
3411 focus .road2.z.t
3412 }
3413
3414 proc roadmap2k {} {
3415 global FG BG
3416
3417 catch {destroy .road2}
3418 toplevel .road2
3419
3420 wm title .road2 "Help with Verification"
3421 wm iconname .road2 "ValHelp"
3422 frame .road2.z
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."
3438
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
3444 focus .road2.z.t
3445 }
3446
3447 proc roadmap2d {} {
3448 global FG BG
3449
3450 catch {destroy .road2}
3451 toplevel .road2
3452
3453 wm title .road2 "Help with Verification"
3454 wm iconname .road2 "ValHelp"
3455 frame .road2.z
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.
3471
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.
3481
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.
3486
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."
3491
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
3497 focus .road2.z.t
3498 }
3499
3500 proc roadmap2e {} {
3501 global FG BG
3502
3503 catch {destroy .road2}
3504 toplevel .road2
3505
3506 wm title .road2 "Help with Verification"
3507 wm iconname .road2 "ValHelp"
3508 frame .road2.z
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.
3523
3524 => Safety properties are properties of single states (like\
3525 deadlocks = invalid endstates, or assertion violations).
3526
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).
3533
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\
3537 active processes.
3538
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.
3543
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)."
3547
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
3553 focus .road2.z.t
3554 }
3555
3556 proc roadmap2f {} {
3557 global FG BG
3558
3559 catch {destroy .road2}
3560 toplevel .road2
3561
3562 wm title .road2 "Help with Verification"
3563 wm iconname .road2 "ValHelp"
3564 frame .road2.z
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.
3581
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.
3586
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\
3590 active processes."
3591
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
3597 focus .road2.z.t
3598 }
3599
3600 proc roadmap2 {} {
3601 global FG BG
3602
3603 catch {destroy .road2}
3604 toplevel .road2
3605
3606 wm title .road2 "Help with Verification"
3607 wm iconname .road2 "ValHelp"
3608 frame .road2.z
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
3623 settings panel.
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."
3637
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
3643 focus .road2.z.t
3644 }
3645
3646 proc roadmap3 {} {
3647 global FG BG
3648
3649 catch {destroy .road3}
3650 toplevel .road3
3651
3652 wm title .road3 "Reducing Complexity"
3653 wm iconname .road3 "CompHelp"
3654 frame .road3.z
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.
3667
3668 0. Run the Slicing Algorithm (in the Run Menu) to find\
3669 potential redundancy in your model for the stated properties.
3670
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.
3677
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.
3683
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).
3688
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.
3695
3696 5. Combine local computations into atomic, or d_step, sequences.
3697
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\
3705 wherever possible.
3706
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).
3711
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."
3716
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
3722 focus .road3.z.t
3723 }
3724
3725 proc roadmap5 {} {
3726 global FG BG
3727
3728 catch {destroy .road5}
3729 toplevel .road5
3730
3731 wm title .road5 "Spin Automata"
3732 wm iconname .road5 "FsmHelp"
3733 frame .road5.z
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.
3747
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.
3752
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.
3761
3762 In the default layout, the following button actions are
3763 defined (the first one is not needed when using DOT):
3764
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
3769 Xspin window.
3770
3771 If labels look bad -- try changing the font definitions at
3772 the start of the xspin.tcl file (hints are given there).
3773 "
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
3779 focus .road5.z.t
3780 }
3781
3782 proc roadmap6 {} {
3783 global FG BG
3784
3785 catch {destroy .road6}
3786 toplevel .road6
3787
3788 wm title .road6 "Optional Compiler Directives"
3789 wm iconname .road6 "Optional"
3790 frame .road6.z
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:
3801
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)
3804
3805 Related to partial order reduction:
3806
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
3810
3811 Speedups:
3812
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)
3816
3817 Memory saving (slower):
3818
3819 MA=N use a minimized DFA encoding for state vectors up to N bytes
3820
3821 Experimental:
3822
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
3830
3831 Debugging:
3832
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
3835
3836 Already set by the other xspin options:
3837
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
3853 "
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
3859 focus .road6.z.t
3860 }
3861
3862
3863 # simulation options panel
3864
3865 set s_options ""
3866 set v_options ""
3867 set a_options ""
3868 set c_options ""
3869
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"
3875
3876 set fd 0
3877 set Depth 0
3878 set Seq(0) 0
3879 set Sdbox 0
3880 set Spbox(0) 0
3881 set sbox 0
3882
3883 set simruns 0
3884 set stepper 0
3885 set stepped 0
3886 set VERBOSE 0
3887 set SYMBOLIC 0
3888 set howmany 0
3889 set Choice(1) 0
3890 set Sticky(0) 0
3891 set SparseMsc 1
3892 set showvars 1
3893 set vv 1
3894 set qv 1
3895 set gvars 1
3896 set lvars 0
3897 set hide_q1 ""
3898 set hide_q2 ""
3899 set hide_q3 ""
3900 set PlaceSim "+200+100"
3901
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
3907
3908 catch { .menu.run.m entryconfigure 5 -state normal }
3909
3910 catch {destroy .s}
3911 toplevel .s
3912 set k [string first "\+" $PlaceSim]
3913 if {$k > 0} {
3914 set PlaceSim [string range $PlaceSim $k end]
3915 }
3916
3917 wm title .s "Simulation Options"
3918 wm iconname .s "SIM"
3919 wm geometry .s $PlaceSim
3920
3921 frame .s.opt -relief flat
3922
3923 mkpan_in
3924
3925 frame .s.opt.mode -relief raised -borderwidth 1m
3926 label .s.opt.mode.fld0 \
3927 -font $HelvBig \
3928 -text "Display Mode" \
3929 -relief sunken -borderwidth 1m
3930
3931 checkbutton .s.opt.mode.fld4b -text "Time Sequence Panel - with:" \
3932 -variable tsc \
3933 -relief flat
3934 frame .s.opt.mode.flds
3935 radiobutton .s.opt.mode.flds.fld3 \
3936 -text " Interleaved Steps" \
3937 -variable m_typ -value 2 \
3938 -relief flat
3939 radiobutton .s.opt.mode.flds.fld1 \
3940 -text " One Window per Process" \
3941 -variable m_typ -value 0 \
3942 -relief flat
3943 radiobutton .s.opt.mode.flds.fld2 \
3944 -text " One Trace per Process" \
3945 -variable m_typ -value 1 \
3946 -relief flat
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}
3953
3954 checkbutton .s.opt.mode.fld4a -text "MSC Panel - with:" \
3955 -variable msc \
3956 -relief flat
3957 frame .s.opt.mode.steps
3958 radiobutton .s.opt.mode.steps.fld5 -text " Step Number Labels" \
3959 -variable SYMBOLIC -value 0 \
3960 -relief flat
3961 radiobutton .s.opt.mode.steps.fld6 -text " Source Text Labels" \
3962 -variable SYMBOLIC -value 1 \
3963 -relief flat
3964 radiobutton .s.opt.mode.steps.fld7 -text " Normal Spacing" \
3965 -variable SparseMsc -value 1 \
3966 -relief flat
3967 radiobutton .s.opt.mode.steps.fld8 -text " Condensed Spacing" \
3968 -variable SparseMsc -value 0 \
3969 -relief flat
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}
3977
3978 checkbutton .s.opt.mode.fld4c -text "Execution Bar Panel" \
3979 -variable ebc \
3980 -relief flat
3981 checkbutton .s.opt.mode.fld4d -text "Data Values Panel" \
3982 -variable vv \
3983 -relief flat
3984
3985 frame .s.opt.mode.vars
3986
3987 checkbutton .s.opt.mode.vars.fld4c -text " Track Buffered Channels" \
3988 -variable qv \
3989 -relief flat
3990 checkbutton .s.opt.mode.vars.fld4d -text " Track Global Variables" \
3991 -variable gvars \
3992 -relief flat
3993 checkbutton .s.opt.mode.vars.fld4e -text " Track Local Variables" \
3994 -variable lvars \
3995 -relief flat
3996
3997 checkbutton .s.opt.mode.vars.fld4f \
3998 -text " Display vars marked 'show' in MSC" \
3999 -variable showvars \
4000 -relief flat
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}
4008
4009 pack append .s.opt.mode .s.opt.mode.fld0 {top pady 4 frame w fillx}
4010
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}
4013
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}
4016
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}
4019
4020 pack append .s.opt.mode .s.opt.mode.fld4c {top pady 4 frame w}
4021
4022 pack append .s.opt .s.opt.mode {left frame n}
4023
4024 frame .s.opt.mesg -relief raised -borderwidth 1m
4025 label .s.opt.mesg.loss0 \
4026 -font $HelvBig \
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 \
4031 -relief flat
4032 radiobutton .s.opt.mesg.loss2 -text "Loses New Msgs" \
4033 -variable l_typ -value 1 \
4034 -relief flat
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}
4038
4039 frame .s.opt.hide -relief raised -borderwidth 1m
4040 label .s.opt.hide.txt \
4041 -font $HelvBig \
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 }
4045
4046 for {set i 1} {$i < 4} {incr i} {
4047 frame .s.opt.hide.q$i
4048 label .s.opt.hide.q$i.qno \
4049 -font $HelvBig \
4050 -text "Queue nr:"
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}
4056 }
4057 frame .s.opt.lframe -relief raised -borderwidth 1m
4058 label .s.opt.lframe.tl \
4059 -font $HelvBig \
4060 -text "Simulation Style" \
4061 -relief sunken -borderwidth 1m
4062 radiobutton .s.opt.lframe.is -text "Interactive" \
4063 -variable s_typ -value 2 \
4064 -relief flat
4065 radiobutton .s.opt.lframe.gs -text "Guided (using pan.trail)" \
4066 -variable s_typ -value 1 \
4067 -relief flat
4068 frame .s.opt.lframe.b
4069 entry .s.opt.lframe.b.entry -relief sunken -width 8
4070 label .s.opt.lframe.b.label \
4071 -font $HelvBig \
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}
4076
4077 radiobutton .s.opt.lframe.rs -text "Random (using seed)" \
4078 -variable s_typ -value 0 \
4079 -relief flat
4080 frame .s.opt.lframe.s
4081 entry .s.opt.lframe.s.entry -relief sunken -width 8
4082 label .s.opt.lframe.s.label \
4083 -font $HelvBig \
4084 -text "Seed Value"
4085 pack append .s.opt.lframe.s \
4086 .s.opt.lframe.s.label {left} \
4087 .s.opt.lframe.s.entry {left}
4088
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}
4095
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}
4099
4100 pack append .s .s.opt { top frame n }
4101
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}
4108
4109 .s.opt.lframe.s.entry insert end $seed
4110 .s.opt.lframe.b.entry insert end $jumpsteps
4111
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
4115
4116 raise .s
4117 }
4118
4119
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
4125 global whichsim
4126
4127 catch { .menu.run.m entryconfigure 5 -state normal }
4128
4129 catch {destroy .s}
4130 toplevel .s
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]
4135 if {$k > 0} {
4136 set PlaceSim [string range $PlaceSim $k end]
4137 }
4138
4139 wm title .s "Simulation Options"
4140 wm iconname .s "SIM"
4141 wm geometry .s $PlaceSim
4142
4143 mkpan_in
4144
4145 # lower frame with 'start', 'cancel' and 'help' buttons
4146 frame .s.l -relief flat
4147 pack .s.l -side bottom -fill both
4148
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" \
4152 -command "
4153 Stopsim;
4154 catch {rmfile pan_in9999999.trail}
4155 "
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
4159
4160 # upper frame with modes and options
4161 frame .s.u -relief flat
4162 pack .s.u -side top -fill both
4163
4164 frame .s.u.mode -relief raised -borderwidth 1m
4165 pack .s.u.mode -side left -fill both -expand 1
4166
4167 frame .s.u.mode.fdis -relief flat
4168 pack .s.u.mode.fdis -side top -fill x -expand 1
4169
4170 label .s.u.mode.fdis.fld0 \
4171 -font $HelvBig \
4172 -text "Display Mode" \
4173 -relief sunken -borderwidth 1m
4174 pack .s.u.mode.fdis.fld0 -side top -fill x
4175
4176 #MSC Panel
4177
4178 frame .s.u.mode.fmsc -relief flat
4179 pack .s.u.mode.fmsc -side top -fill x
4180
4181 checkbutton .s.u.mode.fmsc.fld4a -text "MSC Panel - with:" \
4182 -variable msc \
4183 -relief flat
4184 pack .s.u.mode.fmsc.fld4a -side left
4185
4186 frame .s.u.mode.msc -relief flat
4187 pack .s.u.mode.msc -side top -fill x
4188
4189 frame .s.u.mode.msc.lab -relief flat
4190 pack .s.u.mode.msc.lab -side top -fill x
4191
4192 frame .s.u.mode.msc.lab.dummy -width 18 -relief flat
4193 pack .s.u.mode.msc.lab.dummy -side left -fill y
4194
4195 frame .s.u.mode.msc.lab.radios -relief flat
4196 pack .s.u.mode.msc.lab.radios -side left -fill x
4197
4198 frame .s.u.mode.msc.lab.radios.fnum -relief flat
4199 pack .s.u.mode.msc.lab.radios.fnum -side top -fill x
4200
4201 radiobutton .s.u.mode.msc.lab.radios.fnum.fld5 \
4202 -text " Step Number Labels" \
4203 -variable SYMBOLIC -value 0 \
4204 -relief flat
4205 pack .s.u.mode.msc.lab.radios.fnum.fld5 -side left
4206
4207 frame .s.u.mode.msc.lab.radios.ftext -relief flat
4208 pack .s.u.mode.msc.lab.radios.ftext -side top -fill x
4209
4210 radiobutton .s.u.mode.msc.lab.radios.ftext.fld6 \
4211 -text " Source Text Labels" \
4212 -variable SYMBOLIC -value 1 \
4213 -relief flat
4214 pack .s.u.mode.msc.lab.radios.ftext.fld6 -side left
4215
4216 frame .s.u.mode.msc.lab.bracket
4217 pack .s.u.mode.msc.lab.bracket -side left -fill y
4218
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
4222
4223 frame .s.u.mode.msc.space -relief flat
4224 pack .s.u.mode.msc.space -side top -fill x
4225
4226 frame .s.u.mode.msc.space.dummy -width 18 -relief flat
4227 pack .s.u.mode.msc.space.dummy -side left -fill y
4228
4229 frame .s.u.mode.msc.space.radios -relief flat
4230 pack .s.u.mode.msc.space.radios -side left -fill x
4231
4232 frame .s.u.mode.msc.space.radios.fnorm -relief flat
4233 pack .s.u.mode.msc.space.radios.fnorm -side top -fill x
4234
4235 radiobutton .s.u.mode.msc.space.radios.fnorm.fld7 \
4236 -text " Normal Spacing" \
4237 -variable SparseMsc -value 1 \
4238 -relief flat
4239 pack .s.u.mode.msc.space.radios.fnorm.fld7 -side left
4240
4241 frame .s.u.mode.msc.space.radios.fcond -relief flat
4242 pack .s.u.mode.msc.space.radios.fcond -side top -fill x
4243
4244 radiobutton .s.u.mode.msc.space.radios.fcond.fld8 \
4245 -text " Condensed Spacing" \
4246 -variable SparseMsc -value 0 \
4247 -relief flat
4248 pack .s.u.mode.msc.space.radios.fcond.fld8 -side left
4249
4250 frame .s.u.mode.msc.space.bracket
4251 pack .s.u.mode.msc.space.bracket -side left -fill y
4252
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
4256
4257 # Time Sequence Panel
4258
4259 frame .s.u.mode.ftsp -relief flat
4260 pack .s.u.mode.ftsp -side top -fill x
4261
4262 checkbutton .s.u.mode.ftsp.fld4b \
4263 -text "Time Sequence Panel - with:" \
4264 -variable tsc \
4265 -relief flat
4266 pack .s.u.mode.ftsp.fld4b -side left
4267
4268 frame .s.u.mode.tsp
4269 pack .s.u.mode.tsp -side top -fill x
4270
4271 frame .s.u.mode.tsp.proc
4272 pack .s.u.mode.tsp.proc -side top -fill x
4273
4274 frame .s.u.mode.tsp.proc.dummy -width 18
4275 pack .s.u.mode.tsp.proc.dummy -side left -fill y
4276
4277 frame .s.u.mode.tsp.proc.radios -relief flat
4278 pack .s.u.mode.tsp.proc.radios -side left -fill y
4279
4280 frame .s.u.mode.tsp.proc.radios.is
4281 pack .s.u.mode.tsp.proc.radios.is -side top -fill x
4282
4283 radiobutton .s.u.mode.tsp.proc.radios.is.fld3 \
4284 -text " Interleaved Steps" \
4285 -variable m_typ -value 2 \
4286 -relief flat
4287 pack .s.u.mode.tsp.proc.radios.is.fld3 -side left
4288
4289 frame .s.u.mode.tsp.proc.radios.1win -relief flat
4290 pack .s.u.mode.tsp.proc.radios.1win -side top -fill x
4291
4292 radiobutton .s.u.mode.tsp.proc.radios.1win.fld1 \
4293 -text " One Window per Process" \
4294 -variable m_typ -value 0 \
4295 -relief flat
4296 pack .s.u.mode.tsp.proc.radios.1win.fld1 -side left
4297
4298 frame .s.u.mode.tsp.proc.radios.1trace -relief flat
4299 pack .s.u.mode.tsp.proc.radios.1trace -side top -fill x
4300
4301 radiobutton .s.u.mode.tsp.proc.radios.1trace.fld2 \
4302 -text " One Trace per Process" \
4303 -variable m_typ -value 1 \
4304 -relief flat
4305 pack .s.u.mode.tsp.proc.radios.1trace.fld2 -side left
4306
4307 frame .s.u.mode.tsp.proc.bracket
4308 pack .s.u.mode.tsp.proc.bracket -side left -fill y
4309
4310 set y 13
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] \
4314 10 [expr 0 + $y] \
4315 10 [expr 25 + $y] \
4316 5 [expr 25 + $y] \
4317 10 [expr 25 + $y] \
4318 10 [expr 50 + $y] \
4319 5 [expr 50 + $y]
4320
4321 frame .s.u.mode.fdvp -relief flat
4322 pack .s.u.mode.fdvp -side top -fill x
4323
4324 checkbutton .s.u.mode.fdvp.fld4d -text "Data Values Panel" \
4325 -variable vv \
4326 -relief flat
4327 pack .s.u.mode.fdvp.fld4d -side left
4328
4329 frame .s.u.mode.vars
4330 pack .s.u.mode.vars -side top -fill x
4331
4332 frame .s.u.mode.vars.dummy -width 18
4333 pack .s.u.mode.vars.dummy -side left -fill y
4334
4335 frame .s.u.mode.vars.chks -relief flat
4336 pack .s.u.mode.vars.chks -side left -fill y
4337
4338 frame .s.u.mode.vars.chks.ftbc
4339 pack .s.u.mode.vars.chks.ftbc -side top -fill x
4340
4341 checkbutton .s.u.mode.vars.chks.ftbc.fld4c -text " Track Buffered Channels" \
4342 -variable qv \
4343 -relief flat
4344 pack .s.u.mode.vars.chks.ftbc.fld4c -side left
4345
4346 frame .s.u.mode.vars.chks.ftgv
4347 pack .s.u.mode.vars.chks.ftgv -side top -fill x
4348
4349 checkbutton .s.u.mode.vars.chks.ftgv.fld4d -text " Track Global Variables" \
4350 -variable gvars \
4351 -relief flat
4352 pack .s.u.mode.vars.chks.ftgv.fld4d -side left
4353
4354 frame .s.u.mode.vars.chks.ftlv
4355 pack .s.u.mode.vars.chks.ftlv -side top -fill x
4356
4357 checkbutton .s.u.mode.vars.chks.ftlv.fld4e -text " Track Local Variables" \
4358 -variable lvars \
4359 -relief flat
4360 pack .s.u.mode.vars.chks.ftlv.fld4e -side left
4361
4362 frame .s.u.mode.vars.chks.fshow
4363 pack .s.u.mode.vars.chks.fshow -side top -fill x
4364
4365 checkbutton .s.u.mode.vars.chks.fshow.fld4f \
4366 -text " Display vars marked 'show' in MSC" \
4367 -variable showvars \
4368 -relief flat
4369
4370 pack .s.u.mode.vars.chks.fshow.fld4f -side left
4371
4372 frame .s.u.mode.fexecbar -relief flat
4373 pack .s.u.mode.fexecbar -side top -fill x
4374
4375 checkbutton .s.u.mode.fexecbar.fld4c -text "Execution Bar Panel" \
4376 -variable ebc \
4377 -relief flat
4378 pack .s.u.mode.fexecbar.fld4c -side left
4379
4380 #Right upper frame
4381 frame .s.u.r -relief flat
4382 pack .s.u.r -side right -fill y -expand 1
4383
4384 #Simulation Style
4385 frame .s.u.r.sim -relief raised -borderwidth 1m
4386 pack .s.u.r.sim -side top -fill both -expand 1
4387
4388 frame .s.u.r.sim.flab -relief sunken
4389 pack .s.u.r.sim.flab -side top -fill x
4390
4391 label .s.u.r.sim.flab.tl \
4392 -font $HelvBig \
4393 -text "Simulation Style" \
4394 -relief sunken -borderwidth 1m
4395 pack .s.u.r.sim.flab.tl -side top -fill x
4396
4397 frame .s.u.r.sim.random
4398 pack .s.u.r.sim.random -side top -fill x
4399
4400 radiobutton .s.u.r.sim.random.rs -text "Random (using seed)" \
4401 -variable s_typ -value 0 \
4402 -relief flat \
4403 -command "enable_disable_sub_buttons"
4404 pack .s.u.r.sim.random.rs -side left
4405
4406 frame .s.u.r.sim.seedvalue
4407 pack .s.u.r.sim.seedvalue -side top -fill x
4408
4409 frame .s.u.r.sim.seedvalue.dummy -width 18
4410 pack .s.u.r.sim.seedvalue.dummy -side left -fill y
4411
4412 label .s.u.r.sim.seedvalue.label \
4413 -font $HelvBig \
4414 -text "Seed Value"
4415 pack .s.u.r.sim.seedvalue.label -side left
4416
4417 entry .s.u.r.sim.seedvalue.entry -relief sunken -width 8
4418 pack .s.u.r.sim.seedvalue.entry -side left
4419
4420 frame .s.u.r.sim.guided
4421 pack .s.u.r.sim.guided -side top -fill x
4422
4423 radiobutton .s.u.r.sim.guided.gs -text "Guided" \
4424 -variable s_typ -value 1 \
4425 -relief flat \
4426 -command "enable_disable_sub_buttons"
4427 pack .s.u.r.sim.guided.gs -side left
4428
4429 frame .s.u.r.sim.guided_type
4430 pack .s.u.r.sim.guided_type -side top -fill x
4431
4432 frame .s.u.r.sim.guided_type.dummy -width 18
4433 pack .s.u.r.sim.guided_type.dummy -side left -fill y
4434
4435 frame .s.u.r.sim.guided_type.radios
4436 pack .s.u.r.sim.guided_type.radios -side left
4437
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
4440
4441 radiobutton .s.u.r.sim.guided_type.radios.pan_trail.rb \
4442 -text "Using pan_in.trail" \
4443 -variable whichsim -value 0 \
4444 -relief flat
4445 pack .s.u.r.sim.guided_type.radios.pan_trail.rb -side left
4446
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
4449
4450 radiobutton .s.u.r.sim.guided_type.radios.trail_other.rb \
4451 -text "Use" \
4452 -variable whichsim -value 1 \
4453 -relief flat
4454 pack .s.u.r.sim.guided_type.radios.trail_other.rb -side left
4455
4456 entry .s.u.r.sim.guided_type.radios.trail_other.entry \
4457 -width 20
4458 pack .s.u.r.sim.guided_type.radios.trail_other.entry -side left
4459
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
4463
4464 frame .s.u.r.sim.skipstep
4465 pack .s.u.r.sim.skipstep -side top -fill x
4466
4467 label .s.u.r.sim.skipstep.label \
4468 -font $HelvBig \
4469 -text "Steps Skipped"
4470 pack .s.u.r.sim.skipstep.label -side left
4471
4472 entry .s.u.r.sim.skipstep.entry -relief sunken -width 8
4473 pack .s.u.r.sim.skipstep.entry -side left
4474
4475 frame .s.u.r.sim.interactive
4476 pack .s.u.r.sim.interactive -side top -fill x
4477
4478 radiobutton .s.u.r.sim.interactive.is -text "Interactive" \
4479 -variable s_typ -value 2 \
4480 -relief flat \
4481 -command "enable_disable_sub_buttons"
4482 pack .s.u.r.sim.interactive.is -side left
4483
4484 #A Full Queue
4485 frame .s.u.r.fq -relief raised -borderwidth 1m
4486 pack .s.u.r.fq -side top -fill both -expand 1
4487
4488 frame .s.u.r.fq.label -relief sunken
4489 pack .s.u.r.fq.label -side top -fill x
4490
4491 label .s.u.r.fq.label.loss0 \
4492 -font $HelvBig \
4493 -text "A Full Queue" \
4494 -relief sunken -borderwidth 1m
4495 pack .s.u.r.fq.label.loss0 -side top -fill x
4496
4497 frame .s.u.r.fq.block
4498 pack .s.u.r.fq.block -side top -fill x
4499
4500 radiobutton .s.u.r.fq.block.loss1 -text "Blocks New Msgs" \
4501 -variable l_typ -value 0 \
4502 -relief flat
4503 pack .s.u.r.fq.block.loss1 -side left
4504
4505 frame .s.u.r.fq.lose
4506 pack .s.u.r.fq.lose -side top -fill x
4507
4508 radiobutton .s.u.r.fq.lose.loss2 -text "Loses New Msgs" \
4509 -variable l_typ -value 1 \
4510 -relief flat
4511 pack .s.u.r.fq.lose.loss2 -side left
4512
4513 #Hide Queues in MSC
4514 frame .s.u.r.hq -relief raised -borderwidth 1m
4515 pack .s.u.r.hq -side top -fill both -expand 1
4516
4517 frame .s.u.r.hq.flabel -relief sunken
4518 pack .s.u.r.hq.flabel -side top -fill x
4519
4520 label .s.u.r.hq.flabel.txt \
4521 -font $HelvBig \
4522 -text "Hide Queues in MSC" \
4523 -relief sunken -borderwidth 1m
4524 pack .s.u.r.hq.flabel.txt -side top -fill x
4525
4526 for {set i 1} {$i < 4} {incr i} {
4527 frame .s.u.r.hq.q$i
4528 pack .s.u.r.hq.q$i -side top -fill x
4529 label .s.u.r.hq.q$i.qno \
4530 -font $HelvBig \
4531 -text "Queue nr:"
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
4536 }
4537
4538 .s.u.r.sim.seedvalue.entry insert end $seed
4539 .s.u.r.sim.skipstep.entry insert end $jumpsteps
4540
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
4545
4546 tkwait visibility .s
4547 raise .s
4548 }
4549
4550 proc enable_disable_sub_buttons {} {
4551 global s_typ
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
4556 }
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
4561 }
4562
4563 }
4564 }
4565
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"
4573 } default {
4574 set fileselect "tk_getOpenFile"
4575 }
4576 set init_dir [pwd]
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
4580 raise .s
4581
4582 }
4583
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
4589
4590 set s_options "-X -p -v $ival(5)"
4591
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"
4596 } }
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 {
4608 set trail_num ""
4609 #Guided
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."
4615 }
4616 return 0
4617 }
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]
4621 if {$ind > -1} {
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"
4625 } else {
4626 #strip off path
4627 set trail_file [string range $trail_file \
4628 [expr $ind + 1] \
4629 [expr [string length $trail_file] - 1]]
4630 }
4631 }
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]
4636
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] {
4641 set trail_num $num
4642 set is_pan_in_trail_file 1
4643 } } }
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
4650 } else {
4651 catch {tk_messageBox -icon info \
4652 -message "Unable to create input file in $pwd \
4653 check write permissions."
4654 }
4655 return 0
4656 }
4657 }
4658 } else {
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."
4662 }
4663 return 0
4664 }
4665 }
4666
4667 set s_options [format "%s -t%s" $s_options $trail_num]
4668 } else {
4669 if {[string length $seed] > 0} {
4670 set s_options [format "%s -n%s" $s_options $seed]
4671 } }
4672 if {$s_typ!=2} then {
4673 if {[string length $jumpsteps] > 0} {
4674 set s_options [format "%s -j%s" $s_options $jumpsteps]
4675 } }
4676 return 1
4677 }
4678
4679 proc Stopsim {} {
4680 global stop dbox2 Sticky PlaceSim PlaceCanvas
4681 global stepper stepped howmany fd
4682
4683 set stop 1
4684 set stepped 0
4685 set stepper 0
4686 add_log "<stop simulation>"
4687 if {[winfo exists .s]} {
4688 set PlaceSim [wm geometry .s]
4689 destroy .s
4690 }
4691 catch {set howmany 0}
4692 catch {stopbar}
4693 catch { if {$Sticky($dbox2) == 0} {
4694 set PlaceCanvas(msc) [wm geometry .f$dbox2]
4695 destroy .f$dbox2
4696 } }
4697 catch {
4698 puts $fd "q"
4699 flush $fd
4700 }
4701 update
4702 }
4703
4704 proc Step_forw {} {
4705 global stepper stepped sbox simruns PlaceSim
4706
4707 set stepped 1
4708 set stepper 1
4709 if {$simruns == 0} {
4710 if {[winfo exists .s]} {
4711 set PlaceSim [wm geometry .s]
4712 destroy .s
4713 }
4714 runsim
4715 } else {
4716 catch { .c$sbox.run configure \
4717 -text "Run" -command "Runsim" }
4718 }
4719 }
4720
4721 proc Rewind {} {
4722 global Depth s_typ whichsim trail_file
4723 global Sdbox Spbox
4724 global seed jumpsteps simruns
4725 global hide_q1 hide_q2 hide_q3 trail_file
4726
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] }
4731
4732 if {$s_typ == 0} {
4733 catch { set seed [.s.u.r.sim.seedvalue.entry get] }
4734 }
4735 if {$s_typ == 1} {
4736 #Guided
4737 set Depth 0
4738 catch {
4739 foreach el [array names Spbox] {
4740 set Sdbox $Spbox($el)
4741 .c$Sdbox.z.t tag remove Rev 1.0 end
4742 } }
4743 if {$whichsim == 1} {
4744 set trail_file ""
4745 catch {set trail_file [.s.u.r.sim.guided_type.radios.trail_other.entry get]}
4746 }
4747 }
4748
4749 set simruns 0
4750
4751 Step_forw
4752 }
4753
4754 proc Runsim {} {
4755 global stepper stepped sbox
4756
4757 catch { .c$sbox.run configure \
4758 -text "Suspend" -command "Step_forw" }
4759 set stepper 1
4760 set stepped 0
4761 }
4762
4763 proc BreakPoint {} {
4764 global stepped sbox
4765
4766 set stepped 1
4767 catch { .c$sbox.run configure \
4768 -text "BreakPoint" -command "Runsim" }
4769 }
4770
4771 proc runsim {} {
4772 global Unix SPIN tk_major
4773 global s_options s_typ dbox2
4774 global stepper stepped
4775 global simruns m_typ
4776 global gvars lvars
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
4783 global dbox Vvbox
4784 global whichsim trail_num
4785
4786 set simruns 1
4787 set Vvbox 0
4788 set pno 0
4789 set Varnm("") ""
4790 set Queues("") ""
4791 set Depth 0
4792 set Seq(0) 0
4793 set Pstp 1
4794 set Seenpno 1
4795 set Banner "Select"
4796
4797 # catch { unset Spbox(0) }
4798 catch {
4799 foreach el [array names pbox] {
4800 catch { destroy .c$pbox($el) }
4801 catch { unset pbox($el) }
4802 }
4803 foreach el [array names Spbox] {
4804 catch { destroy .c$Spbox($el) }
4805 catch { unset Spbox($el) }
4806 }
4807 }
4808 if ![bld_s_options] {
4809 return
4810 }
4811
4812 add_log "<starting simulation>"
4813 add_log "$SPIN $s_options pan_in"
4814 update
4815 set s_options [format "%s pan_in" $s_options]
4816
4817 mkpan_in
4818
4819 set sbox [mkbox "Simulation Output" "SimOut" "sim.out" 71 11 100 100]
4820
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}
4825
4826 .c$sbox.b configure -text "Cancel" -command "Stopsim"
4827
4828 raise .c$sbox
4829
4830 set YSZ 12
4831 set XSZ 84
4832 set YNR 60
4833 set NPR 10
4834 set SMX 250
4835 set Easy 1
4836 set HAS 0
4837 set HAS_CYCLE 0
4838 set dontwait 0
4839 set notexecutable 0
4840 set lastexecutable 0
4841
4842 if {$m_typ == 2} {
4843 if {$tsc} {
4844 set pbox(0) \
4845 [mkbox "Time Sequence" "Sequence" "seq.out" 80 10 100 325]
4846 set dbox $pbox(0)
4847 } }
4848 if {$msc} {
4849 if {[hasWord "!!"] || [hasWord "\\?\\?"]} {
4850 set Easy 0
4851 }
4852
4853 set maxx [expr [winfo screenwidth .] - 400] ;# button widths
4854 set maxh [expr [winfo screenheight .] - (5+120)] ;# borders+buttons
4855 set dbox2 \
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]"
4860
4861 raise .f$dbox2
4862 }
4863
4864 raise .c$sbox
4865
4866 set stop 0
4867 set good_trail 0
4868 if {$s_typ == 1} {
4869 if $whichsim {
4870 set filen "pan_in${trail_num}.trail"
4871 if [file exists $filen] {
4872 set good_trail 1
4873 }
4874 } else {
4875 if {[file exists pan_in.trail] || [file exists pan_in.tra]} {
4876 set good_trail 1
4877 }
4878 }
4879 if $good_trail {
4880 catch { .c$sbox.z.t insert end "preparing trail, please wait..." }
4881 update
4882 rmfile trail.out
4883 catch {eval exec $SPIN $s_options >&trail.out} errmsg
4884 } else {
4885 set errmsg "error: no trail file for guided simulation"
4886 return
4887 }
4888 if {[string length $errmsg]>0} {
4889 add_log "$errmsg"
4890 catch {
4891 tk_messageBox -icon info -message $errmsg
4892 }
4893 catch {
4894 set fd [open trail.out r]
4895 while {[gets $fd line] > -1} {
4896 add_log "$line"
4897 }
4898 close $fd
4899 }
4900 Stopsim
4901 catch { destroy .c$sbox }
4902 catch { destroy .c$dbox }
4903 set simruns 0
4904 update
4905 return
4906 }
4907 set fd [open trail.out r]
4908 catch { .c$sbox.z.t insert end "done\n" }
4909 } else {
4910 update
4911 set fd [open "|$SPIN $s_options" r+]
4912 catch "flush $fd"
4913 update
4914 }
4915
4916 if {$s_typ == 2} {
4917 Runsim
4918 }
4919
4920 if {$ebc} { startbar "Xspin Bar Chart" }
4921
4922 set pstp -1
4923 set bailout 0
4924 set realstring ""
4925
4926 update
4927 raise .c$sbox
4928 lower .
4929
4930 while {$stop == 0 && [eof $fd] == 0} {
4931 if {$bailout == 0 && [gets $fd line] > -1} {
4932 set pln 0
4933 set syntax 0
4934 set isvar 0
4935 set pname ""
4936 set i 0
4937 set VERBOSE 0
4938 set Fnm "pan_in"
4939
4940 raise .c$sbox
4941
4942 if {$Unix == 0} {
4943 if {[string first "processes created" $line] > 0} {
4944 set bailout 1
4945 } }
4946 if {[string first "type return to proceed" $line] > 0} {
4947 puts $fd ""
4948 flush $fd
4949 update
4950 continue
4951 }
4952
4953 set i [string first "<merge" $line]
4954 if {$i > 0} {
4955 set line [string range $line 0 $i]
4956 }
4957
4958 set lastpstp $pstp
4959 set pmtch [scan $line \
4960 "%d: proc %d (%s line %d \"%s\" " \
4961 pstp pno pname pln Fnm]
4962 incr pmtch -1
4963 set i [string first "\[" $line]
4964 if {$i > 0} {
4965 set i [expr $i + 1]
4966 set j [string length $line]
4967 set j [expr $j - 2]
4968 set stmnt [string range $line $i $j]
4969 } else {
4970 set stmnt "-"
4971 }
4972 if {$pmtch != 4} {
4973 set pmtch [scan $line \
4974 " proc %d (%s line %d \"%s\" " \
4975 pno pname pln Fnm]
4976 }
4977 if {$pmtch != 4} {
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
4985 }
4986 if {[string first "assertion viol" $line] < 0} {
4987 set syntax 1
4988 }
4989 }
4990 if {[string first "Error: " $line] >= 0 \
4991 || [string first "warning: " $line] >= 0 } {
4992 set syntax 1
4993 }
4994 }
4995 if {$pmtch != 4 && $syntax == 0} {
4996 set pmtch [scan $line \
4997 "%d: proc - (%s line %d \"%s\" " \
4998 pstp pname pln Fnm]
4999 if { $pmtch == 4 } {
5000 set pno -1
5001 }
5002 }
5003 # set Fnm [string trim $Fnm "\""]
5004 set pname [string trim $pname "()"]
5005
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])} {
5011 unset Plabel($pno)
5012 ##
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 \
5018 -width 2 \
5019 -fill $Red
5020 incr TMP2 4
5021 .f$dbox2.c create line \
5022 [expr $TMP1 - 20] $TMP2 \
5023 [expr $TMP1 + 20] $TMP2 \
5024 -width 2 \
5025 -fill $Red
5026 ##
5027 }
5028 set nwcol([expr $pno+1]) 0
5029 }
5030 if {$pmtch == 4 && $syntax == 0} {
5031 if {$ebc} {
5032 if {[string first "values:" $line] < 0} {
5033 stepbar $pno $pname
5034 } }
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" \
5040 60 10 \
5041 [expr 100+$pno*25] \
5042 [expr 325+$pno*35] ]
5043 }
5044 set dbox $pbox($pno)
5045 } elseif {$m_typ == 0 && $tsc} {
5046 if { [info exists Spbox($pno)] == 0 } {
5047 set Spbox($pno) \
5048 [mkbox "$pname (proc $pno)" \
5049 "$pname" "" \
5050 60 10 \
5051 [expr 100+$pno*25] \
5052 [expr 325+$pno*35] ]
5053 readinfile .c$Spbox($pno).z.t "pan_in"
5054 }
5055 set Sdbox $Spbox($pno)
5056 }
5057 } elseif { [string first "..." $line] > 0 && \
5058 [regexp "^\\\t*MSC: (.*)" $line] == 0 } {
5059 set $line ""
5060 set syntax 1
5061 set pln 0
5062 } elseif {$s_typ == 2 \
5063 && [string first "Select " $line] == 0 } {
5064 set Banner $line
5065 set pln 0
5066 set notexecutable 0
5067 set lastexecutable 0
5068 set has_timeout 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} {
5075 set has_timeout 1
5076 }
5077 if {[string first "unexecutable," $line] >= 0} {
5078 incr notexecutable
5079 } else {
5080 set lastexecutable $howmany
5081 }
5082 set pln 0
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)"
5089 catch {
5090 foreach el [array names Choice] {
5091 unset Choice($el)
5092 } }
5093 } else {
5094 pickoption $Banner
5095 add_log "selected: $howmany"
5096 }
5097 puts $fd $howmany
5098 catch "flush $fd"
5099 set dontwait 1
5100 set pln 0
5101 } elseif { [regexp "^\\\t*MSC: (.*)" $line mch rstr] != 0 } {
5102 if {$realstring != ""} {
5103 set realstring "$realstring $rstr"
5104 } else {
5105 set realstring $rstr
5106 }
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 } {
5112
5113 if { $m_typ == 1 && $tsc} {
5114 set dbox $pbox(0)
5115 } elseif { $m_typ == 0 && $tsc} {
5116 if { [info exists Spbox($pno)] == 0 } {
5117 set Spbox($pno) \
5118 [mkbox "$pname (proc $pno)" \
5119 "$pname" "" \
5120 60 10 \
5121 [expr 100+$pno*25] \
5122 [expr 325+$pno*35] ]
5123 readinfile .c$Spbox($pno).z.t "pan_in"
5124 }
5125 set Sdbox $Spbox($pno)
5126 }
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
5136 set isvar 1
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"
5149 }
5150 } else {
5151 set Alias($qnr) $ZZ
5152 }
5153 set isvar 1
5154 }
5155 } elseif {[string length $line] == 0} {
5156 if {$dontwait == 0} { set stepper 0 }
5157 set pln 0
5158 set Depth [expr $Depth + 1]
5159 set Seq($Depth) [tell $fd]
5160 set dontwait 0
5161 }
5162
5163
5164 if {$syntax == 0} {
5165 if {[string first "terminates" $line] > 0} {
5166 set pln -1
5167 set stmnt "<stop>"
5168 }
5169 ##NEW
5170 if {$pln > 0 && [string first "pan_in" $Fnm] >= 0} {
5171 .inp.t tag remove hilite 0.0 end
5172 src_line $pln
5173 }
5174 ##END
5175 if {$m_typ == 0} {
5176 if {$pln > 0 && [string first "pan_in" $Fnm] >= 0} {
5177 catch {
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
5183 } }
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" \
5189 60 10 \
5190 [expr 100+$pno*25] \
5191 [expr 325+$pno*35] ]
5192 }
5193 set dbox $pbox($pno)
5194 catch {
5195 .c$dbox.z.t yview -pickplace end
5196 .c$dbox.z.t insert end "$line\n"
5197 }
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|" }
5204 }
5205 catch { .c$dbox.z.t insert end "\t|>$stmnt\n" }
5206 }
5207 if {$msc && $pln != 0} {
5208 set Mcont "--"
5209 set HAS 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]
5213 incr HAS
5214 set Mcont [string range $stmnt $HAS end]
5215 set HAS 1
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]
5219 incr HAS
5220 set Mcont [string range $stmnt $HAS end]
5221 set HAS 2
5222 } elseif { [string first "-" $stmnt] == 0} {
5223 set HAS 3
5224 if {$HAS_CYCLE} {
5225 set stmnt [format "Cycle>>"]
5226 } else {
5227 set stmnt [format "<waiting>"]
5228 }
5229 } elseif { [string first "<stop>" $stmnt] == 0} {
5230 set HAS 3
5231 set stmnt [format "<stopped>"]
5232 }
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} {
5237 set VERBOSE 1
5238 set stmnt $realstring
5239 if {[string first "BREAK" $realstring] >= 0} {
5240 BreakPoint
5241 }
5242 set realstring ""
5243 } else {
5244 set VERBOSE 0
5245 }
5246 catch {
5247 if {$VERBOSE \
5248 || $HAS != 0 \
5249 || [info exists R($pstp,$pno)]} {
5250
5251 if { $SparseMsc == 1 \
5252 || [info exists Plabel($pno)] == 0 \
5253 || ([info exists R($pstp,$pno)] == 0 \
5254 && ($HAS != 1 \
5255 || [info exists HasBox($YLOC,[expr 1+$pno])])) } {
5256 incr Pstp
5257 for {set i 1} \
5258 {$Pstp > 1 && $i <= $Seenpno} \
5259 {incr i} {
5260 if {[info exists HasBox($YLOC,$i)]} {
5261 continue
5262 }
5263 set TMP1 [expr $i*$XSZ]
5264 set lncol $Blue
5265 set lnwdt 1
5266 catch {
5267 if {$nwcol($i)} {
5268 set lncol "gray"
5269 set lnwdt 15
5270 } }
5271 .f$dbox2.c create line \
5272 $TMP1 $YLOC $TMP1 \
5273 [expr $YLOC+$YSZ] \
5274 -width $lnwdt \
5275 -fill $lncol
5276 }
5277 if {[info exists HasBox($YLOC,[expr 1+$pno])]} {
5278 set YLOC [expr $Pstp*$YSZ]
5279 } }
5280 if {$HAS == 1 || $HAS == 2} {
5281 set stmnt [string range $stmnt 8 end]
5282 }
5283 if { [info exists Plabel($pno)] == 0} {
5284 set Plabel($pno) 0
5285 if {$SparseMsc == 0} {
5286 set HasBox($YLOC,[expr 1+$pno]) 1
5287 }
5288 .f$dbox2.c create rectangle \
5289 [expr $XLOC-20] $YLOC \
5290 [expr $XLOC+20] \
5291 [expr $YLOC+$YSZ] \
5292 -outline $Red -fill $Yellow
5293
5294 if {$pname != "TRACK"} {
5295 .f$dbox2.c create text $XLOC \
5296 [expr $YLOC+$YSZ/2] \
5297 -font $SmallFont \
5298 -text "$pname:$pno"
5299 } else {
5300 .f$dbox2.c create text $XLOC \
5301 [expr $YLOC+$YSZ/2] \
5302 -font $SmallFont \
5303 -text "<show>"
5304 }
5305
5306 set YLOC [expr $Pstp*$YSZ]
5307 incr Pstp
5308 for {set i 1} \
5309 {$Pstp > 1 && $i <= $Seenpno} \
5310 {incr i} {
5311 set TMP1 [expr $i*$XSZ]
5312 set lncol $Blue
5313 set lnwdt 1
5314 catch {
5315 if {$nwcol($i)} {
5316 set lncol "gray"
5317 set lnwdt 15
5318 } }
5319 .f$dbox2.c create line \
5320 $TMP1 $YLOC $TMP1 \
5321 [expr $YLOC+$YSZ] \
5322 -width $lnwdt \
5323 -fill $lncol
5324 }
5325 }
5326 if {(1+$pno) > $NPR} {
5327 set NPR [expr $pno+2]
5328 .f$dbox2.c configure \
5329 -scrollregion \
5330 "[expr -$XSZ/2] 0 \
5331 [expr $NPR*$XSZ] [expr $SMX*$YSZ]"
5332 }
5333 if {$Pstp > $SMX-2} {
5334 set SMX [expr 2*$SMX]
5335 .f$dbox2.c configure \
5336 -scrollregion \
5337 "[expr -$XSZ/2] 0 \
5338 [expr $NPR*$XSZ] [expr $SMX*$YSZ]"
5339 }
5340
5341 if { [info exists R($pstp,$pno)] == 0 } {
5342 if {$VERBOSE == 1} {
5343 if {[string first "~W " $stmnt] == 0} {
5344 set BoxFil $White
5345 set stmnt [string range $stmnt 3 end]
5346 } else { if {[string first "~G " $stmnt] == 0} {
5347 set BoxFil $Green
5348 set stmnt [string range $stmnt 3 end]
5349 } else { if {[string first "~R " $stmnt] == 0} {
5350 set BoxFil $Red
5351 set stmnt [string range $stmnt 3 end]
5352 } else { if {[string first "~B " $stmnt] == 0} {
5353 set BoxFil $Blue
5354 set stmnt [string range $stmnt 3 end]
5355 } else { set BoxFil $Yellow } } } }
5356 set BoxLab $stmnt
5357 if {[string first "line " $stmnt] == 0} {
5358 scan $stmnt "line %d" pln
5359 set Fnm "pan_in" ;# not necessarily right...
5360 }
5361 } else {
5362 set BoxLab $pstp
5363 set BoxFil $White
5364 }
5365 if {$SparseMsc == 0} {
5366 set HasBox($YLOC,[expr 1+$pno]) 1
5367 }
5368 set R($pstp,$pno) \
5369 [.f$dbox2.c create rectangle \
5370 [expr $XLOC-20] $YLOC \
5371 [expr $XLOC+20] \
5372 [expr $YLOC+$YSZ] \
5373 -outline $Blue -fill $BoxFil]
5374 set T($pstp,$pno) \
5375 [.f$dbox2.c create text \
5376 $XLOC \
5377 [expr $YLOC+$YSZ/2] \
5378 -font $SmallFont \
5379 -text $BoxLab]
5380 #if {$Pstp > $YNR-2} {
5381 # .f$dbox2.c yview \
5382 # [expr ($Pstp-$YNR)]
5383 #}
5384 }
5385 if { $HAS == 3 } {
5386 .f$dbox2.c itemconfigure \
5387 $R($pstp,$pno) \
5388 -outline $Red -fill $Yellow
5389 }
5390
5391 if {$SYMBOLIC} {
5392 .f$dbox2.c itemconfigure $T($pstp,$pno) \
5393 -font $SmallFont -text "$stmnt"
5394 } else {
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} {
5401 src_line $pln
5402 }
5403 "
5404 .f$dbox2.c bind $T($pstp,$pno) <Any-Leave> "
5405 .f$dbox2.c itemconfigure $T($pstp,$pno) \
5406 -font $SmallFont -text {$pstp}
5407 "
5408 } else {
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} {
5412 src_line $pln
5413 }
5414 "
5415 }
5416 }
5417 }
5418
5419 set YLOC [expr $YLOC+$YSZ/2]
5420 if {$HAS == 1} {
5421 if { [info exists Q_add($inq)] == 0 } {
5422 set Q_add($inq) 0
5423 set Q_del($inq) 0
5424 }
5425 set Slot $Q_add($inq)
5426 incr Q_add($inq) 1
5427
5428 set Mesg_y($inq,$Slot) $YLOC
5429 set Mesg_x($inq,$Slot) $XLOC
5430 set Q_val($inq,$Slot) $Mcont
5431
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 } {
5437 if {$Easy} {
5438 set Slot $Q_del($inq)
5439 incr Q_del($inq) 1
5440 } else {
5441 for {set Slot $Q_del($inq)} \
5442 {$Slot < $Q_add($inq)} \
5443 {incr Slot} {
5444 if {$Q_val($inq,$Slot) == "_X_"} {
5445 incr Q_del($inq) 1
5446 } else {
5447 break
5448 } }
5449
5450 for {set Slot $Q_del($inq)} \
5451 {$Slot < $Q_add($inq)} \
5452 {incr Slot} {
5453 if {$Mcont == $Q_val($inq,$Slot)} {
5454 set Q_val($inq,$Slot) "_X_"
5455 break
5456 } }
5457 }
5458 if {$Slot >= $Q_add($inq)} {
5459 add_log "<<error: cannot match $stmnt>>"
5460 } else {
5461 set TMP1 $Mesg_x($inq,$Slot)
5462 set TMP2 $Mesg_y($inq,$Slot)
5463 if {$XLOC < $TMP1} {
5464 set Delta -20
5465 } else {
5466 set Delta 20
5467 }
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}
5473
5474 if {$SparseMsc == 0} {
5475 set TMP3 5
5476 } else {
5477 set TMP3 0
5478 }
5479
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)
5484 }
5485 } }
5486 }
5487 if {$pln == 0 && ($gvars || $lvars || $qv)} {
5488 if {$Vvbox == 0} {
5489 if {$vv} { set Vvbox [mkbox "Data Values" \
5490 "Vars" "var.out" 71 19 100 350] }
5491 } else {
5492 catch { .c$Vvbox.z.t delete 0.0 end }
5493 }
5494 if {$vv} {
5495 if {$gvars || $lvars} {
5496 raise .c$Vvbox
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" }
5501 } }
5502 }
5503 if {$qv} {
5504 foreach el [lsort [array names Queues]] {
5505 catch {
5506 .c$Vvbox.z.t insert end "queue $el ($Alias($el))\n"
5507 .c$Vvbox.z.t insert end " $Queues($el)\n"
5508 } }
5509 } }
5510 }
5511 } else {
5512 set stepper 0
5513 }
5514 if {$isvar == 0} {
5515 if {$syntax == 1} {
5516 if {[string first "..." $line] < 0} {
5517 add_log "$line"
5518 catch { .c$sbox.z.t insert end "$line\n" }
5519 catch { .c$sbox.z.t yview -pickplace end }
5520 }
5521 } else {
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 }
5525 }
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" }
5530 catch {
5531 set XLOC [expr $Seenpno*$XSZ+$XSZ/2]
5532 set YLOC [expr $Pstp*$YSZ+$YSZ/2]
5533
5534 .f$dbox2.c create text \
5535 [expr $XLOC+$XSZ] $YLOC \
5536 -font $SmallFont \
5537 -text "Cycle/Waiting" \
5538 -fill $Red
5539
5540 .f$dbox2.c create line \
5541 $XLOC $YLOC \
5542 [expr $XLOC+$XSZ/2] $YLOC \
5543 -fill $Red \
5544 -arrow first -arrowshape {5 5 5}
5545 }
5546 set HAS_CYCLE [expr $YLOC+1]
5547 }
5548 if {$m_typ == 2 && $HAS == 3 && $HAS_CYCLE != 0} {
5549 catch {
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] \
5555 $XLOC0 $YLOC \
5556 -fill $Red
5557 .f$dbox2.c create line \
5558 $XLOC0 $YLOC $XLOC $YLOC \
5559 -fill $Red
5560
5561 set XLOC [expr $Seenpno*$XSZ+$XSZ]
5562
5563 .f$dbox2.c create line \
5564 $XLOC $YLOC $XLOC \
5565 [expr $HAS_CYCLE-1] \
5566 -fill $Red
5567 } } } }
5568 # mystery update:
5569 if {$tk_major >= 4 || $m_typ != 1} {
5570 update ;# tk 3.x can crash on this
5571 }
5572
5573 if {$syntax == 0 \
5574 && $stop == 0 \
5575 && $stepped == 1 \
5576 && $stepper == 0 \
5577 && $dontwait == 0} {
5578 update ;# here it is harmless also with tk 3.x
5579 tkwait variable stepper
5580 }
5581 } else {
5582 if {$s_typ == 0 || $s_typ == 2} {
5583 add_log "<at end of run>"
5584 } else {
5585 add_log "<at end of trail>"
5586 }
5587 catch { addscales $dbox2 }
5588 if {$ebc} { barscales }
5589 update
5590 tkwait variable stepper
5591 }
5592 }
5593 # end of guided trail
5594
5595 while {$stepper == 1} {
5596 tkwait variable stepper
5597 }
5598 teardown
5599
5600 catch "close $fd"
5601 add_log "<done>"
5602
5603 update
5604 }
5605
5606 proc teardown {} {
5607 global m_typ pbox sbox dbox Spbox Vvbox
5608 global simruns stop stepped stepper howmany
5609
5610 set simruns 0
5611 set stop 1
5612 set stepped 0
5613 set stepper 0
5614 catch { set howmany 0 }
5615 catch {
5616 if { $m_typ == 1 } {
5617 foreach el [array names pbox] {
5618 catch { destroy .c$pbox($el) }
5619 catch { unset pbox($el) }
5620 }
5621 } elseif { $m_typ == 0 } {
5622 foreach el [array names Spbox] {
5623 catch { destroy .c$Spbox($el) }
5624 catch { unset Spbox($el) }
5625 } }
5626 }
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)]
5631 if {$k > 0} {
5632 set PlaceBox($x) [string range $PlaceBox($x) $k end]
5633 }
5634 destroy .c$sbox
5635 }
5636 catch { destroy .c$dbox }
5637 if {[winfo exists .c$Vvbox]} {
5638 set x "Data Values"
5639 set PlaceBox($x) [wm geometry .c$Vvbox]
5640 set k [string first "\+" $PlaceBox($x)]
5641 if {$k > 0} {
5642 set PlaceBox($x) [string range $PlaceBox($x) $k end]
5643 }
5644 destroy .c$Vvbox
5645 }
5646 }
5647
5648 set PlaceMenu "+150+150"
5649
5650 proc pickoption {nm} {
5651 global howmany Choice PlaceMenu
5652
5653 catch {destroy .prompt}
5654 toplevel .prompt
5655 wm title .prompt "Select"
5656 wm iconname .prompt "Select"
5657 wm geometry .prompt $PlaceMenu
5658
5659 text .prompt.t -relief raised -bd 2 \
5660 -width [string length $nm] -height 1 \
5661 -setgrid 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)" \
5671 -anchor w \
5672 -command "set howmany $i" ] \
5673 {top expand fillx}
5674
5675 set j [string first "line " $Choice($i)]
5676 if {$j > 0} {
5677 set k [string range $Choice($i) $j end]
5678 scan $k "line %d" k
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"
5682 } } }
5683 tkwait variable howmany
5684 set PlaceMenu [wm geometry .prompt]
5685 set k [string first "\+" $PlaceMenu]
5686 if {$k > 0} {
5687 set PlaceMenu [string range $PlaceMenu $k end]
5688 }
5689 catch { foreach el [array names Choice] { unset Choice($el) } }
5690 destroy .prompt
5691 }
5692
5693 proc report {n} {
5694 .inp.t tag remove hilite 0.0 end
5695 if {$n > 0} { src_line $n }
5696 }
5697
5698 # validation options panel
5699
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
5705 set nv_typ 1
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
5711 set waitwhat "none"
5712 set not_warned_yet 1
5713
5714 set LastGenerate ""
5715 set LastCompile ""
5716 set NextCompile ""
5717
5718 proc syntax_check {a T} {
5719 global SPIN BG FG
5720
5721 mkpan_in
5722 add_log "$SPIN $a pan_in"
5723 catch {exec $SPIN $a pan_in >&pan.tmp} err ;# added -v
5724 set cnt 0
5725 set maxln 50
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
5729 set pln 0
5730 set allmsg ""
5731 while {[gets $ef line] > -1} {
5732 add_log "$line"
5733 set allmsg "$allmsg\n$line"
5734 if {[string first "spin: line" $line] >= 0} {
5735 scan $line "spin: line %d" pln
5736 src_line $pln
5737 }
5738 if {[string first "spin: warning, line" $line] >= 0} {
5739 scan $line "spin: warning, line %d" pln
5740 src_line $pln
5741 }
5742 incr cnt
5743 }
5744 close $ef
5745 if {$cnt == 0} { add_log "no syntax errors" } else {
5746 warner $T "$allmsg" 800
5747 }
5748 update
5749 }
5750
5751 proc prescan {} {
5752 global an_typ cp_typ nv_typ po_typ
5753 global xu_typ as_typ ie_typ
5754
5755 mkpan_in
5756
5757 if {$an_typ == -1} {
5758 set an_typ 0
5759 set nv_typ [hasWord "never"]
5760 if {[hasWord "accept.*:"]} {
5761 set an_typ 1
5762 set cp_typ 2
5763 } elseif {[hasWord "progress.*:"]} {
5764 set an_typ 1
5765 set cp_typ 1
5766 }
5767 }
5768 if {$po_typ == -1} {
5769 if {[hasWord "_last"] \
5770 || [hasWord "provided.*\\("] \
5771 || [hasWord "enabled\\("]} {
5772 set po_typ 0
5773 } else {
5774 set po_typ 1
5775 }
5776 }
5777 if {$xu_typ == -1} {
5778 if {[hasWord "xr"] || [hasWord "xs"]} {
5779 set xu_typ 1
5780 } else {
5781 set xu_typ 0
5782 }
5783 }
5784 if {$as_typ == -1} {
5785 if {$an_typ == 0} {
5786 set as_typ [hasWord "assert"]
5787 set ie_typ 1
5788 } else {
5789 set as_typ 0
5790 set ie_typ 0
5791 }
5792 }
5793 }
5794
5795 proc basicval2 {} {
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
5801
5802 set nv_typ 1
5803 set an_typ 1
5804 set cp_typ 2
5805
5806 dump_tl "pan.ltl"
5807
5808 catch { .menu.run.m entryconfigure 8 -state normal }
5809 catch { .tl.results.top.rv configure -state normal }
5810 set stop 0
5811 set firstime 0
5812 set lt_typ 1
5813
5814 catch {destroy .v}
5815 toplevel .v
5816
5817 set k [string first "\+" $PlaceSim]
5818 if {$k > 0} {
5819 set PlaceSim [string range $PlaceSim $k end]
5820 }
5821
5822 wm title .v "LTL Verification Options"
5823 wm iconname .v "VAL"
5824 wm geometry .v $PlaceSim
5825
5826 prescan
5827
5828 frame .v.correct -relief flat -borderwidth 1m
5829 frame .v.cframe -relief raised -borderwidth 1m
5830
5831 set z .v.correct
5832
5833 frame $z.rframe -relief raised -borderwidth 1m
5834
5835 label $z.rframe.lb \
5836 -font $HelvBig \
5837 -text "Options" \
5838 -relief sunken -borderwidth 1m
5839
5840 checkbutton $z.rframe.fc -text "With Weak Fairness" \
5841 -variable cyc_typ \
5842 -relief flat
5843 checkbutton $z.rframe.xu -text "Check xr/xs Assertions" \
5844 -variable xu_typ \
5845 -relief flat
5846
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}
5851
5852 pack append $z $z.rframe {top frame nw filly}
5853
5854 label .v.cframe.lb \
5855 -font $HelvBig \
5856 -text "Verification" \
5857 -relief sunken -borderwidth 1m
5858
5859 radiobutton .v.cframe.ea -text "Exhaustive" \
5860 -variable ct_typ -value 0 \
5861 -relief flat
5862 radiobutton .v.cframe.sa -text "Supertrace/Bitstate" \
5863 -variable ct_typ -value 1 \
5864 -relief flat
5865 radiobutton .v.cframe.hc -text "Hash-Compact" \
5866 -variable ct_typ -value 2 \
5867 -relief flat
5868
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}
5873
5874 frame .v.pf -relief raised -borderwidth 1m
5875 frame .v.pf.mesg -borderwidth 1m
5876
5877 label .v.pf.mesg.loss0 \
5878 -font $HelvBig \
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 \
5883 -relief flat
5884 radiobutton .v.pf.mesg.loss2 -text "Loses New Msgs" \
5885 -variable l_typ -value 1 \
5886 -relief flat
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}
5891 pack append .v.pf \
5892 .v.pf.mesg {left frame w expand fillx}
5893
5894 pack append .v \
5895 .v.cframe {top frame w fill}\
5896 .v.correct {top frame w fill}\
5897 .v.pf {top frame w expand fill}
5898
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}
5908
5909 tkwait visibility .v
5910 raise .v
5911 }
5912
5913 set PlaceBasic "+200+10"
5914 set PlaceAdv "+150+10"
5915
5916 proc basicval {} {
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
5922
5923 catch { .menu.run.m entryconfigure 8 -state normal }
5924 catch { .tl.results.top.rv configure -state normal }
5925 set stop 0
5926 set firstime 0
5927 set lt_typ 0
5928
5929 catch {destroy .v}
5930 toplevel .v
5931
5932 wm title .v "Basic Verification Options"
5933 wm iconname .v "VAL"
5934 wm geometry .v $PlaceBasic
5935
5936 prescan
5937
5938 frame .v.correct -relief flat -borderwidth 1m
5939 frame .v.cframe -relief raised -borderwidth 1m
5940
5941 set z .v.correct
5942
5943 frame $z.rframe -relief raised -borderwidth 1m
5944
5945 label $z.rframe.lb \
5946 -font $HelvBig \
5947 -text "Correctness Properties" \
5948 -relief sunken -borderwidth 1m
5949 radiobutton $z.rframe.sp -text "Safety (state properties)" \
5950 -variable an_typ -value 0 \
5951 -relief flat \
5952 -command { set cyc_typ 0; set cp_typ 0
5953 if {$an_typ == 0} {
5954 set as_typ [hasWord "assert"]
5955 set ie_typ 1
5956 }
5957 }
5958 frame $z.rframe.sf
5959 checkbutton $z.rframe.sf.as -text "Assertions" \
5960 -variable as_typ \
5961 -relief flat \
5962 -command {
5963 set an_typ 0
5964 if {![hasWord "assert"] && $as_typ==1} then {
5965 complain6
5966 }
5967 }
5968 checkbutton $z.rframe.sf.ie -text "Invalid Endstates" \
5969 -variable ie_typ \
5970 -relief flat \
5971 -command { set an_typ 0 }
5972
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}
5978
5979 radiobutton $z.rframe.cp -text "Liveness (cycles/sequences)" \
5980 -variable an_typ -value 1 \
5981 -relief flat \
5982 -command {
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 } \
5986 else complain5
5987 }
5988
5989 frame $z.rframe.sub
5990 radiobutton $z.rframe.sub.np -text "Non-Progress Cycles" \
5991 -variable cp_typ -value 1 \
5992 -relief flat \
5993 -command {
5994 set an_typ 1
5995 if {![hasWord "progress"] && $cp_typ==1} then {
5996 complain4
5997 }
5998 }
5999 radiobutton $z.rframe.sub.ac -text "Acceptance Cycles" \
6000 -variable cp_typ -value 2 \
6001 -relief flat \
6002 -command {
6003 set an_typ 1
6004 if {![hasWord "accept"] && $cp_typ==2} then {
6005 complain1
6006 }
6007 }
6008 checkbutton $z.rframe.sub.fc -text "With Weak Fairness" \
6009 -variable cyc_typ \
6010 -relief flat \
6011 -command { if {$an_typ==0} then "set cyc_typ 0; complain3" }
6012
6013 checkbutton $z.rframe.nv -text "Apply Never Claim (If Present)" \
6014 -variable nv_typ \
6015 -relief flat \
6016 -command { if {![hasWord "never"] && $nv_typ==1} then "complain2" }
6017 checkbutton $z.rframe.ur -text "Report Unreachable Code" \
6018 -variable ur_typ \
6019 -relief flat
6020 checkbutton $z.rframe.xu -text "Check xr/xs Assertions" \
6021 -variable xu_typ \
6022 -relief flat
6023
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}
6030
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}
6040
6041 pack append $z $z.rframe {top frame nw filly}
6042
6043 label .v.cframe.lb \
6044 -font $HelvBig \
6045 -text "Search Mode" \
6046 -relief sunken -borderwidth 1m
6047
6048 radiobutton .v.cframe.ea -text "Exhaustive" \
6049 -variable ct_typ -value 0 \
6050 -relief flat
6051 radiobutton .v.cframe.sa -text "Supertrace/Bitstate" \
6052 -variable ct_typ -value 1 \
6053 -relief flat
6054 radiobutton .v.cframe.hc -text "Hash-Compact" \
6055 -variable ct_typ -value 2 \
6056 -relief flat
6057
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}
6062
6063 frame .v.pf -relief raised -borderwidth 1m
6064 frame .v.pf.mesg -borderwidth 1m
6065
6066 label .v.pf.mesg.loss0 \
6067 -font $HelvBig \
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 \
6072 -relief flat
6073 radiobutton .v.pf.mesg.loss2 -text "Loses New Msgs" \
6074 -variable l_typ -value 1 \
6075 -relief flat
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}
6080 pack append .v.pf \
6081 .v.pf.mesg {left frame nw expand fill}
6082
6083 pack append .v \
6084 .v.correct {left} \
6085 .v.cframe {top frame n expand fill}\
6086 .v.pf {top frame n expand fill}
6087
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}
6101
6102 tkwait visibility .v
6103 raise .v
6104 }
6105
6106 set HasNever ""
6107
6108 proc call_nvr {} {
6109 global HasNever
6110 global xversion Fname nv_typ
6111
6112 switch [info commands tk_getOpenFile] "" {
6113 set fileselect "FileSelect open"
6114 } default {
6115 set fileselect "tk_getOpenFile \
6116 -filetypes { \
6117 { { Aut files } .aut } \
6118 { { Nvr files } .nvr } \
6119 { { All Files } * } \
6120 }"
6121 }
6122
6123 set HasNever [eval $fileselect]
6124
6125 if {$HasNever == ""} {
6126 wm title . "SPIN CONTROL $xversion -- File: $Fname"
6127 set nv_typ 0
6128 } else {
6129 set nv_typ 1
6130 set z [string last "\/" $HasNever]
6131 if {$z > 0} {
6132 incr z
6133 set HsN [string range $HasNever $z end]
6134 } else {
6135 set HsN $HasNever
6136 }
6137 wm title . "SPIN CONTROL $xversion -- File: $Fname Claim: $HsN"
6138 }
6139 }
6140
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
6147
6148 catch { .menu.run.m entryconfigure 8 -state normal }
6149 catch { .tl.results.top.rv configure -state normal }
6150 set stop 0
6151 set firstime 0
6152
6153 catch {destroy .av}
6154 toplevel .av
6155
6156 wm title .av "Advanced Verification Options"
6157 wm iconname .av "VAL"
6158 wm geometry .av $PlaceAdv
6159
6160 frame .av.pans
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
6165
6166 prescan
6167
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)
6173
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}
6179
6180 pack append .av.memopts \
6181 .av.memopts.choice$x { top frame w pady 5 fillx}
6182 }
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)
6188
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}
6194
6195 pack append .av.memopts \
6196 .av.memopts.choice$x { top frame w pady 5 fillx}
6197 }
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)
6203
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}
6209
6210 pack append .av.memopts \
6211 .av.memopts.choice$x { top frame w pady 5 fillx}
6212 }
6213 set z .av.pans.correct
6214 frame $z.rframe -relief raised -borderwidth 1m
6215 label $z.rframe.lb3 \
6216 -font $HelvBig \
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 \
6221 -relief flat
6222 checkbutton $z.rframe.c0a -text "Save All Error-trails" \
6223 -variable st_typ \
6224 -relief flat
6225 checkbutton $z.rframe.c0b -text "Find Shortest Trail (iterative)" \
6226 -variable se_typ \
6227 -relief flat
6228 checkbutton $z.rframe.c0c -text "Use Breadth-First Search" \
6229 -variable bf_typ \
6230 -relief flat
6231 frame $z.rframe.basic1
6232
6233 frame $z.rframe.cc
6234 radiobutton $z.rframe.cc.c1 -text "Stop at Error Nr:" \
6235 -variable et_typ -value 1 \
6236 -relief flat
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}
6242
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}
6252
6253 frame .av.pans.pf -relief flat
6254 set z .av.pans.pf
6255 frame $z.mesg -relief raised -borderwidth 1m; # queue loss options
6256 frame $z.pframe -relief raised -borderwidth 1m
6257 label $z.pframe.lb2 \
6258 -font $HelvBig \
6259 -text " Type of Run " \
6260 -relief sunken -borderwidth 1m
6261 checkbutton $z.pframe.po -text "Use Partial Order Reduction" \
6262 -variable po_typ \
6263 -relief flat
6264 checkbutton $z.pframe.cm -text "Use Compression" \
6265 -variable cm_typ \
6266 -relief flat
6267 # checkbutton $z.pframe.vb -text "Verbose (For Debugging Only)" \
6268 # -variable vb_typ \
6269 # -relief flat
6270 checkbutton $z.pframe.pr -text "Add Complexity Profiling" \
6271 -variable pr_typ \
6272 -relief flat
6273 checkbutton $z.pframe.vr -text "Compute Variable Ranges" \
6274 -variable vr_typ \
6275 -relief flat
6276
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}
6283
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}
6289
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"
6293
6294 pack append .av \
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}
6300
6301 raise .av
6302 }
6303
6304 proc g_list {} {
6305 global FG BG
6306
6307 catch {destroy .r}
6308 toplevel .r
6309
6310 wm title .r "Options"
6311 wm iconname .r "Options"
6312
6313 frame .r.top
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 \
6317 .r.top.list {left}\
6318 .r.top.expl {left}
6319 frame .r.bot
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 \
6324 .r.bot.text {top}\
6325 .r.bot.quit {frame s}
6326
6327 frame .r.caps
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} \
6334 .r.caps.cap2 {left}
6335
6336 pack append .r \
6337 .r.caps {frame w}\
6338 .r.top {top expand} \
6339 .r.bot {bottom expand}
6340
6341 foreach i { "-o1" "-o2" "-o3" } {
6342 .r.top.list insert end $i
6343 }
6344
6345 foreach i { \
6346 "disable dataflow-optimizations" \
6347 "disable dead variables elimination" \
6348 "disable statement merging" } {
6349 .r.top.expl insert end $i
6350 }
6351 bind .r.top.list <Double-Button-1> {
6352 set extra [selection get]
6353 .av.memopts.choice5.e1 insert end " $extra"
6354 destroy .r
6355 }
6356 }
6357
6358 proc r_list {} {
6359 global FG BG
6360
6361 catch {destroy .r}
6362 toplevel .r
6363
6364 wm title .r "Options"
6365 wm iconname .r "Options"
6366
6367 frame .r.top
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 \
6371 .r.top.list {left}\
6372 .r.top.expl {left}
6373 frame .r.bot
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 \
6378 .r.bot.text {top}\
6379 .r.bot.quit {frame s}
6380
6381 frame .r.caps
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} \
6388 .r.caps.cap2 {left}
6389
6390 pack append .r \
6391 .r.caps {frame w}\
6392 .r.top {top expand} \
6393 .r.bot {bottom expand}
6394
6395 foreach i { "-d" "-q" "-I" "-h?" "-s" "-A" "-E" "-w?" } {
6396 .r.top.list insert end $i
6397 }
6398
6399 foreach 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" \
6408 "" } {
6409 .r.top.expl insert end $i
6410 }
6411 bind .r.top.list <Double-Button-1> {
6412 set extra [selection get]
6413 .av.memopts.choice4.e1 insert end " $extra"
6414 destroy .r
6415 }
6416 }
6417
6418 proc d_list {nr} {
6419
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 }
6427
6428 catch {destroy .b}
6429 toplevel .b
6430
6431 wm title .b "Options"
6432 wm iconname .b "Options"
6433
6434 frame .b.top
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}
6440
6441 frame .b.bot
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}\
6448 .b.bot.expl {left}\
6449 .b.bot.quit {left}
6450
6451
6452 pack append .b \
6453 .b.top {top frame nw expand} \
6454 .b.bot {bottom}
6455
6456 foreach i { \
6457 "-DBCOMP" \
6458 "-DCTL" \
6459 "-DGLOB_ALPHA" \
6460 "-DMA=?" \
6461 "-DNFAIR=?" \
6462 "-DNIBIS" \
6463 "-DNOBOUNDCHECK" \
6464 "-DNOREDUCE" \
6465 "-DNOCOMP" \
6466 "-DNOSTUTTER" \
6467 "-DNOVSZ" \
6468 "-DPRINTF" \
6469 "-DRANDSTORE=?" \
6470 "-DR_XPT" \
6471 "-DSDUMP" \
6472 "-DSVDUMP" \
6473 "-DVECTORSZ=?" \
6474 "-DW_XPT=?" \
6475 "-DXUSAFE" \
6476 } {
6477 .b.top.list insert end $i
6478 }
6479 bind .b.top.list <Double-Button-1> {
6480 set directive [selection get]
6481 .av.memopts.choice3.e1 insert end " $directive"
6482 destroy .b
6483 }
6484 }
6485
6486 proc complain1 {} {
6487 set m "warning: there are no accept labels"
6488 add_log $m
6489 catch { tk_messageBox -icon info -message $m }
6490 }
6491
6492 proc complain2 {} {
6493 set m "warning: there is no never claim"
6494 add_log $m
6495 catch { tk_messageBox -icon info -message $m }
6496 }
6497
6498 proc complain3 {} {
6499 set m "weak fairness is irrelevant to state properties"
6500 add_log $m
6501 catch { tk_messageBox -icon info -message $m }
6502 }
6503
6504 proc complain4 {} {
6505 set m "warning: there are no progress labels"
6506 add_log $m
6507 catch { tk_messageBox -icon info -message $m }
6508 }
6509
6510 proc complain5 {} {
6511 global an_typ
6512 set m "warning: there are neither accept nor progress labels"
6513 add_log $m
6514 set an_typ 0
6515 catch { tk_messageBox -icon info -message $m }
6516 }
6517
6518 proc complain6 {} {
6519 set m "warning: there are no assert statements in the spec"
6520 add_log $m
6521 catch { tk_messageBox -icon info -message $m }
6522 }
6523
6524 proc complain7 {} {
6525 set m "warning: Breadth-First Search implies a restriction to Safety properties"
6526 add_log $m
6527 catch { tk_messageBox -icon info -message $m }
6528 }
6529
6530 proc complain8 {} {
6531 set m "error: cannot combine -DMA and -DBITSTATE"
6532 add_log $m
6533 catch { tk_messageBox -icon info -message $m }
6534 }
6535
6536 proc stopval {how} {
6537 global stop ival PlaceAdv
6538
6539 if {$how} {
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]"
6548 }
6549 set stop 1
6550 if {[winfo exists .av]} {
6551 set PlaceAdv [wm geometry .av]
6552 set k [string first "\+" $PlaceAdv]
6553 if {$k > 0} {
6554 set PlaceAdv [string range $PlaceAdv $k end]
6555 }
6556 destroy .av
6557 }
6558 }
6559
6560 proc log {n} {
6561 set m 1
6562 set cnt 0
6563 while {$m<$n} {
6564 set m [expr $m*2]
6565 incr cnt
6566 }
6567 return $cnt
6568 }
6569
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
6577
6578 set ol_typ $l_typ
6579 set oct_typ $ct_typ
6580
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] }
6584
6585 set Mbytes $ival(0)
6586 catch { set Mbytes [.av.memopts.choice0.e1 get] }
6587
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]]] }
6591 set Mdepth $ival(2)
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]" }
6600
6601 if {$ct_typ == 2} { ;# hash-compact
6602 set c_options [format "-DHC -DMEMLIM=%d" $Mbytes]
6603
6604 # in exhaustive mode: #hashtable ~~ #states
6605
6606 set v_options "-X -m$Mdepth -w$Mstate"
6607
6608 if {$Mstate >= $Mbytes} {
6609 catch {
6610 tk_messageBox -icon info \
6611 -message "The Estimated Statespace size exceeds \
6612 the maximum that the Memory limit you set would allow."
6613 }
6614 return 0
6615 }
6616 } elseif {$ct_typ==1} {
6617 set c_options [format "-DBITSTATE -DMEMLIM=%d" $Mbytes]
6618
6619 # in supertrace mode: #bits ~~ 128x #states
6620 # (effectively the #bytes will be ~~ 16x #states)
6621
6622 set Mstate [expr 7+$Mstate]
6623 set v_options "-X -m$Mdepth -w$Mstate"
6624
6625 if {$Mstate-3 >= $Mbytes} {
6626 catch {
6627 tk_messageBox -icon info \
6628 -message "The Estimated Statespace size exceeds \
6629 maximum allowed by the Memory limit that you set would allow."
6630 }
6631 return 0
6632 }
6633 } else {
6634 set c_options [format "-DMEMLIM=%d" $Mbytes]
6635
6636 # in exhaustive mode: #hashtable ~~ #states
6637
6638 set v_options "-X -m$Mdepth -w$Mstate"
6639
6640 if {$Mstate >= $Mbytes} {
6641 catch {
6642 tk_messageBox -icon info \
6643 -message "The Estimated Statespace size exceeds \
6644 the maximum that the Physical Memory limit allows."
6645 }
6646 return 0
6647 }
6648 }
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] }
6657 if {$bf_typ!=0} {
6658 if {$an_typ != 0} {
6659 complain7
6660 set c_options [format "%s -DBFS -DSAFETY" $c_options]
6661 } else {
6662 set c_options [format "%s -DBFS" $c_options]
6663 } }
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] }
6667 if {$cyc_typ==1} {
6668 set c_options [format "%s -DNFAIR=3" $c_options]
6669 } else {
6670 set c_options [format "%s -DNOFAIR" $c_options]
6671 }
6672 set foo $ival(3)
6673 catch { set foo [.av.memopts.choice3.e1 get] }
6674
6675 if {[string first "-DBITSTATE" $c_options] > 0 && [string first "-DMA" $foo] > 0} {
6676 complain8
6677 }
6678 set c_options [format "%s %s" $c_options $foo ]
6679
6680 set foo $ival(4)
6681 catch { set foo [.av.memopts.choice4.e1 get] }
6682 set v_options [format "%s %s" $v_options $foo ]
6683
6684 set foo $ival(5)
6685 catch { set foo [.av.memopts.choice.5.e1 get] }
6686 set a_options [format "%s %s" $a_options $foo ]
6687
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)] }
6699 return 1
6700 }
6701
6702 set mt 0
6703 set skipmax 10
6704
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
6711
6712 set stop 0
6713 if {[bld_v_options] == 0} {
6714 advanced_val
6715 return
6716 }
6717 if {[winfo exists .v]} {
6718 set PlaceSim [wm geometry .v]
6719 destroy .v
6720 }
6721 catch {destroy .av}
6722 if {[string first "\?" $c_options] > 0} {
6723 add_log "error: undefined '?' in optional compiler directives"
6724 return
6725 }
6726 if {[string first "\?" $v_options] > 0} {
6727 add_log "error: undefined '?' in extra runtime options"
6728 return
6729 }
6730 add_log "<starting verification>"
6731 if {$havedest != "0"} {
6732 $havedest insert end "<starting verification>\n"
6733 }
6734
6735 set nochange [no_change]
6736 if {$nochange == 0} { set LastGenerate "" }
6737
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"
6742 }
6743 set errmsg 0
6744 } else {
6745 set LastCompile ""
6746 add_log "$SPIN $a_options pan_in"; update
6747 if {$havedest != "0"} {
6748 $havedest insert end "$SPIN $a_options pan_in\n"
6749 }
6750 if {$Unix} {
6751 catch {eval exec $SPIN $a_options pan_in} errmsg
6752 } else {
6753 catch {eval exec $SPIN $a_options pan_in >&pan.tmp}
6754 set errmsg [msg_file pan.tmp 0]
6755 }
6756 if {[string length $errmsg]>0} {
6757 set foo [string first "Exit-Status 0" $errmsg]
6758 if {$foo<0} {
6759 add_log "$errmsg"
6760 if {$havedest != "0"} {
6761 $havedest insert end "$errmsg\n"
6762 }
6763 update
6764 return
6765 }
6766 incr foo -2
6767 set errmsg [string range $errmsg 0 $foo]
6768 add_log "$errmsg"
6769 if {$havedest != "0"} {
6770 $havedest insert end "$errmsg\n"
6771 }
6772 } }
6773 set LastGenerate $a_options
6774
6775 set NextCompile "$CC -o pan $c_options pan.c"
6776
6777 if {$havedest != "0"} {
6778 catch { $havedest yview -pickplace end }
6779 }
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"
6784 }
6785 set errmsg 0
6786 } else {
6787 add_log $NextCompile
6788 if {$havedest != "0"} {
6789 $havedest insert end "$NextCompile\n"
6790 }
6791 catch {
6792 warner "Compiling" "Please wait until compilation of the \
6793 executable produced by spin completes." 300
6794 }
6795 update
6796 if {$Unix} {
6797 rmfile "./pan"
6798 catch {eval exec $NextCompile >pan.tmp 2>pan.err}
6799 } else {
6800 rmfile "pan.exe"
6801 catch {eval exec $NextCompile >pan.tmp 2>pan.err}
6802 }
6803
6804 set errmsg [msg_file pan.tmp 0]
6805 if {[string length $errmsg] == 0} {
6806 set errmsg [msg_file pan.err 0]
6807 } else {
6808 set errmsg "$errmsg\n[msg_file pan.err 0]"
6809 }
6810
6811 catch {destroy .warn}
6812
6813 auto_reset
6814 if {$Unix} {
6815 if {[auto_execok "./pan"] == "" \
6816 || [auto_execok "./pan"] == 0} {
6817 add_log "$errmsg"
6818 add_log "compilation failed"
6819 if {$havedest != "0"} {
6820 $havedest insert end "<compilation failed>\n"
6821 }
6822 update
6823 return
6824 }
6825 } else {
6826 if {[auto_execok "pan"] == "" \
6827 || [auto_execok "pan"] == 0} {
6828 add_log "$errmsg"
6829 add_log "compilation failed"
6830 if {$havedest != "0"} {
6831 $havedest insert end "<compilation failed>\n"
6832 }
6833 update
6834 return
6835 } } }
6836
6837 set LastCompile $NextCompile
6838 set NextCompile ""
6839
6840 if {$Unix} {
6841 set PREFIX "time ./pan -v"
6842 } else {
6843 set PREFIX "pan -v"
6844 }
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 }
6849 }
6850 set errmsg ""
6851 update
6852 rmfile pan.out
6853 set errmsg [catch {eval exec $PREFIX $v_options >&pan.out &}]
6854 if {$errmsg} {
6855 add_log "$errmsg"
6856 add_log "could not run verification"
6857 if {$havedest != "0"} {
6858 $havedest insert end "<could not run verification>\n"
6859 }
6860 update
6861 return
6862 }
6863
6864 set not_warned_yet 1
6865 if {$havedest != "0"} {
6866 set vbox $havedest
6867 } else {
6868 set vv [mkbox "Verification Output" "VerOut" "$Fname.out" 80 20]
6869 set vbox .c$vv.z.t
6870 }
6871 update
6872 set mt 0
6873 after 5000 outcheck $vbox
6874 update
6875 }
6876
6877 proc outcheck {vbox} {
6878 global stop where not_warned_yet runtime mt Unix Fname FG skipmax
6879
6880 set firstline 1
6881 set have_trail 0
6882 set po_red_viol 0
6883
6884 if {[winfo exists $vbox] == 0} {
6885 add_log "<verification output panel $vbox was closed>"
6886 return
6887 }
6888
6889 set erline 0; set lnr 0
6890 set nomem 0; set nerr 0
6891
6892 if {$stop == 0} {
6893 catch { set nt [file mtime pan.out] }
6894 if {$mt == $nt && $skipmax > 0} {
6895 incr skipmax -1
6896 } else {
6897 set mt $nt
6898 set skipmax 10
6899 set fd [open pan.out r]
6900 while {[gets $fd line] > -1} {
6901 if {$firstline} {
6902 set firstline 0
6903 set nerr 0
6904 set trunc 0
6905 set nomem 0
6906 .inp.t tag remove hilite 0.0 end
6907 catch { $vbox delete 0.0 end }
6908 set lnr 0
6909 }
6910 catch { $vbox insert end "$line\n" }
6911 incr lnr
6912 catch { $vbox yview -pickplace end }
6913 update
6914
6915 if {[string first "line" $line]>=0} {
6916 scan $line "\tline %d" where
6917 catch { src_line $where }
6918 }
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]
6924 if {$nerr > 0} {
6925 set part [string range $line $nerr end]
6926 scan $part "errors: %d" nerr
6927 if {$nerr == 0} {
6928 catch { .tl.results.top.title configure\
6929 -text "Verification Result: valid" -fg $FG
6930 }
6931 } else {
6932 catch { .tl.results.top.title configure\
6933 -text "Verification Result: not valid" -fg red
6934 }
6935 }
6936 set erline $lnr
6937 incr erline -1
6938 }
6939 }
6940 if {[string first "search depth too small" $line]>0} {
6941 set trunc 1
6942 }
6943 if {[string first "wrote pan_in.trail" $line]>0} {
6944 set have_trail 1
6945 }
6946 if {[string first "violated: access to chan" $line]>0} {
6947 set po_red_viol 1
6948 }
6949 if {[string first "out of memory" $line]>0} {
6950 set nomem 1
6951 }
6952 if {[string first "A=atomic;" $line]>0} {
6953 set stop 1
6954 }
6955 update
6956 }
6957 catch "close $fd"
6958 } }
6959 if {$nomem || $po_red_viol} { set erline 0 }
6960
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
6969 }
6970 catch { repeatbox $nerr $trunc $nomem }
6971 }
6972 } else {
6973 if {$not_warned_yet} {
6974 set runtime 0
6975 set stop 0
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" }
6980 if {$Unix == 0} {
6981 set line "\t(use ctl-alt-del to kill pan)"
6982 catch { $vbox insert end "$line\n" }
6983 } else {
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 }
6987 }
6988 set not_warned_yet 0
6989 } else {
6990 incr runtime 5
6991 if {$stop} {
6992 add_log "<done>"
6993 return
6994 } else {
6995 if {$runtime%60 == 0} {
6996 set rt [expr $runtime / 60]
6997 add_log "verification now running for approx $rt min.."
6998 }}
6999 update
7000 }
7001 after 5000 outcheck $vbox
7002 }
7003 }
7004
7005 proc src_line {s} {
7006 global FG BG
7007 scan $s %d tgt_lnr
7008
7009 if {$tgt_lnr > 0} {
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]
7014 } else {
7015 .inp.t yview -pickplace [expr $tgt_lnr-1]
7016 }
7017 }
7018 }
7019
7020 proc repeatbox { {nerr} {trunc} {nomem}} {
7021 global s_typ PlaceWarn whichsim
7022
7023 if {$nerr <= 0 && $trunc <= 0 && $nomem <= 0} { return }
7024
7025 catch {destroy .rep}
7026 toplevel .rep
7027
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 }
7036
7037 if {$nerr>0} {
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.
7041
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)."
7046 set s_typ 1
7047 set whichsim 0
7048
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}
7053 } else {
7054
7055 if {$nomem>0} {
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."
7063 } else {
7064
7065 if {$trunc} {
7066
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."
7073 }
7074 }
7075 pack append .rep .rep.t {top expand fill}
7076 pack append .rep .rep.b0 {right}
7077 }
7078 }
7079
7080 # Main startup and arg processing
7081 # this is at the end - to make sure all
7082 # proc declarations were seen
7083
7084 if {$argc == 1} {
7085 set Fname "$argv"
7086 wm title . "SPIN CONTROL $xversion -- File: $Fname"
7087 cleanup 0
7088 cpfile $argv.trail pan_in.trail
7089 reopen
7090
7091 check_xsp $argv
7092 }
7093
7094 focus .inp.t
7095 update
LTTng 2.x Viewer (LTTV)
This page took 0.22964 seconds and 4 git commands to generate.