#!/usr/sfw/bin/wish8.3 -f
# the next line restarts using wish \
exec wish c:/cygwin/bin/xspin -- $*

# cd	;# enable to cd to home directory by default

# on PCs:
# adjust the first argument to wish above with the name and
# location of this tcl/tk file on your system, if different.
#
# Cygwin:
# if you use cygwin, do not refer to the file as /usr/bin/xspin
# /usr/bin is a symbolic link to /bin, which really
# lives in c:/cygwin, hence the contortions above
#
# on Unix/Linux/Solaris systems
# replace the first line with something like
#	#!/usr/bin/wish -f
# using the pathname for the wish executable on your system

#======================================================================#
# Tcl/Tk Spin Controller, written by Gerard J. Holzmann, 1995-2004.    #
# See the README.html file for full installation notes.                #
#        http://spinroot.com/spin/whatispin.html                       #
#======================================================================#
set xversion "4.2.3 -- 5 February 2005"

# -- Xspin Installation Notes (see also README.html):

# 1. On Unix systems: change the first line of this file to point to the wish
#    executable you want to use (e.g., wish4.2 or /usr/local/bin/wish8.0)
#    ==> be careful, the pathname should be 30 characters or less
#
# 2. If you use another C compiler than gcc, change the set CC line below
#
# 3. Browse the configurable options below if you would like to
#    change or adjust the visual appearance of the GUI
#
# 4. If you run on a PC, and have an ancient version of tcl/tk,
#    you must set the values fo Unix, CMD, and Go32 by hand below
#    => with Tcl/Tk 7.5/4.1 or later, this happens automatically

# set CC   "cc -w -Wl -woff,84"	;# ANSI-C compiler, suppress warnings
# set CC   "cl -w -nologo"	;# Visual Studio C/C++ compiler, prefered on PCs
  set CC   "gcc -w"		;# standard gcc compiler - no warnings
  set CC0  "gcc"

# set CPP  "cpp"		;# the normal default C preprocessor
  set CPP  "gcc -E -x c"	;# c preprocessor, assuming we have gcc

  set SPIN "/mit/spin_v4.2.5/bin/spin.real"	;# use a full path-name if necessary, e.g. c:/cygwin/bin/spin.exe
  set DOT  "/mit/spin_v4.2.5/bin/dot.real"	;# optional, graph layout interface
  			;# no prob if dot is not available
  set BG   "white"	;# default background color for text
  set FG   "black"	;# default foreground color for text
  set CMD  ""		;# default is empty, and adjusted below
  set Unix 1		;# default is Unix, but this is adjusted below
  set Ptype "color"	;# printer-type: mono, color, or gray
  set NT 0		;# scratch variable, ignore

  set debug_on 0
  if {$debug_on} {
	toplevel .debug ;   #debugging window
	text .debug.txt -width 80 -height 60 -relief raised -bd 2 \
		-yscrollcommand ".debug.scroll set"
	scrollbar .debug.scroll -command ".debug.txt yview"
	pack .debug.scroll -side right -fill y
	pack .debug.txt -side left
  }
  proc debug {txt} {
	global debug_on
	if {$debug_on} {
	catch { .debug.txt insert end "\n$txt" }
  }	}

  if [info exists tcl_platform] {
	set sys $tcl_platform(platform)
#	if {$sys == "macintosh"} {
#		... no adjustments needed? ...
#	}
        if {[string match windows $sys]} {
		set Unix 0	;# means Windows95/98/2000/NT/XP

		if {[auto_execok cl] != ""} {
			set CC   "cl -w -nologo"	;# Visual Studio compiler, PCs
			set CC0  "cl"
		}

		if {$tcl_platform(os) == "Windows 95"} {
			set CMD  "command.com"	;# Windows95
		} else {
			set CMD  "cmd"
			set NT 1
  }	}	}

#-- GUI configuration options - by Leszek Holenderski <lhol@win.tue.nl>
#-- basic text size:
	set HelvBig	-Adobe-Helvetica-Medium-R-Normal--*-120-*-*-*-*-*-*
# mscs:
	if {$NT} {	;# on a windows nt machine
	set SmallFont	"-*-Courier-Bold-R-Normal--*-110-*"
	set BigFont	"-*-Courier-Bold-R-Normal--*-110-*"
	} else {
	set SmallFont	"-*-Courier-Bold-R-Normal--*-80-*"
	set BigFont	"-*-Courier-Bold-R-Normal--*-80-*"
	}

# Some visual aspects of Xspin GUI can be configured by the user.
# On PCs, the values of configuration options that are hard-coded
# into this script can be modified (see below). On Unix, in addition to
# (or rather, instead of) the manual modification, the values can be set in
# an Xspin resource file ($HOME/.xspinrc) and/or in the X11 default resource
# file (usually, $HOME/.Xdefaults).

# Since the same option can be specified in several places, options can have
# several, possibly inconsistent, values. The value which takes effect is
# determined by the order in which options are scanned. The values specified
# later in the order have higher priority. First, hard-coded options are
# scanned, then options specified in .Xdefaults, and finally options
# specified in .xspinrc.

# When setting configuration options in an .xspinrc file, convert the 
# settings below to the format of an X11 resource file. For example,
#
#	# width of scrollbars (any Tk dimension, default 15 pixels)
#	option add *Scrollbar.width	13	startupFile
#
# should be converted to
#
#	! width of scrollbars (any Tk dimension, default 15 pixels)
#	*Scrollbar.width	13
# In .Xdefaults file, configuration options should be preceded by the
# application's name, so the above option should be converted to
#
#	! width of scrollbars (any Tk dimension, default 15 pixels)
#	xspin*Scrollbar.width	13
# side on which side scrollbars are put (left or right, default=right)

option add *Scrollbar.side	left	startupFile

#--- sizes
	# width of scrollbars (any Tk dimension, default 15 pixels)
	option add *Scrollbar.width	13	startupFile
	# width of borders (in pixels, typically 1 or 2, default 2)
	option add *borderWidth		1	startupFile
	# initial width of the input/log area (in characters, default 80)
	option add *Input*Text.width	72	startupFile
	option add *Log*Text.width	72	startupFile
	# initial height of the input area (in lines, default 24)
	option add *Input*Text.height	20	startupFile
	# initial height of the log area (in lines, default 24)
	option add *Log*Text.height	5	startupFile
	# size of the handle used to adjust the height of the log area
	# (in pixels, default 0)
	option add *Handle.width	10	startupFile
	option add *Handle.height	10	startupFile
#--- colors
	# colors for the input/log area
	option add *Input*Text.background	white	startupFile
	option add *Input*Text.foreground	black	startupFile
	option add *Log*Text.background		gray95	startupFile
	option add *Log*Text.foreground		black	startupFile
	# colors for the editable/read-only area
	option add *Entry.background		white	startupFile
	option add *Edit*Text.background	white	startupFile
	option add *Edit*Text.foreground	black	startupFile
	# colors for the editable/read-only area
	option add *Read*Text.background	gray95	startupFile
	option add *Read*Text.foreground	black	startupFile
#--- fonts
	# fonts for the input/log area (default is system dependent,
	# usually -*-Courier-Medium-R-Normal--*-120-*)
option add *Input*Text.font	-*-Helvetica-Medium-R-Normal--*-120-*	startupFile
#option add *Input*Text.font	-schumacher-clean-medium-r-normal--*-120-*-60-*	startupFile
#option add *Log*Text.font	-schumacher-clean-medium-r-normal--*-120-*-60-*	startupFile

#--- widgets
	# simple texts (dialogs which present read-only texts, such as help)
	option add *SimpleText.Text.width 60
	option add *SimpleText.Text.height 30
	option add *SimpleText.Text.background white

	# sections (decorated frames for grouping related buttons)
	option add *Section*Title.font		-*-Helvetica-Bold-R-Normal--*-100-*	startupFile

#option add *Section*Checkbutton.font	-*-Helvetica-Medium-R-Normal--*-100-*	startupFile
#option add *Section*Radiobutton.font	-*-Helvetica-Medium-R-Normal--*-100-*	startupFile
#option add *Section*Label.font		-*-Helvetica-Medium-R-Normal--*-100-*	startupFile

################ end of configurable parameters #######################

wm title . "SPIN CONTROL $xversion"
wm iconname . "SPIN"
wm geometry . +50+50
wm minsize  . 400 200

set Fname ""
set firstime 1
set notignored 0

#### seed the advanced parameters settings

set e(0)	"Physical Memory Available (in Mbytes): "
set ival(0)	128
set expl(0)	"explain"

set e(1)	"Estimated State Space Size (states x 10^3): "
set ival(1)	500
set expl(1)	"explain"

set e(2)	"Maximum Search Depth (steps): "
set ival(2)	10000
set expl(2)	"explain"

set e(7)	"Nr of hash-functions in Bitstate mode: "
set ival(7)	2
set expl(7)	"explain"

set e(3)	"Extra Compile-Time Directives (Optional): "
set ival(3)	""
set expl(3)	"Choose"

set e(4)	"Extra Run-Time Options (Optional): "
set ival(4)	""
set expl(4)	"Choose"

set e(5)	"Extra Verifier Generation Options: "
set ival(5)	""
set expl(5)	"Choose"

set ival(6)	1	;# which error is reported, default is 1st


# allow no more than one entry per selection
catch { tk_listboxSingleSelect Listbox }

proc msg_file {f nowarn} {
	set msg ""
	set ef [open $f r]

	while {[gets $ef line] > -1} {
		if {$nowarn} {
			if {[string first "warning" $line] < 0} {
				set msg "$msg\n$line"
			}
		} else {
			set msg "$msg\n$line"
	}	}
	close $ef
	return $msg
}

	scan $tk_version "%d.%d" tk_major tk_minor

	set version ""

	if {[auto_execok $SPIN] == "" \
	||  [auto_execok $SPIN] == 0} {
		set version "Error: No executable $SPIN found..."
	} else {
		if {$Unix} {
			set version [exec $SPIN -V]
		} else {
			catch { exec $SPIN -V >&pan.tmp } err
			if {$err == ""} {
				set version [msg_file pan.tmp 1]
			} else {
				puts "error: $err"
				puts "is there a $SPIN and a go32.exe?"
				exit
		}	}
		if {[string first "Spin Version 3" $version] < 0 \
		&&  [string first "Spin Version 4" $version] < 0 } {
			set version "Spin Version not recognized: $version"
		}
	}

frame .menu
	# top level menu bar
	menubutton .menu.file -text "File.." \
		-relief raised -menu .menu.file.m
	menubutton .menu.run -text "Run.." -fg red \
		-relief raised -menu .menu.run.m
	menubutton .menu.edit -text "Edit.." \
		-relief raised -menu .menu.edit.m
	menubutton .menu.view -text "View.." \
		-relief raised -menu .menu.view.m
	label .menu.title -text "SPIN  DESIGN  VERIFICATION" -fg blue

	set lno 1
	label .menu.lno -text "Line#:" -relief raised 
	entry .menu.ent -width 6 -textvariable lno \
		-relief sunken -background white -foreground black
	bind  .menu.ent <Return> {
		.inp.t tag remove hilite 0.0 end
		.inp.t tag add hilite $lno.0 $lno.1000
		.inp.t tag configure hilite -background $FG -foreground $BG
		.inp.t yview -pickplace [expr $lno-4]
	}

	label .menu.fnd1 -text "Find:" -relief raised 
	entry .menu.fnd2 -width 8 -textvariable pat \
		-relief sunken -background white -foreground black
	bind  .menu.fnd2 <Return> {
		.inp.t tag remove hilite 0.0 end
		forAllMatches .inp.t $pat
	}

	menubutton .menu.help -text "Help" -relief raised \
		-menu .menu.help.m

	pack append .menu \
		.menu.file {left frame w} \
		.menu.edit {left frame w} \
		.menu.view {left frame w} \
		.menu.run {left frame w} \
		.menu.help {left frame w} \
		.menu.title {left frame c expand} \
		.menu.fnd2 {right frame e} \
		.menu.fnd1 {right frame e} \
		.menu.ent {right frame e} \
		.menu.lno {right frame e}

set loglines 5
frame .log
	text .log.t -bd 2 -height $loglines -background $FG -foreground $BG
frame .log.b
	button .log.b.pl -text "+" \
		-command {incr loglines  1; .log.t configure -height $loglines}
	button .log.b.mn -text "-" \
		-command {incr loglines -1; .log.t configure -height $loglines}
	pack append .log.b .log.b.pl {top}
	pack append .log.b .log.b.mn {top}
	pack append .log .log.b {left filly}
	pack append .log .log.t {right expand fill}

proc dopaste {} {
	global FG BG
	set from [.inp.t index insert]
	tk_textPaste .inp.t
	set upto [.inp.t index insert]
	.inp.t tag add sel $from $upto
#	.inp.t tag configure hilite -background $FG -foreground $BG
}

#- fetch the value of user-defined configuration options

proc fetchOption {name default args} {

  set class Dummy
  set fullName $name

  # class encoded in name ?
  switch -glob -- $name *.* {
    set list [split $name .]
    switch [llength $list] 2 {} default { error "wrong option \"$name\" }
    set class [lindex $list 0]
    set name  [lindex $list 1]
  }

  # create a unique dummy frame of requested class and get the option's value
  set dummy .0
  while {[winfo exists $dummy]} { append dummy 0 }
  frame $dummy -class $class
  set value [option get $dummy $name $class]
  destroy $dummy

  # option not defined ?
  switch -- $value "" { return $default }

  # check a restriction on option's value
  switch [llength $args] {
    0 { # no restriction
      }
    1 { # restriction is given as a list of allowed values
        switch -- [lsearch -exact [lindex $args 0] $value] -1 {
          set msg "wrong value \"$value\" of option \"$fullName\"\
                   (should be one of $args)"
          return -code error -errorinfo $msg $msg
        }
      }
    2 { # restriction is given as a range (min and max)
        set min [lindex $args 0]
        set max [lindex $args 1]
        if {$value < $min} { set $value $min }
        if {$value > $max} { set $value $max }
      }
    default {
      error "internal error in fetchOption: wrong restriction \"$args\""
    }
  }

  return $value
}

# width of borders
set BD [fetchOption borderWidth 1 0 4]
#option add *Text.highlightThickness $BD startupFile

# scrollbar's side
set scrollbarSide [fetchOption Scrollbar.side right {left right}]

frame .inp
	# view of spin input
	scrollbar .inp.s  -command ".inp.t yview"
	text .inp.t -bd 2  -font $HelvBig -yscrollcommand ".inp.s set" -wrap word

	pack .inp.s -side $scrollbarSide -fill y
	pack append .inp \
		.inp.t {left expand fill}

	menu .inp.t.edit -tearoff 0
	.inp.t.edit add command -label "Cut" \
		-command {tk_textCopy .inp.t; tk_textCut .inp.t}
	.inp.t.edit add command -label "Copy" \
		-command {tk_textCopy .inp.t}
	.inp.t.edit add command -label "Paste" \
		-command {dopaste}

	bind .inp.t <ButtonPress-3> {
		tk_popup .inp.t.edit %X %Y
	}
	bind .inp.t <ButtonRelease-1> { setlno }


set l_typ 0;	# used by both simulator and validator
set lt_typ 0;	# used by ltl panel
set ol_typ -1;	# remembers setting last used in compilation
set m_typ 2;	# used by simulator

menu .menu.file.m
	.menu.file.m add command -label "New"  \
		-command ".inp.t delete 0.0 end"
#	.menu.file.m add command -label "UnSelect" \
#		-command ".inp.t tag remove hilite 0.0 end;\
#			  .inp.t tag remove Rev 0.0 end;\
#			  .inp.t tag remove sel 0.0 end"
	.menu.file.m add command -label "ReOpen" -command "open_spec"
	.menu.file.m add command -label "Open.." -command "open_spec 0"
	.menu.file.m add command -label "Save As.." -command "save_spec 0"
	.menu.file.m add command -label "Save" -command "save_spec"
	.menu.file.m add command -label "Quit" \
		-command "cleanup 1; destroy .; exit"

menu .menu.help.m
	.menu.help.m add command -label "About Spin" \
		-command "aboutspin"
	.menu.help.m add separator
	.menu.help.m add command -label "Promela Usage" \
		-command "promela"
	.menu.help.m add command -label "Xspin Usage" \
		-command "helper"
	.menu.help.m add command -label "Simulation" \
		-command "roadmap1"
	.menu.help.m add command -label "Verification" \
		-command "roadmap2"
	.menu.help.m add command -label "LTL Formulae" \
		-command "roadmap4"
	.menu.help.m add command -label "Spin Automata View" \
		-command "roadmap5"
	.menu.help.m add command -label "Reducing Complexity" \
		-command "roadmap3"

menu .menu.run.m
	.menu.run.m add command -label "Run Syntax Check" \
		-command {syntax_check "-a -v" "Syntax Check"}
	.menu.run.m add command -label "Run Slicing Algorithm" \
		-command {syntax_check "-A" "Property-Specific Slicing"}
	.menu.run.m add separator
	.menu.run.m add command -label "Set Simulation Parameters.." \
		-command simulation
	.menu.run.m add command -label "(Re)Run Simulation" \
		-command Rewind -state disabled
	.menu.run.m add separator
	.menu.run.m add command -label "Set Verification Parameters.." \
		-command basicval
	.menu.run.m add command -label "(Re)Run Verification" \
		-command {runval "0"} -state disabled
	.menu.run.m add separator
	.menu.run.m add command -label "LTL Property manager.." \
		-command call_tl
	.menu.run.m add separator
	.menu.run.m add command -label "View Spin Automaton for each Proctype.." \
		-command fsmview


menu .menu.edit.m
	.menu.edit.m add command -label "Cut" \
		-command {tk_textCopy .inp.t; tk_textCut .inp.t}
	.menu.edit.m add command -label "Copy" \
		-command {tk_textCopy .inp.t}
	.menu.edit.m add command -label "Paste" \
		-command {tk_textPaste .inp.t}

set FSz 110

menu .menu.view.m
	.menu.view.m add command -label "Larger" \
		-command {
			incr FSz 10
			set HelvBig "-Adobe-Helvetica-Medium-R-Normal--*-$FSz-*-*-*-*-*-*"
			.inp.t configure -font $HelvBig
		}
	.menu.view.m add command -label "Default text size" \
		-command {
			set FSz 110
			set HelvBig "-Adobe-Helvetica-Medium-R-Normal--*-$FSz-*-*-*-*-*-*"
			.inp.t configure -font $HelvBig
		}
	.menu.view.m add command -label "Smaller" \
		-command {
			incr FSz -10
			set HelvBig "-Adobe-Helvetica-Medium-R-Normal--*-$FSz-*-*-*-*-*-*"
			.inp.t configure -font $HelvBig
		}
	.menu.view.m add separator
	.menu.view.m add command -label "Clear Selections" \
		-command ".inp.t tag remove hilite 0.0 end;\
			  .inp.t tag remove Rev 0.0 end;\
			  .inp.t tag remove sel 0.0 end"

proc setlno {} {
	scan [.inp.t index insert] "%d.%d" lno cno
	.menu.ent delete 0 end
	.menu.ent insert end $lno
	.inp.t tag remove hilite $lno.0 $lno.end	;# or else cursor is invis
	update
}

proc add_log {{y ""}} {

	if {$y == "\n"} { return }
	.log.t insert end "\n$y"
	.log.t yview -pickplace end
}

proc cleanup {how} {
	global Unix
	if {$Unix == 0 && $how == 1} {
		add_log "removing temporary files, please wait.."; update
	}
	rmfile "pan.h pan.c pan.t pan.m pan.b pan.tmp pan.ltl"
	rmfile "pan.oin pan.pre pan.out pan.exe pan.otl"
	rmfile "pan_in pan_in.trail trail.out pan"
	rmfile "_tmp1_ _tmp2_ pan.o pan.obj pan.exe"
	if {$Unix == 0 && $how == 1} { add_log "done.." }
}


pack append . \
	.log  {bot frame w fillx} \
	.inp  {bot frame w expand fill} \
	.menu {top fillx}

# simulation parameters - initial settings
	set fvars 1
	set msc   1;	set svars 1
	set rvars 1
	set stop  0;	set tsc 0
	set seed	"1";	# random sumulation
	set jumpsteps	"0";	# guided simulation

	set s_typ 0
	# meaning s_type values:
	# 0 - Random Simulation (using seed)
	# 1 - Guided Simulation (using pan.trail)
	# 2 - Interactive Simulation

	set whichsim 0
	# meaning of whichsim values:
	# 0 - use pan_in.tra(il)
	# 1 - use user specified file

tkwait visibility .log
add_log "SPIN LOG:"
add_log " $version"
add_log "Xspin Version $xversion"
add_log "TclTk Version [info tclversion]/$tk_version\n"

	if {$Unix == 0} {
	if {[auto_execok $CC0] == "" \
	||  [auto_execok $CC0] == 0} {
		set m "Error: no C compiler found: $CC"
		add_log $m
		catch { tk_messageBox -icon info -message $m }
	}}

.inp.t configure -background $BG -foreground $FG

# process execution barchart

set Data(0) 0
set Name(0) "-"
set n 0
set bar_handle 0
set PlaceBar	""

proc stopbar {} {
	global Data Name n PlaceBar
	for {set i 0} {$i <= $n} {incr i} {
		set Data($i) 0
		set Name($i) ""
	}
	set n 0
	set PlaceBar [wm geometry .bar]
	set k [string first "\+" $PlaceBar]
	if {$k > 0} {
		set PlaceBar [string range $PlaceBar $k end]
	}
	catch { destroy .bar }
}

proc growbar {v} {
	global n Data
	set Data($n) $v
	incr n
	catch { fillbar }
}

proc shrinkbar {} {
	global n
	incr n -1
	set Data($n) 0
	catch { fillbar }
}

proc stepbar {v nm} {
	global n Data Name

	if {$v >= 0} {
		if { [info exists Data($v)] } {
			incr Data($v)
		} else {
			set Data($v) 1
		}
		if {$v >= $n} {
			set n [expr $v+1]
		}
		if { [string length $nm] > 4} {
			set Name($v) [string range $nm 0 4]
		} else {
			set Name($v) $nm
		}
		catch { fillbar }
	}
}

proc adjustbar {v w} {
	global Data

	set Data($v) $w
	catch { fillbar }
}

proc startbar {tl} {
	global n Data bar_handle Ptype PlaceBar

	catch { destroy .bar }
	toplevel .bar
	wm minsize .bar 200 200
	wm title .bar "$tl"

	set maxy [expr [winfo screenheight .] - 200]
	if {$PlaceBar == ""} {
		set PlaceBar "+[expr [winfo rootx .]+150]+$maxy"
	}
	wm geometry .bar $PlaceBar

	set bar_handle [canvas .bar.c -height 410 -width 410 -relief raised]
	frame  .bar.buts

	button .bar.buts.s1 -text "Save in:  panbar.ps" \
		-command ".bar.c postscript -file panbar.ps -colormode $Ptype"

	button .bar.buts.b -text " Close " -command "stopbar"
	pack .bar.buts.b .bar.buts.s1 -side right
	pack append .bar  .bar.c {top expand fill}  .bar.buts {bot frame e}
}

proc fillbar {} {
	global n Data Name

	.bar.c delete grid
	.bar.c delete data
	set sum 0
	for {set i 0} {$i < $n} {incr i} {
		if { [info exists Data($i)] } {
			incr sum $Data($i)
		} else {
			set Data($i) 0
			set Name($i) "-"
		}
	}
	for {set i 0} {$i < $n} {incr i} {
		.bar.c create line \
			$i 0 \
			$i 100 \
			-fill #222222 -tags grid
		.bar.c create text $i 105 \
			-text $i -tags grid
		.bar.c create text $i 110 \
			-text "$Name($i)" \
			-fill blue -tags grid

		if { [info exists Data($i)] } {
			set y [expr ($Data($i)*100)/$sum]
			.bar.c create line \
				$i 100  \
				$i [expr 100-$y] \
				-width 35 -fill red -tags data
			if {$y > 6} {
				set nrcol "yellow"
			} else {
				set nrcol "red"
			}
			.bar.c create text $i 95 \
				-text "$Data($i)" \
				-fill $nrcol -tags grid
		}
	}

	.bar.c create text [expr ($n)/2.0] -15 -text "Percentage of $sum System Steps" \
		-anchor c -justify center -tags grid
	.bar.c create text [expr ($n)/2.0] -8 -text "Executed Per Process ($n total)" \
		-anchor c -justify center -tags grid
	.bar.c scale all 0 0 55 3
	if {$n <= 5} {
		.bar.c move all 100 60
	} else {
		.bar.c move all 50 60
	}
}

proc barscales {} {
	global bar_handle

	catch {
		button .bar.buts.b4 -text "Larger" \
			-command "$bar_handle scale all 0 0 1.1 1.1"
		button .bar.buts.b5 -text "Smaller" \
			-command "$bar_handle scale all 0 0 0.9 0.9"
		pack append .bar.buts \
			.bar.buts.b4 {right padx 5} \
			.bar.buts.b5 {right padx 5}
	}
}

# Files and Generic Boxes

set file ""
set boxnr 0

proc rmfile {f} {
	global Unix CMD tk_major tk_minor

	set err ""
	catch { eval file delete -force $f } err
	if {$err == "" } { return }

	if {$Unix} {
		catch {exec rm -f $f}
	} else {
		set n [llength $f]
		for {set i 0} {$i < $n} {incr i} {
			set g [lindex $f $i]
			add_log "rm $g"
			if {$tk_major >= 4 && $tk_minor >= 2} {
				catch {exec $CMD /c del $g}
			} else {
				catch {exec $CMD >&@stdout /c del $g}
			}
	}	}
}

proc mvfile {f g} {
	global Unix CMD tk_major tk_minor

	set err ""
	catch { file rename -force $f $g } err
	if {$err == "" } { return }

	if {$Unix} {
		catch {exec mv $f $g}
	} else {
		if {$tk_major >= 4 && $tk_minor >= 2} {
			catch {exec $CMD /c move $f $g}
		} else {
			catch {exec $CMD >&@stdout /c move $f $g}
		}
	}
}

proc cpfile {f g} {
	global Unix CMD tk_major tk_minor

	set err ""
	catch { file copy -force $f $g } err
	if {$err == "" } { return }

	if {$Unix} {
		catch {exec cp $f $g}
	} else {
		if {$tk_major >= 4 && $tk_minor >= 2} {
		catch {exec $CMD /c copy $f $g}
		} else {
		catch {exec $CMD >&@stdout /c copy $f $g}
	}	}
}

proc cmpfile {f g} {
	global Unix

	set err ""
	if {$Unix} {
		catch {exec cmp $f $g} err
	} else {
		if {[file exists $f] == 0 \
		||  [file exists $g] == 0} {
			return "error"
		}
		set fd1 [open $f r]
		set fd2 [open $g r]
		while {1} {
			set n1 [gets $fd1 line1]
			set n2 [gets $fd2 line2]
			if {$n1 != $n2 \
			||  [string compare $line1 $line2] != 0} {
				set err "files differ"
				break
			}
			if {$n1 < 0} { break }
		}
		close $fd1
		close $fd2
	}
	return $err
}

proc file_ok {f} {
	if {[file exists $f]} {
		if {![file isfile $f] || ![file writable $f]} {
			set m "error: file $f is not writable"
			add_log $m
			catch { tk_messageBox -icon info -message $m }
			return 0
	}	}
	return 1
}

proc mkpan_in {} {
	global HasNever
	set fd [open pan_in w]
	puts $fd [.inp.t get 0.0 end] nonewline

	if {$HasNever != ""} {
		if [catch {set fdn [open $HasNever r]} errmsg] {
			add_log $errmsg
			catch { tk_messageBox -icon info -message $errmsg }
		} else {
			while {[gets $fdn line] > -1} {
				puts $fd $line
			}
			catch "close $fdn"
	}	}
	catch "flush $fd"
	catch "close $fd"
}

proc no_ltlchange {} {

	if {![file exists pan.ltl]} {
		return 1
	}
	if {![file exists pan.otl]} {
		cpfile pan.ltl pan.otl
		return 0		; first time
	}
	set err [cmpfile pan.ltl pan.otl]
	if {[string length $err] > 0} {
		cpfile pan.ltl pan.otl
		return 0		;# different
	}
	return 1			;# unchanged
}

proc no_change {} {
	global nv_typ

	mkpan_in	;# keep this up to date
	if {![file exists pan.oin]} {
		cpfile pan_in pan.oin
		return 0		; first time
	}
	set err [cmpfile pan_in pan.oin]
	if {[string length $err] > 0} {
		cpfile pan_in pan.oin
		return 0		;# different
	}
	if {$nv_typ == 0} {
		return 1
	}
	return [no_ltlchange]		;# unchanged
}

proc mk_exec {} {
	global Unix CC SPIN notignored

	set nochange [no_change]
	if {$nochange == 1 && [file exists "pan"]} {
		add_log "<no recompilation needed>"
		return 1
	}

	add_log "<compiling executable>"
	catch {
	warner "Compiling" "Please wait until compilation of the \
executable produced by spin completes." 300
	}
	add_log "$SPIN -a pan_in"

	catch {exec $SPIN -a pan_in >&pan.tmp}
	set errmsg [msg_file pan.tmp 1]

	if {[string length $errmsg]>0} {
		add_log "$errmsg"
		catch { tk_messageBox -icon info -message $errmsg }
		add_log "<stopped compilation attempt>"
		catch { destroy .warn }
		return 0
	}

	add_log "$CC -o pan -D_POSIX_SOURCE pan.c"; update
	if {$Unix} {
		catch { eval exec $CC -o pan -D_POSIX_SOURCE pan.c >pan.tmp 2>pan.err} errmsg
	} else {
		catch { eval exec $CC -o pan -D_POSIX_SOURCE pan.c >pan.tmp 2>pan.err}
	}
	set errmsg [msg_file pan.tmp 0]
	set errmsg "$errmsg \n [msg_file pan.err 0]"

		if {[string length $errmsg]>0 && $notignored} {
			add_log "$errmsg"
			catch { tk_messageBox -icon info -message $errmsg }
			catch { destroy .warn }
			return 0
		}
	add_log "<compilation complete>"
	catch {destroy .warn}
	return 1
}

set PlaceWarn	"+20+20"

proc warner {banner msg w} {
	global PlaceWarn

	catch {destroy .warn}
	toplevel .warn

	wm title .warn "$banner"
	wm iconname .warn "Info"
	set k [string first "\+" $PlaceWarn]
	if {$k > 0} {
		set PlaceWarn [string range $PlaceWarn $k end]
	}
	wm geometry .warn $PlaceWarn

	message .warn.t -width $w -text $msg
	button .warn.ok -text "Ok" \
		-command "set PlaceWarn [wm geometry .warn]; destroy .warn"

	pack append .warn .warn.t {top expand fill}
	pack append .warn .warn.ok {bottom}

	update
}

proc dosave {} {
	global Fname xversion

	if {[file_ok $Fname]==0} return
	set fd [open $Fname w]
	add_log "<saved spec in $Fname>"
	puts $fd "[.inp.t get 0.0 end]" nonewline
	catch "flush $fd"
	catch "close $fd"
	wm title . "SPIN CONTROL $xversion -- File: $Fname"
}

proc save_spec {{curr 1}} {
#-
#- Save the input area into a file.
#-
#- If 'curr' is true then we save to the current file. Otherwise, a file
#- selection dialog is presented. If a file is selected (note that the
#- dialog can be canceled) then we try to write to it.
#-

  global Fname

  if $curr {
    switch -- $Fname "" {
      add_log "no file to save to, try \"Save as ...\""
      return
    }
    writeoutfile .inp.t $Fname
  } else {
    # try to use the predefined file selection dialog
    switch [info commands tk_getSaveFile] "" {
      # some old version of Tk so use our own file selection dialog
      set fileselect "FileSelect save"
    } default {
      set fileselect "tk_getSaveFile"
    }
  
    # get the file (return if the file selection dialog canceled)
    switch -- [set file [eval $fileselect]] "" return
  
    # write the file and update Fname if the file written successfully
    if [writeoutfile .inp.t $file] {
      set Fname $file
    }
  }
}

proc consider_it {} {
	global file Fname xversion

	if {[file isdirectory $file]} then {
		cd $file
		fillerup ""
		add_log "cd $file"
	} else {
		if {![file isfile $file]} {
			set file ""
		} else {
			readinfile .inp.t $file

			rmfile pan_in.trail
			cpfile $file.trail pan_in.trail

			set dir [pwd]
			set Fname $file
			wm title . "SPIN CONTROL $xversion -- File: $Fname"
			destroy .b
	}	}
}

#----------------------------------------------------------------------
# Improvements - by Leszek Holenderski <lhol@win.tue.nl>
# GUI configuration and File Selection dialogs
#----------------------------------------------------------------------

# predefined priorities for options stored in the option data base are
#	widgetDefault	20
#	startupFile	40
#	userDefault	60
#	interactive	80

# most of frames are used for layout purposes so they should be invisible
option add *Frame.borderWidth 0 interactive

proc try_with {xspinrc} {

  if ![file exists $xspinrc] return

  if ![file isfile $xspinrc] {
    puts "xspin warning: the resource file \"$xspinrc\" exists but is not\
          a normal file"
    return
  }
  if ![file readable $xspinrc] {
    puts "xspin warning: the resource file \"$xspinrc\" exists but is not\
          readable"
    return
  }
  if [catch {option readfile $xspinrc userDefault} result] {
    puts "xspin warning: some problems when trying to load the resource\
          file \"$xspinrc\"\n$result"
    return
  }
}

if [info exists env(HOME)] {
  if $Unix {
    try_with [file join $env(HOME) .xspinrc]
  } else {
    try_with [file join $env(HOME) xspinrc]
  }
}

proc FileSelect {mode {title ""}} {
  switch -- $mode open - save {} default { set mode open }

  switch $mode {
    open {
      set title Open
      set okButtonText Open
    }
    save {
      set title Save
      set okButtonText Save
    }
  }

  set w .fileselect
  upvar #0 $w this

  if [winfo exists $w] {
    wm title $w $title
    $this(okButton) config -text $okButtonText
    catch {wm geom $w $this(geom)}
    wm deiconify $w
  } else {
    toplevel $w -class Fileselect
    wm title $w $title
    # the minimal size is given in characters and lines (setgrid is on)
    wm minsize $w 14 7

    # layout frames
    pack [set f [frame $w.f]] -padx 5 -pady 5 -fill both -expand yes
    pack [set buttons [frame $f.b]] -side bottom -fill x
    pack [set name    [frame $f.n]] -side bottom -fill x -pady 5
    pack [set path    [frame $f.p]] -side top -fill x
    pack [set files   [frame $f.f]] -side top -fill both -expand yes
  
    # create ok/cancel buttons
    set okButton [button $buttons.ok -text $okButtonText \
			-command "FileSelect.Close $w 1"]
    pack $okButton -side right

    set cancelButton [button $buttons.cancel -text Cancel \
			-command "FileSelect.Close $w 0"]
    pack $cancelButton -side left

    MakeSameWidth "$okButton $cancelButton"
  
    # create path button
    set pathButton $path.path
    global $w|currDir
    set pathMenu [tk_optionMenu $pathButton $w|currDir ""]
    pack $pathButton -side top
  
    # create the list of files
    global scrollbarSide

    set fileList $files.l
    set scrollbar $files.s
    pack [scrollbar $files.s -command "$fileList yview"] \
	 -side $scrollbarSide -fill y
    pack [listbox $fileList -yscrollcommand "$files.s set" -selectmode single -setgrid on] \
	 -side $scrollbarSide -expand yes -fill both
  
    bind $fileList <ButtonPress-1>        "FileSelect.Selected $w %x %y"
    bind $fileList <Double-ButtonPress-1> "FileSelect.Chosen   $w %x %y"

    set fileEntry $name.e
    pack [label $name.l -text File:] -side left
    pack [entry $fileEntry] -side right -expand yes -fill x

    set this(okButton)   $okButton
    set this(pathButton) $pathButton
    set this(pathMenu)   $pathMenu
    set this(fileList)   $fileList
    set this(fileEntry)  $fileEntry

    foreach widget "$okButton $cancelButton $pathButton $fileList $scrollbar" {
      $widget config -highlightthickness 0
    }

    wm protocol $w WM_DELETE_WINDOW [$cancelButton cget -command]
  }

  # fill in the list of files
  if ![info exists this(path)] { set this(path) [pwd] }
  FileSelect.cd $w $this(path)

  # make the dialog modal (set a grab and claim the focus)

  set oldFocus [focus]
  set oldGrab [grab current $w]
  if {$oldGrab != ""} { set grabStatus [grab status $oldGrab] }
  grab $w
  focus $this(fileEntry)

  # make the contents of file entry selected (for easy deletion)
  $this(fileEntry) select from 0
  $this(fileEntry) select to end

  # Wait for the user to respond, then restore the focus and return the
  # contents of file entry.
  # Restore the focus before deleting the window, since otherwise the
  # window manager may take the focus away so we can't redirect it.
  # Finally, restore any grab that was in effect.

  global $w|response
  tkwait variable $w|response
  catch {focus $oldFocus}
  grab release $w
  set this(geom) [wm geom $w]
  wm withdraw $w
  if {$oldGrab != ""} {
      if {$grabStatus == "global"} {
	  grab -global $oldGrab
      } else {
	  grab $oldGrab
      }
  }
  return [set $w|response]
}

proc CompareNoCase {s1 s2} {
  return [string compare [string tolower $s1] [string tolower $s2]]
}

proc FileSelect.LoadFiles {w} {
    upvar #0 $w this

    # split all names in the current directory into dirs and files
    set dirs ""
    set files ""
    set filter ""
    if [info exists this(filter)] { set filter $this(filter) }
    switch -- $filter "" { set filter * }
    foreach f [lsort -command CompareNoCase [glob -nocomplain .* *]] {
	if [file isdir $f] {
	  # exclude the '.' and '..' directory
	  switch -- $f . - .. continue
	  lappend dirs $f
	}
	if [file isfile $f] {
	  # filter files
	  switch -glob -- $f $filter { lappend files $f }
	}
    }

    # Fill in the file list
    $this(fileList) delete 0 end
    foreach d $dirs {
	# append directory mark to the name (tricky)
	set d [string trimright [file join $d a] a]
	$this(fileList) insert end $d
    }
    foreach f $files { $this(fileList) insert end $f }
}

proc FileSelect.LoadPath {w} {
    upvar #0 $w this

    # convert path to list
    set dirs [file split $this(path)]

    # compute prefix paths
    set path ""
    set paths ""
    foreach d $dirs {
	set path [file join $path $d]
	lappend paths $path
    }

    # reverse dirs and paths
    set rev_dirs ""
    foreach d $dirs { set rev_dirs [concat [list $d] $rev_dirs] }
    set rev_paths ""
    foreach p $paths { set rev_paths [concat [list $p] $rev_paths] }

    # update the path menubutton
    global $w|currDir
    set $w|currDir [lindex $rev_dirs 0]

    # fill in the path menu
    $this(pathMenu) delete 0 end
    foreach d [lrange $rev_dirs 1 end] p [lrange $rev_paths 1 end] {
	$this(pathMenu) add command -label $d -command "FileSelect.cd $w $p"
    }
}

proc FileSelect.Selected {w x y} {
    upvar #0 $w this

    # determine the selected list element
    set elem [$this(fileList) get [$this(fileList) index @$x,$y]]
    switch -- $elem "" return

    # directories cannot be selected (they can only be chosen)
    if [file isdir $elem] return

    $this(fileEntry) delete 0 end
    $this(fileEntry) insert end $elem
}

proc FileSelect.Chosen {w x y} {
    upvar #0 $w this

    # determine the selected list element
    set elem [$this(fileList) get [$this(fileList) index @$x,$y]]
    switch -- $elem "" return

    # if directory then cd, otherwise close the dialog
    if [file isdir $elem] { FileSelect.cd $w $elem } { FileSelect.Close $w 1 }
}

proc FileSelect.Close {w {ok 1}} {
  # trigger the end of dialog
  upvar #0 $w this $w|response response
  if $ok {
    set response [file join $this(path) [$this(fileEntry) get]]
  } else {
    set response ""
  }
}

proc FileSelect.cd {w dir} {
    upvar #0 $w this

    if [catch {cd $dir} errmsg] {
	puts "xspin warning: $errmsg"
	return
    }

    set this(path) [pwd]
    FileSelect.LoadFiles $w
    FileSelect.LoadPath $w
}

proc open_spec {{curr 1}} {
  global Fname

  if $curr {
    switch -- $Fname "" {
      add_log "no file to reopen, try \"Open ...\""
      return
    }
    readinfile .inp.t $Fname
  } else {
    # try to use the predefined file selection dialog
    switch [info commands tk_getOpenFile] "" {
      # some old version of Tk so use our own file selection dialog
      set fileselect "FileSelect open"
    } default {
      set fileselect "tk_getOpenFile"
    }
    set init_dir [pwd]
    # get the file (return if the file selection dialog canceled)
    switch -- [set file [eval $fileselect -initialdir { $init_dir } ]] "" return
  
    # load the file and update some items if the file loaded successfully
    if [readinfile .inp.t $file] {
      rmfile pan_in.trail
      cpfile $file.trail pan_in.trail
      set Fname $file
      set_path $Fname
    }
  }
}


proc set_path {Fname} {
	#cd to directory in file
	set fullpath [split $Fname /]
	set nlen [llength $fullpath]
	set fullpath [lrange $fullpath 0 [expr $nlen - 2]] 	;# get rid of filename
	set wd [join $fullpath /] 				;#put path back together
 	catch {cd $wd}
}

set defname ""

proc loaddefault_tl {} {
	global Fname defname

	if {$defname ==""} {
		set file2 "$Fname.ltl"
	} else {
		set file2 $defname
	}
	catch {
		.tl.main.e1 delete 0 end
		.tl.macros.t delete 0.0 end
		.tl.notes.t delete 0.0 end
		.tl.never.t delete 0.0 end
		.tl.results.t delete 0.0 end
	}
	if {![file exists $file2]} {
		.tl.notes.t insert end "Use Load to open a file or a template."
		return
	}
	catch {
		.tl.notes.title configure -text "Notes \[file $file2]:"
	}
	readinfile .tl.never.t $file2
	catch { extract_defs }
}

set suffix "ltl"

proc browse_tl {} {
	global defname suffix

	set suffix "ltl"

	catch {destroy .b}
	toplevel .b
	wm iconname .b "Load"

	frame .b.top
	frame .b.bot
	scrollbar .b.top.scroll -command ".b.top.list yview"
	listbox .b.top.list -yscroll ".b.top.scroll set" -relief raised 

	button .b.zap -text "Cancel" -command "destroy .b"
	button .b.all -text "Show All Files" \
		-command {
			set suffix ""
			fillerup ""
			destroy .b.all
		}
	message .b.bot.msg -text "Dir: "
	entry .b.bot.entry -textvariable dir -relief sunken -width 20
	pack append .b.top \
		.b.top.scroll {right filly} \
		.b.top.list {left expand fill}
	pack append .b.bot \
		.b.bot.msg {left} \
		.b.bot.entry {left}
	pack append .b \
		.b.top {top fillx} \
		.b.all {left} \
		.b.zap {left} \
		.b.bot {left}
	
	bind .b.bot.entry <Return> {
		set nd [.b.bot.entry get]
		if {[file isdirectory $nd]} {
			cd $nd
			fillerup $suffix
			add_log "cd $nd"
		}
	}

	fillerup  $suffix
	bind .b.top.list <Double-Button-1> {
		set file2 [selection get]
		if {[string first "---" $file2] >= 0} {
			# ignore
		} elseif {[string first "Invariance" $file2] >= 0} {
			catch {
			.tl.main.e1 delete 0 end
			.tl.macros.t delete 0.0 end
			.tl.notes.t delete 0.0 end
			.tl.never.t delete 0.0 end
			.tl.results.t delete 0.0 end

			.tl.main.e1 insert end "\[\] (p)"
			.tl.notes.t insert end "'p' is invariantly true throughout
an execution"
			.tl.notes.title configure \
				-text "Notes \[template $file2]:"
			do_ltl
			destroy .b
			}
		} elseif {[string first "Response" $file2] >= 0} {
			catch {
			.tl.main.e1 delete 0 end
			.tl.macros.t delete 0.0 end
			.tl.notes.t delete 0.0 end
			.tl.never.t delete 0.0 end
			.tl.results.t delete 0.0 end

			.tl.main.e1 insert end "\[\] ((p) -> (<> (q)))"
			.tl.notes.t insert end "if 'p' is true in at least one state,
then sometime thereafter 'q' must also
become true at least once."
			.tl.notes.title configure \
				-text "Notes \[template $file2]:"
			do_ltl
			destroy .b
			}
		} elseif {[string first "Precedence" $file2] >= 0} {
			catch {
			.tl.main.e1 delete 0 end
			.tl.macros.t delete 0.0 end
			.tl.notes.t delete 0.0 end
			.tl.never.t delete 0.0 end
			.tl.results.t delete 0.0 end

			.tl.main.e1 insert end "\[\] ((p) -> ((q) U (r)))"
			.tl.notes.t insert end "'p' is a trigger, or 'enabling' condition that
determines when this requirement becomes applicable
'r' is the fullfillment of the requirement, and
'q' is a condition that must remain true in the interim."
			.tl.notes.title configure \
				-text "Notes \[template $file2]:"
			do_ltl
			destroy .b
			}
		} elseif {[string first "Objective" $file2] >= 0} {
			catch {
			.tl.main.e1 delete 0 end
			.tl.macros.t delete 0.0 end
			.tl.notes.t delete 0.0 end
			.tl.never.t delete 0.0 end
			.tl.results.t delete 0.0 end

			.tl.main.e1 insert end "\[\] ((p) -> <>((q) || (r)))"
			.tl.notes.t insert end "'p' is a trigger, or 'enabling' condition that
determines when this requirement becomes applicable
'q' is the fullfillment of the requirement, and
'r' is a discharging condition that terminates the
applicability of the requirement."

			.tl.notes.title configure \
				-text "Notes \[template $file2]:"
			do_ltl
			destroy .b
			}
		} elseif {[file isdirectory $file2]} then {
			cd $file2
			fillerup $suffix
			add_log "cd $file2"
		} else {
			if {![file isfile $file2]} {
				set file2 ""
			} else {
				catch {
				.tl.main.e1 delete 0 end
				.tl.macros.t delete 0.0 end
				.tl.notes.t delete 0.0 end
				.tl.never.t delete 0.0 end
				.tl.results.t delete 0.0 end
				.tl.notes.title configure \
					-text "Notes \[file $file2]:"
				}
				readinfile .tl.never.t $file2
				set defname $file2
				catch { extract_defs }
				set dir [pwd]
				destroy .b
			}
		}
	}
}

proc reopen {} {
	global Fname

	catch {readinfile .inp.t $Fname} ermsg
	if {[string length $ermsg]<=1} { return }
	add_log $ermsg
	catch { tk_messageBox -icon info -message $ermsg }
}

proc writeoutfile {from to} {

  if ![file_ok $to] { return 0 }

  if [catch {set fd [open $to w]} errmsg] {
    add_log $errmsg
    catch { tk_messageBox -icon info -message $ermsg }
    return 0
  }

  add_log "<saved spec in $to>"
  puts $fd [string trimright [$from get 0.0 end] "\n"]
# puts -nonewline $fd [$from get 0.0 end]
  close $fd
  return 1
}

proc readinfile {into from} {

  if [catch {set fd [open $from r]} errmsg] {
    add_log $errmsg
    catch { tk_messageBox -icon info -message $ermsg }
    return 0
  }
	
  $into delete 0.0 end
  while {[gets $fd line] > -1} { $into insert end $line\n }
  catch { close $fd }
  add_log "<open $from>"

  global LastGenerate
  set LastGenerate ""	;# used in Validation.tcl
  return 1
}

proc fillerup {suffix} {
	wm title .b [pwd]
	.b.top.list delete 0 end

	set dotdot 0
	set l {}
	catch {	if {$suffix != ""} {
			set l [lsort [glob *.$suffix]]
		} else {
			set l [lsort [glob *]]
	}	}
	foreach i $l {
		.b.top.list insert end $i
		if {$i == ".."} { set dotdot 1 }
	}
	if {$dotdot == 0} {
		.b.top.list insert 0 ".."
	}
	if {$suffix != ""} {
		.b.top.list insert 0 "------files:--------"
		.b.top.list insert 0 "Objective(p,q,r)"
		.b.top.list insert 0 "Precedence(p,q,r)"
		.b.top.list insert 0 "Response(p,q)"
		.b.top.list insert 0 "Invariance(p)"
		.b.top.list insert 0 "-----templates:-----"
	}
}

proc gotoline {} {
	global BG FG

	catch { destroy .ln }
	toplevel .ln
	wm title .ln "Goto Line"
	wm iconname .ln "Goto"

	label .ln.lab -text "Enter line number:"
	entry .ln.ent -width 20 -relief sunken -textvariable lno
	pack append .ln \
		.ln.lab {left padx 1m} \
		.ln.ent {right expand}
	bind .ln.ent <Return> {
		.inp.t tag remove hilite 0.0 end
		.inp.t tag add hilite $lno.0 $lno.1000
		.inp.t tag configure hilite \
			-background $FG -foreground $BG
		.inp.t yview -pickplace [expr $lno-1]
	}
	focus .ln.ent
}

proc savebox {b} {
	set fname [.c$b.f.e1 get]
	if {[file_ok $fname]==0} return
	set fd [open $fname w]
	add_log "<saved output in $fname>"
	puts $fd "[.c$b.z.t get 0.0 end]" nonewline
	catch "flush $fd"
	catch "close $fd"
}

proc doplace {a b} {
	global PlaceBox
	set PlaceBox($a) [wm geometry .c$b]
	set k [string first "\+" $PlaceBox($a)]
	if {$k > 0} {
		set PlaceBox($a) [string range $PlaceBox($a) $k end]
	}
}

proc mkbox {n m p {wd 60} {ht 10} {xp 200} {yp 200}} {
	global boxnr FG BG PlaceBox HelvBig
	global ind old_ss old_insert new_insert;# for search capability

	incr boxnr

	toplevel .c$boxnr
	wm title .c$boxnr $n
	wm iconname .c$boxnr $m

	if {[info exists PlaceBox($n)] == 0} {
		set PlaceBox($n) "+$xp+$yp"
	} 
	wm geometry .c$boxnr $PlaceBox($n)

	#initialize search parameters
	set ind 1.0
	set old_ss ""
	set old_insert ""
	set new_insert ""
	frame .c$boxnr.d ;# search bar
		label .c$boxnr.d.l -text "Search for: "
		entry .c$boxnr.d.e -width 15
		bind .c$boxnr.d.e <KeyPress-Return> "search_sim .c$boxnr.z.t .c$boxnr.d.e .c$boxnr" 
		button .c$boxnr.d.b -text "Find" -command "search_sim .c$boxnr.z.t .c$boxnr.d.e .c$boxnr"

	pack .c$boxnr.d -side top -fill x
	pack .c$boxnr.d.b -side right
	pack .c$boxnr.d.e -side right
	pack .c$boxnr.d.l -side right

	frame .c$boxnr.z
	
	text .c$boxnr.z.t -relief raised -bd 2 -font $HelvBig \
		-background $BG -foreground $FG \
		-yscrollcommand ".c$boxnr.z.s set" \
		-setgrid 1 -width $wd -height $ht -wrap word
	bind .c$boxnr.z.t <ButtonRelease-1> "+update idletasks; update_insert .c$boxnr.z.t"
	scrollbar .c$boxnr.z.s \
		-command ".c$boxnr.z.t yview"
	pack append .c$boxnr.z \
		.c$boxnr.z.s {left filly} \
		.c$boxnr.z.t {left expand fill}

	button .c$boxnr.b -text "Close" \
	-command "doplace {$n} {$boxnr}; destroy .c$boxnr"
	button .c$boxnr.c -text "Clear" \
		-command ".c$boxnr.z.t delete 0.0 end"
	pack append .c$boxnr \
		.c$boxnr.z {top expand fill} \
		.c$boxnr.b {right padx 5} \
		.c$boxnr.c {right padx 5}

	if {[string length $p]>0} {
		frame  .c$boxnr.f -relief sunken
		button .c$boxnr.f.e0 -text "Save in: " \
			-command "savebox $boxnr"
		entry  .c$boxnr.f.e1 -relief flat -width 10
		.c$boxnr.f.e1 insert end $p
		pack append .c$boxnr.f \
			.c$boxnr.f.e0 {left padx 5} \
			.c$boxnr.f.e1 {left}
		pack append .c$boxnr \
			.c$boxnr.f {right padx 5}
	}

	tkwait visibility .c$boxnr
	return $boxnr
}
proc update_insert {t} {
	global new_insert
	update idletasks
	set new_insert [$t index insert]
}

proc search_sim {t e b} {
	global ind old_ss old_insert new_insert

	set ss [$e get]

	if {$ss == ""} {
		return
		}

	#if user has selected use that lin.char as 'ind'. otherwise use end of last word found
	#set new_insert [$t index insert]
	if {$new_insert != $old_insert} {
		set ind $new_insert ;# this is where we will start searching
		set old_insert $new_insert ;# update select location
	}
	set cur_ind $ind
	set ind [$t search $ss $ind]

	set old_ss $ss
	if {$ind != ""} {
		$t yview -pickplace $ind
		$t tag configure hilite -foreground black -background white
		$t tag delete hilite 
		set split_ind [split $ind "."]
		set char [lindex $split_ind 1]	
		set char [incr char [string length $ss]]
		set indstart $ind
		set indend ""
		append indend [lindex $split_ind 0] "." $char
		$t tag add hilite $indstart $indend
		$t tag configure hilite -foreground white -background black
		set ind $indend
	} else {
		# set ind 1.0
		catch { tk_messageBox -icon info -message "no match for $ss" }
		set ind $cur_ind ;# restore ind to last good value
		raise $b
	}	

}

# Tcl/Tk book, page 219
proc forAllMatches {w pattern} {
	global BG FG lno

	scan [$w index end] %d numLines
	for {set i 1} {$i < $numLines} { incr i} {
		$w mark set last $i.0
		if {[regexp -indices $pattern \
			[$w get last "last lineend"] indices]} {
				$w mark set first \
					"last + [lindex $indices 0] chars"
				$w mark set last "last + 1 chars \
					+ [lindex $indices 1] chars"
			.inp.t tag add hilite $i.0 $i.end
			.inp.t tag configure hilite \
				-background $FG -foreground $BG
#			.inp.t yview -pickplace [expr $i-1]
	}	}

#	move to the next line that matches

	for {set i [expr $lno+1]} {$i < $numLines} { incr i} {
		$w mark set last $i.0
		if {[regexp -indices $pattern \
			[$w get last "last lineend"] indices]} {
				$w mark set first \
					"last + [lindex $indices 0] chars"
				$w mark set last "last + 1 chars \
					+ [lindex $indices 1] chars"
			.inp.t yview -pickplace [expr $i-5]
			set lno $i
			return
	}	}
	for {set i 1} {$i <= $lno} { incr i} {
		$w mark set last $i.0
		if {[regexp -indices $pattern \
			[$w get last "last lineend"] indices]} {
				$w mark set first \
					"last + [lindex $indices 0] chars"
				$w mark set last "last + 1 chars \
					+ [lindex $indices 1] chars"
			.inp.t yview -pickplace [expr $i-5]
			set lno $i
			return
	}	}
	catch {
		tk_messageBox -icon info -message "No Match of \"$pattern\""
	}
}

set noprep 0

proc hasWord {pattern} {
	global SPIN noprep
	set err ""
	if {![file exists pan.pre] && $noprep == 0} {
		add_log "$SPIN -Z pan_in ;# preprocess input"
		catch {exec $SPIN -Z pan_in >&pan.tmp} err
		# leaves output in pan.pre
		add_log "<done preprocess>"
	}

	if {[string length $err] == 0 && $noprep == 0} {
		set fd [open pan.pre r]
		while {[gets $fd line] > -1} {
		  if {[regexp -indices $pattern $line indices]} {
			catch "close $fd"
			return 1
		} }
		catch "close $fd"
		return 0
	}

	# else, there were errors, just ignore the include files:
	set noprep 1
	add_log "$err"
	scan [.inp.t index end] %d numLines
	for {set i 1} {$i < $numLines} { incr i} {
		.inp.t mark set last $i.0
		if {[regexp -indices $pattern \
			[.inp.t get last "last lineend"] indices]} {
				return 1
		}
	}
	return 0
}

# FSM view option

set nodeX(0) 0
set nodeY(0) 0
set Label(0) 0
set Transit(0) {}
set TLabel(0) 0
set Lab2Node(0) 0
set Dist(0) 0
set State(0) 0
set Edges(0) {}
set New 0
set MaxDist 0
set Maxx 0
set Maxy 0
set Minx 50
set Miny 50
set reached_end 0
set Scale 1

set cnr	0
set x 0
set y 0

proc fsmview {} {
	global Unix

	add_log "<fsm view option>"

	if {[mk_exec] != 1} { return }

	catch {destroy .z}
	toplevel .z

	wm title .z "Double-Click Proc"

	listbox .z.list -setgrid 1
	button .z.b -text "Cancel" -command "destroy .z"

	pack append .z \
		.z.list {top expand fill} \
		.z.b {right padx 5}

	if {$Unix} {
		add_log "./pan -d	# find proc names"; update
		set fd [open "|./pan -d" w+]
	} else {
		add_log "pan -d	# find proc names"; update
		catch { eval exec pan -d >&pan.tmp } err
		if {$err != ""} {
			add_log "error: $err"
		}
		set fd [open pan.tmp r]
	}
	while {[gets $fd line] > -1} {
		if {[string first "proctype" $line] >= 0 } {
			.z.list insert end \
			[string trim [string range $line 9 end]]
	}	}
	catch { close $fd }

	bind .z.list <Double-Button-1> {
		set pfind [selection get]
		catch { destroy .z }
		findfsm $pfind
	}
	focus .z.list
}

proc findfsm {pfind} {
	global Unix New Dist State Edges Label
	global Transit MaxDist reached_end TLabel DOT

	if {[mk_exec] != 1} { return }

	set src  0; set trn 0; set trg 0
	set Want 0; set MaxDist 0; set startstate ""

	catch { foreach el [array names State] { unset State($el) } }
	catch { foreach el [array names Edges] { unset Edges($el) } }
	catch { foreach el [array names Dist]  { unset Dist($el) } }

	if {$Unix} {
		add_log "./pan -d	# compute fsm"; update
		set fd [open "|./pan -d" w+]
	} else {
		add_log "pan -d	# compute fsm"; update
		catch { eval exec pan -d >&pan.tmp }
		set fd [open pan.tmp r]
	}
	while {[gets $fd line] > -1} {
		set k [string first "proctype" $line]
		if { $k >= 0 } {
			if { $Want == 1 } {
				break
			}
			incr k 9
			set pname [string range $line $k end]

			if { [string first $pfind $line] >= 0 \
			&&   [string length $pfind] == [string length $pname]} {
				set Want 1
				set reached_end 0
				set nsrc "$pname:0"
				set Dist($nsrc) 0
				set Label($nsrc) "end"
				set Edges($nsrc) {}
			}
		} elseif { $Want == 1 \
			&& [string first "state" $line] >= 0} {
			scan $line "	state %d -(tr %d)-> state %d" \
				src trn trg
			if {$trg == 0} { set reached_end 1 }

			set nsrc "$pname:$src"
			set ntrg "$pname:$trg"

			if {$startstate == ""} { set startstate $nsrc }

			set k [string first "line" $line]
			if { $k > 0 } {
				set m [string first "=>" $line]
				incr m -1
				set lbl [string range $line $k $m]
				incr m 3
				set action [string range $line $m end]
			} else {
				set lbl "line 0"
				set action "line 0"
			}
			set Label($nsrc) $lbl
			if { [info exists Dist($nsrc)] == 0 } {
				set Dist($nsrc) 0
				set Edges($nsrc) {}
			}
			if { [info exists Dist($ntrg)] == 0 } {
				set Dist($ntrg) [expr $Dist($nsrc) + 1]
				set Edges($ntrg) {}
				if {$Dist($ntrg) > $MaxDist } {
					set MaxDist $Dist($ntrg)
				}
			} else {
				if { [expr $Dist($nsrc) + 1] < $Dist($ntrg) } {
					set Dist($ntrg) [expr $Dist($nsrc) + 1]
					if {$Dist($ntrg) > $MaxDist } {
						set MaxDist $Dist($ntrg)
					}
			}	}
if {0 \
&&  [auto_execok $DOT] != 0 \
&&  [auto_execok $DOT] != ""} {
	set z1 [string first "\[" $action]
	set z2 [string last  "\]" $action]
	if {$z1 > 0 && $z2 > $z1} {
		incr z1 -1; incr z2
		set a1 [string range $action 0 $z1]
		set a2 [string range $action $z2 end]
		set action "$a1$a2"
	}
			set kkk "$nsrc;$trg:$action"
			lappend Edges($nsrc) "$kkk"
			lappend Edges($kkk) $ntrg
			lappend Transit($nsrc) "$lbl"
			lappend Transit($kkk) ""
			set Dist($kkk) $Dist($ntrg)
			set Label($kkk) "T3"
} else {
			lappend Edges($nsrc) $ntrg
			lappend Transit($nsrc) $action
}
		}
	}
	if { $Want == 1 } {
		dograph $pfind $startstate
	} else {
		add_log "sorry, $pfind not found..."
		catch {
		tk_messageBox -icon info -message "$pfind not found..."
		}
	}
	catch "close $fd"
	add_log "<done>"
	update
}

proc plunknode {el prefix} {
	global State Label TLabel
	global x y

	set pn [string range $el $prefix end]
	set State($el) [mkNode "$Label($el)" $pn $x $y]

	if { $x > 250 } {
		set x [expr $x - 250]
		set x [expr 250 - $x]
	} else {
		set x [expr 250 - $x]
		incr x 75
		set x [expr 250 + $x]
	}
}

proc dograph {n s} {
	global Dist Edges Label Transit MaxDist State ELabel
	global cnr lcnr reached_end x y Unix DOT
	set count -1

	set lcnr [mkcanvas "FSM $n" $n 300 300 0]
	set prefix [string length $n]
	incr prefix
	set y 0

	while {$count < $MaxDist} {
		incr count
		incr y 50
		set x 250
		foreach el [array names Dist] {
			if { [ string first $n $el ] >= 0 \
			&&   $Dist($el) == $count \
			&&   $el != "$n:0" } {
				plunknode $el $prefix
		}	}
	}
	if {$reached_end == 1} {
		# force end state at the bottom
		incr y 50
		set x 250
		plunknode "$n:0" $prefix
	}

	foreach el [array names Edges] {
		if { [ string first $n $el ] >= 0 } {
			for {set i 0} { [lindex $Edges($el) $i] != "" } {incr i} {
				set ntrg [lindex $Edges($el) $i]
				set lbl  [lindex $Transit($el) $i]
				mkEdge $lbl $State($el) $State($ntrg)
				set ELabel($el,$ntrg) "$lbl"
			}
	}	}
	addscales $lcnr

	.f$cnr.c itemconfigure $State($s) -outline red; update

	if {[auto_execok $DOT] != 0 \
	&&  [auto_execok $DOT] != ""} {
		dodot $n
#		button .f$lcnr.b66 -text "Redraw with Dot"  -command "dodot $n"
#		pack append .f$lcnr .f$lcnr.b66 {right padx 5}
	}
	update
}

proc mkNode {n t x y} {
	# tcl book p. 213
	global cnr NodeWidth NodeHeight HelvBig
	global nodeX nodeY New TLabel Lab2Node

	if {[string first ";" $t] > 0} {
		set New [.f$cnr.c create rectangle [expr $x-1] [expr $y-1] \
			[expr $x+1] [expr $y+1] \
			-outline white \
			-fill white \
			-tags node]
		set z [string first ":" $t]; incr z
		set t [string range $t $z end]
		set Lab [.f$cnr.c create text $x $y -font $HelvBig -text $n -tags node]
	} else {
		set New [.f$cnr.c create oval [expr $x-10] [expr $y-10] \
			[expr $x+10] [expr $y+10] \
			-outline black \
			-fill white \
			-tags node]
		set Lab [.f$cnr.c create text $x $y -font $HelvBig -text $n -tags node]
	
		.f$cnr.c bind $Lab <Any-Enter> "
			.f$cnr.c itemconfigure {$Lab} -fill black -text {$t}
			if {[string first \"end\" $n] < 0 } { set_src {$t} }
		"
		.f$cnr.c bind $Lab <Any-Leave> "
			.f$cnr.c itemconfigure {$Lab} -fill black -text {$n}
		"
	}
	set nodeX($New) $x
	set nodeY($New) $y
	set TLabel($New) $Lab
	set Lab2Node($Lab) $New
	set NodeWidth($New) 10
	set NodeHeight($New) 10

	update
	return $New
}

proc set_src {n} {
	set where 0
	scan $n "line %d" where
	.inp.t tag remove hilite 0.0 end
	src_line $where
}

proc mkEdge {L a b} {
	global cnr Xrem Yrem TransLabel HelvBig
	global nodeX nodeY edgeHead edgeTail

	if { $nodeY($b) > $nodeY($a) } {
		set ydiff -11
	} elseif { $nodeY($b) < $nodeY($a) } {
		set ydiff 11
	} else {
		set ydiff 0
	}
	if { $nodeX($b) > $nodeX($a) } {
		set xdiff -6
	} elseif { $nodeX($b) < $nodeX($a) } {
		set xdiff 6
	} else {
		set xdiff 0
	}
	set edge [.f$cnr.c create line \
		$nodeX($a) $nodeY($a) \
		[expr $nodeX($b) + $xdiff] \
		[expr $nodeY($b) + $ydiff] \
		 -arrow both -arrowshape {4 3 3} ]
	.f$cnr.c lower $edge
	lappend edgeHead($a) $edge
	lappend edgeTail($b) $edge

	set Xrem($edge) $xdiff
	set Yrem($edge) $ydiff

	set midX [expr $nodeX($a) + $nodeX($b)]
	set midX [expr $midX / 2 ]
	set midY [expr $nodeY($a) + $nodeY($b)]
	set midY [expr $midY / 2 ]

	set TransLabel($a,$b) \
	[.f$cnr.c create text $midX $midY -font $HelvBig -tags texttag]

	.f$cnr.c bind $edge <Button-1> "
		.f$cnr.c coords $TransLabel($a,$b) \[.f$cnr.c canvasx %x\] \[.f$cnr.c canvasy %y\]
		.f$cnr.c itemconfigure $TransLabel($a,$b) \
			-fill black -text {$L} -font $HelvBig
	"
	.f$cnr.c bind $edge <ButtonRelease-1> "
		.f$cnr.c itemconfigure $TransLabel($a,$b) \
			-fill black -text {}
	"
}

proc moveNode {cnr node mx my together} {
	global edgeHead edgeTail TLabel NodeWidth NodeHeight
	global nodeX nodeY Lab2Node
	global Xrem Yrem Scale

	set x [.f$cnr.c coords $node]
	if {[llength $x] == 2} { set node $Lab2Node($node) }

	set mx [.f$cnr.c canvasx $mx]
	set my [.f$cnr.c canvasy $my]

	set wx $NodeWidth($node)
	set wy $NodeHeight($node)

	.f$cnr.c coords $node \
		[expr $mx-$wx] [expr $my-$wy] \
		[expr $mx+$wx] [expr $my+$wy]
	.f$cnr.c coords $TLabel($node) $mx $my

	set nodeX($node) $mx
	set nodeY($node) $my
	if {$together == 0} { return }
	catch {
	foreach edge $edgeHead($node) {
		set ec [.f$cnr.c coords $edge]
		set nx [expr $nodeX($node) + $Xrem($edge)*$Scale]
		set ny [expr $nodeY($node) + $Yrem($edge)*$Scale]
		.f$cnr.c coords $edge \
			$nx $ny \
			[lindex $ec 2] [lindex $ec 3]
	}}
	catch {
	foreach edge $edgeTail($node) {
		set ec [.f$cnr.c coords $edge]
		set nx [expr $nodeX($node) + $Xrem($edge)*$Scale]
		set ny [expr $nodeY($node) + $Yrem($edge)*$Scale]
		.f$cnr.c coords $edge \
			[lindex $ec 0] [lindex $ec 1] \
			$nx $ny
	}}
}

set PlaceCanvas(msc)	""

proc mkcanvas {n m geox geoy placed} {
	global cnr tk_version
	global Chandle Sticky
	global FG BG Ptype PlaceCanvas

	incr cnr
	toplevel .f$cnr
	wm title .f$cnr "$n"
	wm iconname .f$cnr $m
	if {$placed} {
		if {$PlaceCanvas($m) == ""} {
			set PlaceCanvas($m) "+$geox+$geoy"
		}
		set k [string first "\+" $PlaceCanvas($m)]
		if {$k > 0} {
		set PlaceCanvas($m) [string range $PlaceCanvas($m) $k end]
		}
		wm geometry .f$cnr $PlaceCanvas($m)
	}
	wm minsize .f$cnr 100 100

	if {[string first "4." $tk_version] == 0 \
	||  [string first "8." $tk_version] == 0} {
		set cv [canvas .f$cnr.c  -relief raised -bd 2\
			-scrollregion {-15c -5c 30c 40c} \
			-background $BG \
			-xscrollcommand ".f$cnr.hscroll set" \
			-yscrollcommand ".f$cnr.vscroll set"]
		scrollbar .f$cnr.vscroll -relief sunken \
			-command ".f$cnr.c yview"
		scrollbar .f$cnr.hscroll -relief sunken -orient horiz \
			-command ".f$cnr.c xview"
	} else {
		set cv [canvas .f$cnr.c  -relief raised -bd 2\
			-scrollregion {-15c -5c 30c 40c} \
			-background $BG \
			-xscroll ".f$cnr.hscroll set" \
			-yscroll ".f$cnr.vscroll set"]
		scrollbar .f$cnr.vscroll -relief sunken \
			-command ".f$cnr.c yview"
		scrollbar .f$cnr.hscroll -relief sunken -orient horiz \
			-command ".f$cnr.c xview"
	}
	set Chandle($cnr) $cv
	#-width 500 -height 500

	button .f$cnr.b1 -text "Close" \
		-command "set PlaceCanvas($m) [wm geometry .f$cnr]; destroy .f$cnr"
	button .f$cnr.b2 -text "Save in: $m.ps" \
		-command "$cv postscript -file $m.ps -colormode $Ptype"

	pack append .f$cnr \
		.f$cnr.vscroll {right filly} \
		.f$cnr.hscroll {bottom fillx} \
		.f$cnr.c {top expand fill}

	if {$m == "msc"} {
		set Sticky($cnr) 0
		checkbutton .f$cnr.b6 -text "Preserve" \
			-variable Sticky($cnr) \
			-relief flat
		pack append .f$cnr \
			.f$cnr.b6 { right padx 5}
	}
	pack append .f$cnr \
		.f$cnr.b1 {right padx 5} \
		.f$cnr.b2 {right padx 5}

	bind $cv <2> "$cv scan mark %x %y"	;# Geert Janssen, TUE
	bind $cv <B2-Motion> "$cv scan dragto %x %y"

	.f$cnr.c bind node <B1-Motion> "
		moveNode $cnr \[.f$cnr.c find withtag current] %x %y 1
	"

#	.f$cnr.c bind node <B2-Motion> "
#		moveNode $cnr \[.f$cnr.c find withtag current] %x %y 1
#	"

	tkwait visibility .f$cnr
	return $cnr
}

proc addscales {p} {
	global Chandle Scale

	catch {
		set cv $Chandle($p)
		button .f$p.b4 -text "Larger" \
			-command "$cv scale all 0 0 1.1 1.1; set Scale [expr $Scale*1.1]"
		button .f$p.b5 -text "Smaller" \
			-command "$cv scale all 0 0 0.9 0.9; set Scale [expr $Scale*0.9]"
		pack append .f$p \
			.f$p.b4 {right padx 5} \
			.f$p.b5 {right padx 5}
	}
}

proc dodot {n} {
	global Edges edgeHead edgeTail NodeWidth NodeHeight Maxx Maxy
	global State ELabel TransLabel Unix cnr lcnr Xrem Yrem DOT

	add_log "<dot graph layout...>"
	set fd [open "|$DOT" w+]

	puts $fd "digraph dodot {"

	foreach el [array names Edges] {
		if { [ string first $n $el ] >= 0 } {
		for {set i 0} { [lindex $Edges($el) $i] != "" } {incr i} {
			set ntrg [lindex $Edges($el) $i]
			puts $fd " \"$el\" -> \"$ntrg\"; "
		}
	}}

	puts $fd "}"
	flush $fd
	set ends ""
	set nodot 1
	while {[gets $fd line] > -1} {
		if {[string first "\}" $line] >= 0} {
			break;
		}
		set dd [string length $line]; incr dd -1
		while {[string range $line $dd $dd] == "\\"} {
			gets $fd more
			set line "[string range $line 0 [expr $dd-1]]$more"
			set dd [string length $line]; incr dd -1
		}
		if {[string first " -> " $line] >= 0} {
			set a [string first "\[pos=\"" $line]; incr a 8
			set b [string first "\"\];" $line]; incr b -1
			set b2 [string first "->" $line]
			set line1 [string range $line 0 [expr $a - 9]]
			set src [string range $line1 0 [expr $b2 - 1]]
			set src [string trim $src "	 \""]
			set trg [string range $line1 [expr $b2 + 3] [expr $a - 1]]
			set trg [string trim $trg "	 \""]
			set tp [string range $line [expr $a-2] [expr $a-2]]
			set line [string range $line $a $b]
			set k [split $line " "]
			set j [llength $k]
			set j2 [trunc [expr $j/2]]
			set coords ".f$cnr.c create line "
			set spline "-smooth 1"
			set nl $ELabel($src,$trg)
			if {$tp == "e"} {
				set ends "last"
				for {set i 1} {$i < $j} {incr i} {
					scan [lindex $k $i] "%d,%d" x y
					set coords " $coords[expr 50 + $x] [expr 50 + $Maxy - $y] "
					if {$i == $j2} {
						.f$cnr.c coords \
							$TransLabel($State($src),$State($trg)) \
							[expr 50 + $x] [expr 50 + $Maxy - $y]
						.f$cnr.c itemconfigure \
							$TransLabel($State($src),$State($trg)) \
							-fill black -text "$nl"
					}
				}
				scan [lindex $k 0] "%d,%d" x y
				set coords " $coords[expr 50 + $x] [expr 50 + $Maxy - $y] "
			} else {
				set ends "first"
				for {set i 0} {$i < $j} {incr i} {
					scan [lindex $k $i] "%d,%d" x y
					set coords " $coords[expr 50 + $x] [expr 50 + $Maxy - $y] "
					if {$i == $j2} {
						.f$cnr.c coords \
							$TransLabel($State($src),$State($trg)) \
							[expr 50 + $x] [expr 50 + $Maxy - $y]
						.f$cnr.c itemconfigure \
							$TransLabel($State($src),$State($trg)) \
							-fill black -text "$nl"
			}	}	}
			set coords "$coords -arrow $ends $spline -tags connector"

			set ne [eval $coords]
			set Xrem($ne) 10
			set Yrem($ne) 10

			continue
		}
		if {[string first "node " $line] >= 0 \
		||  [string first "\{" $line]    >= 0} {
			continue
		}
		if {[string first "graph " $line] >= 0} {
			set a [string first "\"" $line]; incr a
			set b [string last  "\"" $line]; incr b -1
			set line [string range $line $a $b]
			set k [split $line ","]
			if {[llength $k] == 4} {
				set Maxx [lindex $k 2]
				set Maxy [lindex $k 3]
			} else {
				set Maxx [lindex $k 0]
				set Maxy [lindex $k 1]
			}
			set nodot 0
		} else {	;# a node
			set a [string first "\[" $line]; incr a
			set b [string last  "\]" $line]; incr b -1
			set line1 [string range $line 0 [expr $a - 2]]
			set line  [string range $line $a $b]
			set nn [string trim $line1 "	 \""]

			set a [string first "pos=" $line]; incr a 5
			set b [string first "\"" [string range $line $a end]]
			set b [expr $a + $b - 1]
			set line1  [string range $line $a $b]
			set k [split $line1 ","]
			set x [lindex $k 0]
			set y [lindex $k 1]

			set a [string first "width=" $line]; incr a 7
			set b [string first "\"" [string range $line $a end]]
			set b [expr $a + $b - 1]
			set w [expr 75 * [string range $line $a $b]]

			set a [string first "height=" $line]; incr a 8
			set b [string first "\"" [string range $line $a end]]
			set b [expr $a + $b - 1]
			set h [expr 75 * [string range $line $a $b]]

		catch {
			set NodeWidth($State($nn)) [expr $w/2]
			set NodeHeight($State($nn)) [expr $h/2]
			moveNode $lcnr $State($nn) \
				[expr 50 + $x] [expr 50 + $Maxy - $y] 0
		} err
#puts $err
		}
	}
	catch { close $fd }

	if {$nodot} {
		add_log "<cannot find dot>"
		catch {
		tk_messageBox -icon info -message "<cannot find dot>"
		}
		return
	}

	foreach el [array names Edges] {
		if { [ string first $n $el ] >= 0 } {
			catch {
			foreach edge $edgeHead($State($el)) {
				.f$cnr.c delete $edge
			}
			unset edgeHead($State($el))
			unset edgeTail($State($el))
			}
	}	}
	.f$cnr.c bind node <B1-Motion> {}	;# no moving
	.f$cnr.c bind node <B2-Motion> {}
	catch { destroy .f$lcnr.b6 }
#	button .f$lcnr.b6 -text "No Labels" \
#		-command ".f$lcnr.c delete texttag; destroy .f$lcnr.b6"
	button .f$lcnr.b6 -text "No Labels" \
		-command "hide_automata_labels .f$lcnr.b6 .f$cnr.c"
	pack append .f$lcnr .f$lcnr.b6 {right padx 5}
}

proc hide_automata_labels {b c} {
	$b configure -text "Add Labels"
	$c itemconfigure texttag -fill white
	$b configure -command "show_automata_labels $b $c"
}

proc show_automata_labels {b c} {
	$b configure -text "No Labels"
	$c itemconfigure texttag -fill black
	$b configure -command "hide_automata_labels $b $c"
}

proc trunc {p} {
	set foo [string first "." $p]
	if {$foo >= 0} {
		incr foo -1
		set p [string range $p 0 $foo]
	}
	return $p
}

# Help menus

proc aboutspin {} {
	global FG BG HelvBig version xversion

	catch {destroy .h}
	toplevel .h

	wm title .h "About SPIN"
	wm iconname .h "About"
	message .h.t -width 600 -background $BG -foreground $FG -font $HelvBig \
	-text " $version
Xspin Version $xversion

Spin is an on-the-fly LTL model checking system
for proving properties of asynchronous software
system designs, first distributed in 1991.

The master sources for the latest version of
this software can always be found via:

http://spinroot.com/spin/whatispin.html

For help:  spin_list@spinroot.com

The Spin sources are (c) 1990-2004 Bell Labs,
Lucent Technologies, Murray Hill, NJ, USA.
All rights are reserved. This software is for
educational and research purposes only.
No guarantee whatsoever is expressed or implied
by the distribution of this code.
"
	button .h.b -text "Ok" -command {destroy .h}
	pack append .h .h.t {top expand fill}
	pack append .h .h.b {top}
}

proc promela {} {
	global FG BG HelvBig

	catch {destroy .h}
	toplevel .h

	wm title .h "Promela URL"
	wm iconname .h "Promela"
	message .h.t -width 600 -background $BG -foreground $FG -font $HelvBig \
	-text "All Promela references are available online:

http://spinroot.com/spin/Man/index.html

"
	button .h.b -text "Ok" -command {destroy .h}
	pack append .h .h.t {top expand fill}
	pack append .h .h.b {top}
}

proc helper {} {
	global FG BG HelvBig

	catch {destroy .h}
	toplevel .h

	wm title .h "Help with Xspin"
	wm iconname .h "Help"
	message .h.t -background $BG -foreground $FG -font $HelvBig \
	-text "\
Spin Version Controller - (c) 1993-2004 Bell Laboratories

Enter a Promela model into the main text window, or 'Open'
one via the File Menu (e.g., from Spin's Test directory).
Once loaded, you can revert to the stored version of the file
with option ReOpen.  Select Clear to empty the text window.

In the log, just below the text-window, background
commands are printed that Xspin generates.
Outputs from Simulation and Verification runs always
appear in separate windows.

All run-time options are available through the Run menu.
A typical way of working with Xspin is to use:

- First a Syntax Check to get hints and warnings
- Random Simulation for further debugging
- Add the properties to be verified (assertions, never claims)
- Perform a Slicing Check to check for redundancy
- Perform Verification for a correctness proof
- Guided Simulation to inspect errors reported by
  the Verification option

Clicking Button-1 in the main window updates the
Line number display at the top of the window -- as a
simple way of finding out at what line you are.

You can also use another editor to update the
specifications outside Xspin, and use the ReOpen
command from the File menu to refresh the Xspin
edit buffer before starting each new simulation or
verification run."
	button .h.b -text "Ok" -command {destroy .h}
	pack append .h .h.t {top expand fill}
	pack append .h .h.b {top}
}

# LTL interface

set formula ""
set tl_stat 0

proc put_template {s} {
	.tl.main.e1 delete 0 end
	.tl.main.e1 insert end "$s"
}

set PlaceTL	"+100+1"

proc call_tl {} {	;# expanded interface
	global formula tl_stat nv_typ an_typ cp_typ
	global FG BG Fname firstime PlaceTL

	catch {destroy .tl}
	toplevel .tl

	set k [string first "\+" $PlaceTL]
	if {$k > 0} {
		set PlaceTL [string range $PlaceTL $k end]
	}

	wm title .tl "Linear Time Temporal Logic Formulae"
	wm iconname .tl "LTL"
	wm geometry .tl $PlaceTL

	frame .tl.main
	entry .tl.main.e1 -relief sunken \
		-background $BG -foreground $FG
	label .tl.main.e2 -text "Formula: "

	frame .tl.op
	set alw {\[\] }
	set eve {\<\> }
	pack append .tl.op [label .tl.op.s0 -text "Operators: " \
		-relief flat] {left}
	pack append .tl.op [button .tl.op.always -width 1 -text "\[\]" \
		-command ".tl.main.e1 insert insert \"$alw \""] {left}
	pack append .tl.op [button .tl.op.event -width 1 -text "\<\>" \
		-command ".tl.main.e1 insert insert \"$eve \""] {left}
	pack append .tl.op [button .tl.op.until -width 1 -text "U" \
		-command ".tl.main.e1 insert insert \" U \""] {left}
	pack append .tl.op [button .tl.op.impl -width 1 -text "->" \
		-command ".tl.main.e1 insert insert \" -> \""] {left}
	pack append .tl.op [button .tl.op.and -width 1 -text "and" \
		-command ".tl.main.e1 insert insert \" && \""] {left}
	pack append .tl.op [button .tl.op.or -width 1 -text "or" \
		-command ".tl.main.e1 insert insert \" || \""] {left}
	pack append .tl.op [button .tl.op.not -width 1 -text "not" \
		-command ".tl.main.e1 insert insert \" ! \""] {left}

	frame .tl.b -relief ridge -borderwidth 4
	label .tl.b.s0 -text "Property holds for: "
	radiobutton .tl.b.s1 -text "All Executions (desired behavior)" \
		-variable tl_stat -value 0
	radiobutton .tl.b.s2 -text "No Executions (error behavior)" \
		-variable tl_stat -value 1
	pack append .tl.b \
		.tl.b.s0 {left} \
		.tl.b.s1 {left} \
		.tl.b.s2 {left}

	.tl.main.e1 insert end $formula

	button .tl.main.file -text "Load..." \
		-command "browse_tl"

	bind .tl.main.e1 <Return> { do_ltl }

	pack append .tl.main \
		.tl.main.e2 {top left}\
		.tl.main.e1 {top left expand fill} \
		.tl.main.file {top right}

	pack append .tl .tl.main {top fillx frame e}
	pack append .tl .tl.op {top frame w}
	pack append .tl .tl.b {top fillx frame w}

	frame .tl.macros -relief ridge -borderwidth 4
	label .tl.macros.title -text "Symbol Definitions:" -relief flat
	scrollbar .tl.macros.s -relief flat \
		-command ".tl.macros.t yview"
	text .tl.macros.t -height 4 -relief raised -bd 2 \
		-yscrollcommand ".tl.macros.s set" \
		-background $BG -foreground $FG \
		-setgrid 1 \
		-wrap word

	pack append .tl.macros \
		.tl.macros.title {top frame w} \
		.tl.macros.s {left filly} \
		.tl.macros.t {left expand fill}

	frame .tl.notes -relief ridge -borderwidth 4
	label .tl.notes.title -text "Notes: " -relief flat
	scrollbar .tl.notes.s -relief flat \
		-command ".tl.notes.t yview"
	text .tl.notes.t -height 4 -relief raised -bd 2 \
		-yscrollcommand ".tl.notes.s set" \
		-background $BG -foreground $FG \
		-setgrid 1 \
		-wrap word
	pack append .tl.notes \
		.tl.notes.title {top fillx frame w} \
		.tl.notes.s {left filly} \
		.tl.notes.t {left expand fill}

	frame .tl.never
	frame .tl.never.top
	label .tl.never.top.title -text "Never Claim:"\
		 -relief flat
	button .tl.never.top.gc -text "Generate" \
		-command "do_ltl"
	pack append .tl.never.top \
		.tl.never.top.gc {right}\
		.tl.never.top.title {left}

	scrollbar .tl.never.s -relief flat \
		-command ".tl.never.t yview"
	text .tl.never.t -height 8 -relief raised -bd 2 \
		-yscrollcommand ".tl.never.s set" \
		-setgrid 1 \
		-wrap word
	pack append .tl.never \
		.tl.never.top {top fillx frame w} \
		.tl.never.s {left filly} \
		.tl.never.t {left expand fill}

	frame .tl.results
	frame .tl.results.top

	button .tl.results.top.svp -text "Run Verification" \
		-command "do_ltl; basicval2"
	label .tl.results.top.title -text "Verification Result:"\
		 -relief flat
	pack append .tl.results.top \
		.tl.results.top.svp {right}\
		.tl.results.top.title {left}

	scrollbar .tl.results.s -relief flat \
		-command ".tl.results.t yview"
	text .tl.results.t -height 7 -relief raised -bd 2 \
		-yscrollcommand ".tl.results.s set" \
		-setgrid 1 \
		-wrap word
	pack append .tl.results \
		.tl.results.top {top fillx frame w} \
		.tl.results.s {left filly} \
		.tl.results.t {left expand fill}

	pack append .tl \
		.tl.notes {top expand fill} \
		.tl.macros {top expand fill} \
		.tl.never {top expand fill} \
		.tl.results {top expand fill} \

	pack append .tl [button .tl.sv -text "Save As.." \
		-command "save_tl"] {right}
	pack append .tl [button .tl.exit -text "Close" \
	-command "set PlaceTL [wm geometry .tl]; destroy .tl"] {right}

	pack append .tl [button .tl.help -text "Help" -fg red \
		-command "roadmap4"] {left}
	pack append .tl [button .tl.clear -text "Clear" \
		-command ".tl.main.e1 delete 0 end; .tl.never.t delete 0.0 end"] {left}

	loaddefault_tl
	focus .tl.main.e1
}

proc purge_nvr {foo} {
	set j [llength $foo]; incr j -1
	for {set i $j} {$i >= 0} {incr i -1} {
		set k [lindex $foo $i]
		set kk [expr $k+1]
		.tl.never.t delete $k.0 $kk.0
	}
}

proc grab_nvr {inp target} {

	set pattern $inp
	scan [.tl.never.t index end] %d numLines
	set foo {}
	set yes 0

	for {set i 1} {$i < $numLines} { incr i} {
		.tl.never.t mark set last $i.0
		set have [.tl.never.t get last "last lineend + 1 chars"]
		if {[regexp -indices $pattern $have indices]} {
			lappend foo $i
			set yes [expr 1 - $yes]
			if {$yes} {
				set pattern "#endif"
			} else {
				set pattern $inp
			}
		}
		if {$yes && [string first $inp $have] != 0} {
			$target insert end "$have"
			lappend foo $i
		}
	}
	purge_nvr $foo
}

proc extract_defs {} {
	global tl_stat

	set pattern "#define "
	scan [.tl.never.t index end] %d numLines
	set foo {}
	set tl_stat 1
	for {set i 1} {$i < $numLines} { incr i} {
		.tl.never.t mark set last $i.0
		set have [.tl.never.t get last "last lineend + 1 chars"]
		if {[regexp -indices $pattern $have indices]} {
			.tl.macros.t insert end "$have"
			lappend foo $i
		}
		set have [.tl.never.t get last "last lineend"]
		set k [string first "Formula As Typed: " $have]
		if {$k > 0} {
			set ff [string range $have [expr $k+18] end]
			.tl.main.e1 insert end $ff
		}
		if {[string first "To The Negated Formula " $have] > 0} {
			set tl_stat 0
		}
	}
	purge_nvr $foo

	grab_nvr "#ifdef NOTES"  .tl.notes.t
	grab_nvr "#ifdef RESULT" .tl.results.t
}

proc inspect_ltl {} {
	global formula
	set formula "[.tl.main.e1 get]"

	set x $formula
	regsub -all {\&\&} "$x" " " y; set x $y
	regsub -all {\|\|} "$x" " " y; set x $y
	regsub -all {\/\\} "$x" " " y; set x $y
	regsub -all {\\\/} "$x" " " y; set x $y
	regsub -all {\!}  "$x" " " y; set x $y
	regsub -all {<->} "$x" " " y; set x $y
	regsub -all {\->}  "$x" " " y; set x $y
	regsub -all {\[\]} "$x" " " y; set x $y
	regsub -all {\<\>} "$x" " " y; set x $y
	regsub -all {[()]} "$x" " " y; set x $y
	regsub -all {\ \ *} "$x" " " y; set x $y
	regsub -all { U} "$x" " " y; set x $y
	regsub -all { V} "$x" " " y; set x $y
	regsub -all { X} "$x" " " y; set x $y

	set predefs " np_ true false "

	set k [split $x " "]
	set j [llength $k]
	set line [.tl.macros.t get 0.0 end]
	for {set i 0} {$i < $j} {incr i} {
		if {[string length [lindex $k $i]] > 0 \
		&&  [string first " [lindex $k $i] " $predefs] < 0} {
		  set pattern "#define [lindex $k $i]"
		  if {[string first $pattern $line] < 0} {
			catch {
			.tl.macros.t insert end "$pattern\t?\n"
			}
			set line [.tl.macros.t get 0.0 end]
	}	} }
}

proc do_ltl {} {
	global formula tl_stat SPIN tk_major tk_minor

	set formula "[.tl.main.e1 get]"
	.tl.never.t delete 0.0 end
	update

	catch { inspect_ltl }

	set MostSystems 1	;# change to 0 only if there are problems
				;# see below

	if {$tl_stat == 0} {
		add_log "$SPIN -f \"!( $formula )\""
		if {$MostSystems} {
			catch {exec $SPIN -f "!($formula)" >&pan.ltl} err
		} else {
			# this variant was needed on some older systems,
			# but it causes problems on some of the newer ones...
			catch {exec $SPIN -f \"!($formula)\" >&pan.ltl} err
		}
	} else {
		add_log "$SPIN -f \"( $formula )\""
		if {$MostSystems} {
		catch {exec $SPIN -f "($formula)" >&pan.ltl} err
		} else {
		# see above
		catch {exec $SPIN -f \"($formula)\" >&pan.ltl} err
		}
	}
	set lno 0

	if {$err != ""} {
		add_log "<error: $err>"
		add_log "hint: check the Help Button for syntax rules"
	} else {
		.tl.never.t insert end \
		"	/*\n"
		.tl.never.t insert end \
		"	 * Formula As Typed: $formula\n"
		incr lno 2
		if {$tl_stat == 0} {
			.tl.never.t insert end \
			"	 * The Never Claim Below Corresponds\n"
			.tl.never.t insert end \
			"	 * To The Negated Formula !($formula)\n"
			.tl.never.t insert end \
			"	 * (formalizing violations of the original)\n"
			incr lno 3
		}
		.tl.never.t insert end \
		"	 */\n\n"
		incr lno 2
	}
	catch {
		set fd [open pan.ltl r]
		while {[gets $fd line] > -1} {
			.tl.never.t insert end "$line\n"
		}
		close $fd
	}
	rmfile pan.ltl
}

proc dump_tl {bb} {

	if {$bb != ""} {
		set fnm $bb
	} else {
		set fnm [.sv_tl.ent get]
	}

	if {[file_ok $fnm]==0} return
	set fd [open $fnm w]
	add_log "<save claim in $fnm>"
	catch {	puts $fd "[.tl.macros.t get 0.0 end]" nonewline }

	puts $fd "[.tl.never.t get 0.0 end]" nonewline

	catch {	puts $fd "#ifdef NOTES"
		puts $fd "[.tl.notes.t get 0.0 end]" nonewline
		puts $fd "#endif"
	}
	catch {	puts $fd "#ifdef RESULT"
		puts $fd "[.tl.results.t get 0.0 end]" nonewline
		puts $fd "#endif"
	}

	catch "flush $fd"
	catch "close $fd"
	catch "destroy .sv_tl"
	catch "focus .tl.main.e1"
}

proc save_tl {} {
	global Fname PlaceWarn
	catch {destroy .sv_tl}
	toplevel .sv_tl

	wm title .sv_tl "Save Claim"
	wm iconname .sv_tl "Save"
	wm geometry .sv_tl $PlaceWarn

	label  .sv_tl.msg -text "Name for LTL File: " -relief flat
	entry  .sv_tl.ent -width 6 -relief sunken -textvariable fnm
	button .sv_tl.b1 -text "Ok" -command { dump_tl "" }
	button .sv_tl.b2 -text "Cancel" -command "destroy .sv_tl"
	bind   .sv_tl.ent <Return> { dump_tl "" }

	set fnm [.sv_tl.ent get]
	if {$fnm == ""} {
		.sv_tl.ent insert end "$Fname.ltl"
	}

	pack append .sv_tl \
		.sv_tl.msg {top frame w} \
		.sv_tl.ent {top frame e expand fill} \
		.sv_tl.b1 {right frame e} \
		.sv_tl.b2 {right frame e}
	focus .sv_tl.ent
}

proc add_tl {} {
	global BG FG HelvBig PlaceWarn
	catch {destroy .warn}
	toplevel .warn
	set k [string first "\+" $PlaceWarn]
	if {$k > 0} {
		set PlaceWarn [string range $PlaceWarn $k end]
	}

	wm title .warn "Accept"
	wm iconname .warn "Accept"
	wm geometry .warn $PlaceWarn

	message .warn.t -width 300 \
		-background $BG -foreground $FG -font $HelvBig \
		-text " \
Instructions:

1. Save the Never Claim in a file, \
for instance a file called 'never', \
using the <Save> button.

2. Insert the line

#include \"never\"

(the name of the file with the claim) \
at the end of the main specification.

3. Insert macro definitions (#define's) for all \
propositional symbols used in the formula.

For instance, with LTL formula
'[] p -> <> q'  add the macro defs:

#define p	(cnt == 1)
#define q	(cnt > 1)

These macros must be defined just above the line \
with the #include \"never\" directive

4. Perform the verification, and make sure that \
the box 'Apply Never Claim' is checked in the \
Verification Panel (or else the claim is ignored).
You can have a library of claim files that you can \
choose from for verification, by changing only the \
name of the include file.

5. Never claims have no effect during simulation runs.

6. See the HELP->LTL menu for more information.

"
	button .warn.b -text "Ok" \
		-command {set PlaceWarn [wm geometry .warn]; destroy .warn}
	pack append .warn .warn.t {top expand fill}
	pack append .warn .warn.b {right frame e}
}

proc roadmap4 {} {
	global FG BG

	catch {destroy .h}
	toplevel .h

	wm title .h "LTL Help"
	wm iconname .h "Help"
	frame .h.z
	scrollbar .h.z.s -command ".h.z.t yview"
	text .h.z.t -relief raised -bd 2 \
		-background $BG -foreground $FG \
		-yscrollcommand ".h.z.s set" \
		-setgrid 1 -width 60 -height 30 -wrap word
	pack append .h.z \
		.h.z.s {left filly} \
		.h.z.t {left expand fill}
	.h.z.t insert end "GUIDELINES:
You can load an LTL template or a previously saved LTL
formula from a file via the LOAD button on the upper
right of the LTL Property Manager panel.

Define a new LTL formula using lowercase names for the
propositional symbols, for instance:
	[] (p U q)
The formula expresses either a positive (desired) or a
negative (undesired) property of the model.  A positive
property is negated automatically by the translator to
convert it in a never claim (which expresses the
corresponding negative property (the undesired behavior
that is claimed 'never' to occur).

When you type a <Return> or hit the <Generate> button,
the formula is translated into an equivalent never-claim.

You must add a macro-definition for each propositional
symbol used in the LTL formula.  Insert these definitions
in the symbols window of the LTL panel, they will be
remembered together with the annotations and verification
result if the formula is saved in an .ltl file.
Enclose the symbol definitions in braces, to secure correct
operator precedence, for instance:

#define p	(a > b)
#define q	(len(q) < 5)

Valid temporal logic operators are:
	\[\]  Always (no space between \[ and \])
	<>  Eventually (no space between < and >)
	U   (Strong) Until
	V   The Dual of Until: (p V q) == !(!p U !q)

	All operators are left-associative (incl. U and V).

Boolean Operators:
	&&  Logical And (alternative form: /\\, no spaces)
	!   Logical Negation
	||  Logical Or  (alternative form: \\/, no spaces)
	->  Logical Implication
	<-> Logical Equivalence

Boolean Predicates:
	true, false
	any name that starts with a lowercase letter

Examples:
	\[\] p
	!( <> !q )
	p U q
	p U (\[\] (q U r))

Generic properties/Templates:
	Invariance: \[\] p
	Response:   p -> \<\> q
	Precedence: p -> (q U r)
	Objective:  p -> \<\> (q || r)

	Each of the above 4 generic types of properties
	can (and will generally have to) be prefixed by
	temporal operators such as
		\[\], \<\>, \[\]\<\>, \<\>\[\]
	The last (objective) property can be read to mean
	that 'p' is a trigger, or 'enabling' condition that
	determines when the requirement becomes applicable
	(e.g. the sending of a new data message); then 'q'
	can be the fullfillment of the requirement (e.g.
	the arrival of the matching acknowledgement), and
	'r' could be a discharging condition that voids the
	applicability of the check (an abort condition).
"
	button .h.b -text "Ok" -command {destroy .h}
	pack append .h .h.z {top expand fill}
	pack append .h .h.b {top}
	.h.z.t configure -state disabled 
	.h.z.t yview -pickplace 1.0      
	focus .h.z.t
}



# Specific Help

proc roadmap1 {} {
	global FG BG

	catch {destroy .road1}
	toplevel .road1

	wm title .road1 "Help with Simulation"
	wm iconname .road1 "SimHelp"
	frame .road1.z
	scrollbar .road1.z.s -command ".road1.z.t yview"
	text .road1.z.t -relief raised -bd 2 \
		-background $BG -foreground $FG \
		-yscrollcommand ".road1.z.s set" \
		-setgrid 1 -width 60 -height 30 -wrap word
	pack append .road1.z \
		.road1.z.s {left filly} \
		.road1.z.t {left expand fill}
	.road1.z.t insert end "GUIDELINES:
0.  Always use a Syntax Check before running simulations.\
It shakes out the more obvious flaws in the model.

1.  Random simulation option is used to debug a model.\
Other than assert statements, no correctness requirements\
are checked during simulation runs. All nondeterministic\
decisions are resolved randomly.  You can of course still\
force a selection to go into a specific direction by \
modifying the model.\
A random run is repeated precisely if the Seed Value\
for the random number generator is kept the same.

2.  Interactive simulation can be used to force the\
execution towards a known point.  The user is prompted\
at every point in the execution where a nondeterministic\
choice has to be resolved.

3.  A guided simulation is used to follow an error-trail that was\
produced by the verifier.  If the trail gets to be thousands of execution\
steps long, this can be time-consuming. \
You can skip the initial portion of such a long trail by typing\
a number in  the 'Steps Skipped' box in the Simulation Panel .

4. The options in the Simulations Panel allow you to enable or\
disable types of displays that are maintained during simulation\
runs.  Usually, it is not necessary to look at all possible display panels.\
Experiment to see which displays you find most useful.

5. To track the value changes of Selected variables, in the\
Message Sequence Chart and in the Variable Values Panel, add a prefix\
'show ' to the declaration of the selected variables in the Promela\
specification, e.g. use 'show byte cnt;' instead of 'byte cnt;'"

	button .road1.b -text "Ok" -command {destroy .road1}
	pack append .road1 .road1.z {top expand fill}
	pack append .road1 .road1.b {top}
	.road1.z.t configure -state disabled 
	.road1.z.t yview -pickplace 1.0      
	focus .road1.z.t
}

proc roadmap2a {} {
	global FG BG

	catch {destroy .road2}
	toplevel .road2

	wm title .road2 "Help with Verification Parameters"
	wm iconname .road2 "ValHelp"
	frame .road2.z
	scrollbar .road2.z.s -command ".road2.z.t yview"
	text .road2.z.t -relief raised -bd 2 \
		-background $BG -foreground $FG \
		-yscrollcommand ".road2.z.s set" \
		-setgrid 1 -width 60 -height 18 -wrap word
	pack append .road2.z \
		.road2.z.s {left filly} \
		.road2.z.t {left expand fill}
	.road2.z.t insert end "Physical Memory Available:
Set this number to amount of physical (not virtual)
memory in your system, in MegaBytes, and leave it there for all runs.

When the limit is reached, the verification is stopped to
avoid trashing.

The number entered here is the number of MegaBytes directly
(not a power of two, as in previous versions of xspin).

If an exhaustive verification cannot be completed due to
lack of memory, use compression, or switch to a
supertrace/bitstate run under basic options."

	button .road2.b -text "Ok" -command {destroy .road2}
	pack append .road2 .road2.z {top expand fill}
	pack append .road2 .road2.b {top}
	.road2.z.t configure -state disabled 
	.road2.z.t yview -pickplace 1.0      
	focus .road2.z.t
}
proc roadmap2b {} {
	global FG BG

	catch {destroy .road2}
	toplevel .road2

	wm title .road2 "Help with Verification"
	wm iconname .road2 "ValHelp"
	frame .road2.z
	scrollbar .road2.z.s -command ".road2.z.t yview"
	text .road2.z.t -relief raised -bd 2 \
		-background $BG -foreground $FG \
		-yscrollcommand ".road2.z.s set" \
		-setgrid 1 -width 60 -height 15 -wrap word
	pack append .road2.z \
		.road2.z.s {left filly} \
		.road2.z.t {left expand fill}
	.road2.z.t insert end "Estimated State Space Size:
This parameter is used to calculate the size of the
hash-table. It results in a selection of a numeric argument
for the -w flag of the verifier. Setting it too high may
cause an out-of-memory error with zero states reached
(meaning that the verification could not be started).
Setting it too low can cause inefficiencies due to
hash collisions.

In Bitstate runs begin with the default estimate for
this parameter.  After a run completes successfully,
double the estimate, and see if the number of reached
stated changes much.  Continue to do this until
it stops changing, or until you overflow the memory
bound and run out of memory.

The closest power of two is taken by xspin to set the
true number used for the number of reachable states.
(The selected power of two is visible as the number that
follow the -w flag in the run-line that xspin generates).

To set a specific -w parameter, use the Extra Run-Time Option
Field. If, for instance, -w32 is specified there, it will
override the value computed from the Estimated State Space Size."

	button .road2.b -text "Ok" -command {destroy .road2}
	pack append .road2 .road2.z {top expand fill}
	pack append .road2 .road2.b {top}
	.road2.z.t configure -state disabled 
	.road2.z.t yview -pickplace 1.0      
	focus .road2.z.t
}
proc roadmap2c {} {
	global FG BG

	catch {destroy .road2}
	toplevel .road2

	wm title .road2 "Help with Verification"
	wm iconname .road2 "ValHelp"
	frame .road2.z
	scrollbar .road2.z.s -command ".road2.z.t yview"
	text .road2.z.t -relief raised -bd 2 \
		-background $BG -foreground $FG \
		-yscrollcommand ".road2.z.s set" \
		-setgrid 1 -width 60 -height 20 -wrap word
	pack append .road2.z \
		.road2.z.s {left filly} \
		.road2.z.t {left expand fill}
	.road2.z.t insert end "Maximum Search Depth:
This number determines the size of the depth-first
search stack that is used during the verification.
The stack uses memory, so a larger number increases
the memory requirements, and a lower number decreases
it.  In a tight spot, when there seems not to be
sufficient memory for the search depth needed, you
can reduce the estimated state space size to free some
more memory for the stack.

If you hit the maximum search depth during a verification
(noted as 'Search not completed' or 'Search Truncated'
in the verification output) without finding an error,
double the search depth parameter and repeat the run."

	button .road2.b -text "Ok" -command {destroy .road2}
	pack append .road2 .road2.z {top expand fill}
	pack append .road2 .road2.b {top}
	.road2.z.t configure -state disabled 
	.road2.z.t yview -pickplace 1.0      
	focus .road2.z.t
}

proc roadmap2k {} {
	global FG BG

	catch {destroy .road2}
	toplevel .road2

	wm title .road2 "Help with Verification"
	wm iconname .road2 "ValHelp"
	frame .road2.z
	scrollbar .road2.z.s -command ".road2.z.t yview"
	text .road2.z.t -relief raised -bd 2 \
		-background $BG -foreground $FG \
		-yscrollcommand ".road2.z.s set" \
		-setgrid 1 -width 60 -height 10 -wrap word
	pack append .road2.z \
		.road2.z.s {left filly} \
		.road2.z.t {left expand fill}
	.road2.z.t insert end "Number of hash functions:
This number determines how many bits are set per
state when in Bitstate verification mode. The default is 2.
At the end of a Bitstate verification run, the verifier
can issue a recommendation for a different setting of
this flag (which is the -k flag), it a change can be
predicted to lead to better coverage."

	button .road2.b -text "Ok" -command {destroy .road2}
	pack append .road2 .road2.z {top expand fill}
	pack append .road2 .road2.b {top}
	.road2.z.t configure -state disabled 
	.road2.z.t yview -pickplace 1.0      
	focus .road2.z.t
}

proc roadmap2d {} {
	global FG BG

	catch {destroy .road2}
	toplevel .road2

	wm title .road2 "Help with Verification"
	wm iconname .road2 "ValHelp"
	frame .road2.z
	scrollbar .road2.z.s -command ".road2.z.t yview"
	text .road2.z.t -relief raised -bd 2 \
		-background $BG -foreground $FG \
		-yscrollcommand ".road2.z.s set" \
		-setgrid 1 -width 60 -height 26 -wrap word
	pack append .road2.z \
		.road2.z.s {left filly} \
		.road2.z.t {left expand fill}
	.road2.z.t insert end "GENERAL GUIDELINES:
=> When just starting out, it is safe to leave all parameters in the\
Verification Options Panel set at their initial value and to simply\
push the Run button in the Basic Options Panel for a default\
exhaustive verification.\
If you run out of memory, adjust the parameter settings as \
indicated under the 'explain' options.

=> If an error is found, first try to reduce the search depth to \
find a shorter equivalent.  Once you're content with the length,\
move on to a guided simulation to inspect the error-trail in detail.\
Optionally, use the Find Shortest Trail option, but note that this\
can increase runtime and memory use. So: do not use this option until\
you are certain that an error exists -- leave it turned off by default).\
If you are verifying a Safety Property, try the Breadth-First Search\
mode to find the shortest counter-example. It may run out of memory\
sooner than the default depth-first search mode, but it often works.

=> It is always safe to leave the Partial Order Reduction option enabled.\
Turn it off only for debugging purposes, or when warned to do so by the \
verifier itself.  The Profiling option gathers statistics about the \
verification hot-spots in the model.

=> If you save all error-trails, you have to copy the one you are\
interested in inspecting with a guided simulation onto the file\
pan_in.trail manually (outside xspin) after the run completes.\
The trails are numbered in order of discovery."

	button .road2.b -text "Ok" -command {destroy .road2}
	pack append .road2 .road2.z {top expand fill}
	pack append .road2 .road2.b {top}
	.road2.z.t configure -state disabled 
	.road2.z.t yview -pickplace 1.0      
	focus .road2.z.t
}

proc roadmap2e {} {
	global FG BG

	catch {destroy .road2}
	toplevel .road2

	wm title .road2 "Help with Verification"
	wm iconname .road2 "ValHelp"
	frame .road2.z
	scrollbar .road2.z.s -command ".road2.z.t yview"
	text .road2.z.t -relief raised -bd 2 \
		-background $BG -foreground $FG \
		-yscrollcommand ".road2.z.s set" \
		-setgrid 1 -width 60 -height 25 -wrap word
	pack append .road2.z \
		.road2.z.s {left filly} \
		.road2.z.t {left expand fill}
	.road2.z.t insert end "BASIC GUIDELINES:
When just starting out, it is safe to leave all parameters\
at their initial value and to push the Run button for a\
default exhaustive verification.\
If you run out of memory, adjust the parameter settings\
under Advanced Options.

=> Safety properties are properties of single states (like\
deadlocks = invalid endstates, or assertion violations).

=> Liveness properties are properties of sequences of\
states (typically: infinite sequences, i.e., cycles).\
There are two types of cycles: non-progress (not passing\
through any state marked with a 'progress' label) and\
acceptance (passing infinitely often through a state\
marked with an 'accept' label).

=> Use the Weak Fairness option only when really necessary,\
to avoid unwated error reports.  It can increase the CPU-time\
requirements by a factor roughly equal to twice the number of\
active processes.

=> It is safe to leave the Reduced Search option enabled.\
Turn it off only for debugging purposes, or when warned to do so by the \
verifier itself.   The Profiling option gathers statistics about the \
verification hot-spots in the model.

=> You can apply a Never Claim even when checking Safety Properties\
when you want to restrict the search to the sequences that are\
matched by the claim (a user-guided search pruning technique)."

	button .road2.b -text "Ok" -command {destroy .road2}
	pack append .road2 .road2.z {top expand fill}
	pack append .road2 .road2.b {top}
	.road2.z.t configure -state disabled 
	.road2.z.t yview -pickplace 1.0      
	focus .road2.z.t
}

proc roadmap2f {} {
	global FG BG

	catch {destroy .road2}
	toplevel .road2

	wm title .road2 "Help with Verification"
	wm iconname .road2 "ValHelp"
	frame .road2.z
	scrollbar .road2.z.s -command ".road2.z.t yview"
	text .road2.z.t -relief raised -bd 2 \
		-background $BG -foreground $FG \
		-yscrollcommand ".road2.z.s set" \
		-setgrid 1 -width 60 -height 15 -wrap word
	pack append .road2.z \
		.road2.z.s {left filly} \
		.road2.z.t {left expand fill}
	.road2.z.t insert end "GUIDELINES:
This will run a verification for the specific LTL property\
that was defined in the LTL options panel that brought you\
here.  The claim was placed in a separate .ltl\
file, not included in the main specification.\
(It will be picked up in the verification automatically.)\
The separate .ltl file combines the notes, formula,\
macros, results, etc., for easier tracking.

On a first run, leave all choices at their initial\
value and push the Run button for a default verification.\
If you run out of memory, adjust the parameter settings\
under Advanced Options.

Use the Weak Fairness option only when really necessary,\
to avoid unwated error reports.  It can increase the CPU-time\
requirements by a factor roughly equal to twice the number of\
active processes."

	button .road2.b -text "Ok" -command {destroy .road2}
	pack append .road2 .road2.z {top expand fill}
	pack append .road2 .road2.b {top}
	.road2.z.t configure -state disabled 
	.road2.z.t yview -pickplace 1.0      
	focus .road2.z.t
}

proc roadmap2 {} {
	global FG BG

	catch {destroy .road2}
	toplevel .road2

	wm title .road2 "Help with Verification"
	wm iconname .road2 "ValHelp"
	frame .road2.z
	scrollbar .road2.z.s -command ".road2.z.t yview"
	text .road2.z.t -relief raised -bd 2 \
		-background $BG -foreground $FG \
		-yscrollcommand ".road2.z.s set" \
		-setgrid 1 -width 60 -height 20 -wrap word
	pack append .road2.z \
		.road2.z.s {left filly} \
		.road2.z.t {left expand fill}
	.road2.z.t insert end "GUIDELINES:
When just starting out, it is safe to leave all
verification parameters set at their initial values
and to Run a default verification.
If you run out of memory, or encounter other problems,
look at the specific help options in the verification
settings panel.
One parameter is important to set correctly right from
the start: the physical memory size of your system.
It is by default set to 64 Mbytes.  Set it once to the
true amount of physical memory on your system, in Megabytes,
and never change it again (unless you buy more physical
memory for your machine of course).
You can find this parameter under advanced options in the
verification parameters panel.
Bitstate/Supertrace verifications are approximate, and
only used for models too large to verify exhaustively.
This option allows you to get at least an approximate
answer to the correctness of models that could otherwise
not be verified by a finite state system."

	button .road2.b -text "Ok" -command {destroy .road2}
	pack append .road2 .road2.z {top expand fill}
	pack append .road2 .road2.b {top}
	.road2.z.t configure -state disabled 
	.road2.z.t yview -pickplace 1.0      
	focus .road2.z.t
}

proc roadmap3 {} {
	global FG BG

	catch {destroy .road3}
	toplevel .road3

	wm title .road3 "Reducing Complexity"
	wm iconname .road3 "CompHelp"
	frame .road3.z
	scrollbar .road3.z.s -command ".road3.z.t yview"
	text .road3.z.t -relief raised -bd 2 \
		-background $BG -foreground $FG \
		-yscrollcommand ".road3.z.s set" \
		-setgrid 1 -width 60 -height 30 -wrap word
	pack append .road3.z \
		.road3.z.s {left filly} \
		.road3.z.t {left expand fill}
	.road3.z.t insert end "
When a verification cannot be completed because of\
computational complexity; here are some strategies that\
can be applied to combat this problem.

0. Run the Slicing Algorithm (in the Run Menu) to find\
potential redundancy in your model for the stated properties.

1. Try to make the model more general, more abstract.\
Remember that you are constructing a verification model and not\
an implementation.  SPIN's strength is in proving properties of\
*interactions* in a distributed system (the implicit assumptions\
that processes make about each other) -- it's strength is not in\
proving things about local *computations*, data dependencies etc.

2. Remove everything that is not directly related to the property\
you are trying to prove: redundant computations, redundant data. \
*Avoid counters*; avoid incrementing variables that are used for\
only book-keeping purposes.
The Syntax Check option will warn about the gravest offenses.

3. Asynchronous channels are a significant source of complexity in\
verification.  Use a synchronous channel where possible.  Reduce the\
number of slots in asynchronous channels to a minimum (use 2, or 3\
slots to get started).

4. Look for processes that merely transfer messages. Consider if\
you can remove processes that only copy incoming messages from\
one channel into another, by letting the sender generate the\
final message right away.  If the intermediate process makes\
choices (e.g., to delete or duplicate, etc.), let the sender\
make that choice, rather than the intermediate process.

5. Combine local computations into atomic, or d_step, sequences.

6. Avoid leaving scratch data around in variables.  You can reduce\
the number of states by, for instance, resetting local variables\
that are used inside atomic sequences to zero at the end of those\
sequences; so that the scratch values aren't visible outside the\
sequence.  Alternatively: introduce some extra global 'hidden'\
variables for these purposes (see the WhatsNew.html document).
Use the predefined variable \"_\" as a write-only scratch variable\
wherever possible.

7. If possible to do so: combine the behavior of two processes into\
a single one.  Generalize behavior;  focus on coordination aspects\
(i.e., the interfaces between processes, rather than the local\
computation inside processes).

8. Try to exploit the partial order reduction strategies.\
Use the xr and xs assertions (see WhatsNew.html); avoid sharing\
channels between multiple receivers or multiple senders.\
Avoid merging independent data-streams into a single shared channel."

	button .road3.b -text "Ok" -command {destroy .road3}
	pack append .road3 .road3.z {top expand fill}
	pack append .road3 .road3.b {top}
	.road3.z.t configure -state disabled 
	.road3.z.t yview -pickplace 1.0      
	focus .road3.z.t
}

proc roadmap5 {} {
	global FG BG

	catch {destroy .road5}
	toplevel .road5

	wm title .road5 "Spin Automata"
	wm iconname .road5 "FsmHelp"
	frame .road5.z
	scrollbar .road5.z.s -command ".road5.z.t yview"
	text .road5.z.t -relief raised -bd 2 \
		-background $BG -foreground $FG \
		-yscrollcommand ".road5.z.s set" \
		-setgrid 1 -width 60 -height 30 -wrap word
	pack append .road5.z \
		.road5.z.s {left filly} \
		.road5.z.t {left expand fill}
	.road5.z.t insert end "
The Spin Automata view option give a view of the
structure of the automata models that Spin uses in
the verification process.
Each proctype is represented by a unique automaton.

Chosing this option (in the Run menu) will cause Spin to
first generate a verifier, compile it, and then run it
(as pan -d) to obtain a description of the proctype
names and the corresponding automata.

After selecting (double-clicking) the proctype name desired,
the graph will be produced.  The default graph layout
algorithm is small and a self-contained part of Xspin,
but also rather crude.  Be on guard, therefore, for edges
that overlap (a typical case, for instance, is a backedge
that hides behind a series of forward edges. Use DOT
(see the README.html file on Spin) when possible for much
better graph layout.

In the default layout, the following button actions are
defined (the first one is not needed when using DOT):

1. Moving Nodes: either Button-1 or Button-2.
2. Displaying Edge Labels: hold Button-1 down on the edge.
3. Cross-References: Move the cursor over a Node to see the
   corresponding line in the Promela source, in the main
   Xspin window.

If labels look bad -- try changing the font definitions at
the start of the xspin.tcl file (hints are given there).
"
	button .road5.b -text "Ok" -command {destroy .road5}
	pack append .road5 .road5.z {top expand fill}
	pack append .road5 .road5.b {top}
	.road5.z.t configure -state disabled 
	.road5.z.t yview -pickplace 1.0      
	focus .road5.z.t
}

proc roadmap6 {} {
	global FG BG

	catch {destroy .road6}
	toplevel .road6

	wm title .road6 "Optional Compiler Directives"
	wm iconname .road6 "Optional"
	frame .road6.z
	scrollbar .road6.z.s -command ".road6.z.t yview"
	text .road6.z.t -relief raised -bd 2 \
		-background $BG -foreground $FG \
		-yscrollcommand ".road6.z.s set" \
		-setgrid 1 -width 80 -height 30 -wrap word
	pack append .road6.z \
		.road6.z.s {left filly} \
		.road6.z.t {left expand fill}
	.road6.z.t insert end "
		Use only when prompted:

NFAIR=N		size memory used for enforcing weak fairness (default N=2)
VECTORSZ=N	allocates memory (in bytes) for state vector (default N=1024)

		Related to partial order reduction:

CTL		limit p.o.reduction to subset consistent with branching time logic
GLOB_ALPHA	consider process death a global action
XUSAFE		disable validity checks of xr/xs assertions

		Speedups:

NOBOUNDCHECK	don't check array bound violations
NOCOMP		don't compress states with fullstate storage (uses more memory)
NOSTUTTER	disable stuttering rules (warning: changes semantics)

		Memory saving (slower):

MA=N		use a minimized DFA encoding for state vectors up to N bytes

		Experimental:

BCOMP		when in BITSTATE mode, computes hash over compressed state-vector
NIBIS		apply a small optimization of partial order reduction
NOVSZ		risky - removes 4 bytes from state vector - its length field.
PRINTF		enables printfs during verification runs
RANDSTORE=N	in BITSTATE mode, -DRANDSTORE=33 lowers prob of storing a state to 33%
W_XPT=N		with MA, write checkpoint files every multiple of N states stored
R_XPT		with MA, restart run from last checkpoint file written

		Debugging:

SDUMP		with CHECK: adds ascii dumps of state vectors
SVDUMP		add run option -pN to write N-byte state vectors into file sv_dump

		Already set by the other xspin options:

BITSTATE	use supertrace/bitstate instead of exhaustive exploration
HC		use hash-compact instead of exhaustive exploration
COLLAPSE	collapses state vector size by up to 80% to 90%
MEMCNT=N	set upperbound of 2^N bytes to memory that can be allocated
MEMLIM=N	set upperbound of N Mbytes to memory that can be allocated
NOCLAIM		exclude never claim from the verification, if present
NOFAIR		disable the code for weak-fairness (is faster)
NOREDUCE	disables the partial order reduction algorithm
NP		enable non-progress cycle detection (option -l, replacing -a),
PEG		add complexity profiling (transition counts)
REACH		guarantee absence of errors within the -m depth-limit
SAFETY		optimize for the case where no cycle detection is needed
VAR_RANGES	compute the effective value range of byte variables
CHECK		generate debugging information (see also below)
VERBOSE		elaborate debugging printouts
"
	button .road6.b -text "Ok" -command {destroy .road6}
	pack append .road6 .road6.z {top expand fill}
	pack append .road6 .road6.b {top}
	.road6.z.t configure -state disabled 
	.road6.z.t yview -pickplace 1.0      
	focus .road6.z.t
}


# simulation options panel

set s_options	""
set v_options	""
set a_options	""
set c_options	""

set Blue	"blue";		#"yellow"
set Yellow	"yellow";	#"red"
set White	"white";	#"yellow"
set Red		"red";		#"yellow"
set Green	"green";	#"green"

set fd		0
set Depth	0
set Seq(0)	0
set Sdbox	0
set Spbox(0)	0
set sbox	0

set simruns	0
set stepper	0
set stepped	0
set VERBOSE	0
set SYMBOLIC	0
set howmany	0
set Choice(1)	0
set Sticky(0)	0
set SparseMsc	1
set showvars	0
set vv		1
set qv		1
set gvars	1
set lvars	0
set hide_q1	""
set hide_q2	""
set hide_q3	""
set PlaceSim	"+100+100"

proc simulation_old {} {
	global s_typ l_typ showvars qv PlaceSim
	global fvars gvars lvars SparseMsc HelvBig
	global msc ebc tsc vv svars rvars seed jumpsteps
	global hide_q1 hide_q2 hide_q3

	.menu.run.m entryconfigure 5 -state normal

	catch {destroy .s}
	toplevel .s
	set k [string first "\+" $PlaceSim]
	if {$k > 0} {
		set PlaceSim [string range $PlaceSim $k end]
	}

	wm title .s "Simulation Options"
	wm iconname .s "SIM"
	wm geometry .s $PlaceSim

	frame .s.opt -relief flat

	mkpan_in

	frame .s.opt.mode -relief raised -borderwidth 1m
	label .s.opt.mode.fld0 \
		-font $HelvBig \
		-text "Display Mode" \
		-relief sunken -borderwidth 1m

	checkbutton .s.opt.mode.fld4b -text "Time Sequence Panel - with:" \
		-variable tsc \
		-relief flat
	frame .s.opt.mode.flds
	radiobutton .s.opt.mode.flds.fld3 \
		-text "    Interleaved Steps" \
		-variable m_typ -value 2 \
		-relief flat
	radiobutton .s.opt.mode.flds.fld1 \
		-text "    One Window per Process" \
		-variable m_typ -value 0 \
		-relief flat
	radiobutton .s.opt.mode.flds.fld2 \
		-text "    One Trace per Process" \
		-variable m_typ -value 1 \
		-relief flat
	frame .s.opt.mode.flds.fld0 -width 15
	pack append .s.opt.mode.flds \
		.s.opt.mode.flds.fld0 {left frame w}\
		.s.opt.mode.flds.fld3 {top frame w}\
		.s.opt.mode.flds.fld1 {top frame w}\
		.s.opt.mode.flds.fld2 {top frame w}

	checkbutton .s.opt.mode.fld4a -text "MSC Panel - with:" \
		-variable msc \
		-relief flat
	frame .s.opt.mode.steps
	radiobutton .s.opt.mode.steps.fld5 -text "    Step Number Labels" \
		-variable SYMBOLIC -value 0 \
		-relief flat
	radiobutton .s.opt.mode.steps.fld6 -text "    Source Text Labels" \
		-variable SYMBOLIC -value 1 \
		-relief flat
	radiobutton .s.opt.mode.steps.fld7 -text "    Normal Spacing" \
		-variable SparseMsc -value 1 \
		-relief flat
	radiobutton .s.opt.mode.steps.fld8 -text "    Condensed Spacing" \
		-variable SparseMsc -value 0 \
		-relief flat
	frame .s.opt.mode.steps.fld0 -width 15
	pack append .s.opt.mode.steps \
		.s.opt.mode.steps.fld0 {left frame w}\
		.s.opt.mode.steps.fld5 {top frame w}\
		.s.opt.mode.steps.fld6 {top frame w}\
		.s.opt.mode.steps.fld7 {top frame w}\
		.s.opt.mode.steps.fld8 {top frame w}

	checkbutton .s.opt.mode.fld4c -text "Execution Bar Panel" \
		-variable ebc \
		-relief flat
	checkbutton .s.opt.mode.fld4d -text "Data Values Panel" \
		-variable vv \
		-relief flat

	frame .s.opt.mode.vars

	checkbutton .s.opt.mode.vars.fld4c -text "    Track Buffered Channels" \
		-variable qv \
		-relief flat
	checkbutton .s.opt.mode.vars.fld4d -text "    Track Global Variables" \
		-variable gvars \
		-relief flat
	checkbutton .s.opt.mode.vars.fld4e -text "    Track Local Variables" \
		-variable lvars \
		-relief flat

	checkbutton .s.opt.mode.vars.fld4f \
		-text "    Display vars marked 'show' in MSC" \
		-variable showvars \
		-relief flat
	frame .s.opt.mode.vars.fld0 -width 15
	pack append .s.opt.mode.vars \
		.s.opt.mode.vars.fld0 {left frame w}\
		.s.opt.mode.vars.fld4c {top frame w}\
		.s.opt.mode.vars.fld4d {top frame w}\
		.s.opt.mode.vars.fld4e {top frame w}\
		.s.opt.mode.vars.fld4f {top frame w}

	pack append .s.opt.mode .s.opt.mode.fld0 {top pady 4 frame w fillx}

	pack append .s.opt.mode .s.opt.mode.fld4a {top pady 4 frame w}
	pack append .s.opt.mode .s.opt.mode.steps {top frame w}

	pack append .s.opt.mode .s.opt.mode.fld4b {top pady 4 frame w}
	pack append .s.opt.mode .s.opt.mode.flds  {top frame w}

	pack append .s.opt.mode .s.opt.mode.fld4d {top pady 4 frame w}
	pack append .s.opt.mode .s.opt.mode.vars {top frame w}

	pack append .s.opt.mode .s.opt.mode.fld4c {top pady 4 frame w}

	pack append .s.opt .s.opt.mode {left frame n}

	frame .s.opt.mesg -relief raised -borderwidth 1m
	label .s.opt.mesg.loss0 \
		-font $HelvBig \
		-text "A Full Queue" \
		-relief sunken -borderwidth 1m
	radiobutton .s.opt.mesg.loss1 -text "Blocks New Msgs" \
		-variable l_typ -value 0 \
		-relief flat
	radiobutton .s.opt.mesg.loss2 -text "Loses New Msgs" \
		-variable l_typ -value 1 \
		-relief flat
	pack append .s.opt.mesg .s.opt.mesg.loss0 {top pady 4 frame w fillx}
	pack append .s.opt.mesg .s.opt.mesg.loss1 {top pady 4 frame w}
	pack append .s.opt.mesg .s.opt.mesg.loss2 {top pady 4 frame w}

	frame .s.opt.hide -relief raised -borderwidth 1m
	label .s.opt.hide.txt  \
		-font $HelvBig \
		-text "Hide Queues in MSC" \
		-relief sunken -borderwidth 1m
	pack append .s.opt.hide .s.opt.hide.txt {top pady 4 frame w fillx }

	for {set i 1} {$i < 4} {incr i} {
		frame .s.opt.hide.q$i
		label .s.opt.hide.q$i.qno \
			-font $HelvBig \
			-text "Queue nr:"
		entry .s.opt.hide.q$i.entry \
			-relief sunken -width 8
		pack append .s.opt.hide.q$i .s.opt.hide.q$i.qno {left pady 4 frame n }
		pack append .s.opt.hide.q$i .s.opt.hide.q$i.entry {left pady 4 frame n}
		pack append .s.opt.hide .s.opt.hide.q$i {top pady 4 frame w fillx}
	}
	frame .s.opt.lframe -relief raised -borderwidth 1m
	label .s.opt.lframe.tl \
		-font $HelvBig \
		-text "Simulation Style" \
		-relief sunken -borderwidth 1m
	radiobutton .s.opt.lframe.is -text "Interactive" \
		-variable s_typ -value 2 \
		-relief flat
	radiobutton .s.opt.lframe.gs -text "Guided (using pan.trail)" \
		-variable s_typ -value 1 \
		-relief flat
	frame .s.opt.lframe.b
	entry .s.opt.lframe.b.entry -relief sunken -width 8 
	label .s.opt.lframe.b.label \
		-font $HelvBig \
		-text "Steps Skipped"
	pack append .s.opt.lframe.b \
		.s.opt.lframe.b.label {left} \
		.s.opt.lframe.b.entry {left}

	radiobutton .s.opt.lframe.rs -text "Random (using seed)" \
		-variable s_typ -value 0 \
		-relief flat
	frame .s.opt.lframe.s
	entry .s.opt.lframe.s.entry -relief sunken -width 8 
	label .s.opt.lframe.s.label \
		-font $HelvBig \
		-text "Seed Value"
	pack append .s.opt.lframe.s \
		.s.opt.lframe.s.label {left} \
		.s.opt.lframe.s.entry {left}

	pack append .s.opt.lframe .s.opt.lframe.tl {top pady 4 frame w fillx} \
		.s.opt.lframe.rs {top pady 4 frame w} \
		.s.opt.lframe.s  {top pady 4 frame e} \
		.s.opt.lframe.gs {top pady 4 frame w} \
		.s.opt.lframe.b  {top pady 4 frame e} \
		.s.opt.lframe.is {top pady 4 frame w}

	pack append .s.opt .s.opt.lframe {top frame n}
	pack append .s.opt .s.opt.mesg {top frame n fillx}
	pack append .s.opt .s.opt.hide {top frame n expand fillx filly}

	pack append .s .s.opt { top frame n }

	pack append .s [button .s.rewind -text "Start" \
		-command "Rewind"  ] {right frame e}
	pack append .s [button .s.exit -text "Cancel" \
		-command "Stopsim" ] {right frame e}
	pack append .s [button .s.help -text "Help" -fg red \
		-command "roadmap1" ] {right frame e}

	.s.opt.lframe.s.entry  insert end $seed
	.s.opt.lframe.b.entry insert end $jumpsteps

	.s.opt.hide.q1.entry insert end $hide_q1
	.s.opt.hide.q2.entry insert end $hide_q2
	.s.opt.hide.q3.entry insert end $hide_q3
}


proc simulation {} {
	global s_typ l_typ showvars qv PlaceSim
	global fvars gvars lvars SparseMsc HelvBig
	global msc ebc tsc vv svars rvars seed jumpsteps
	global hide_q1 hide_q2 hide_q3
	global whichsim

	.menu.run.m entryconfigure 5 -state normal

	catch {destroy .s}
	toplevel .s
		catch {rmfile pan_in9999999.trail}
		debug {about to remove pan_in9999999.trail}
		rmfile pan_in9999999.trail
	set k [string first "\+" $PlaceSim]
	if {$k > 0} {
		set PlaceSim [string range $PlaceSim $k end]
	}

	wm title .s "Simulation Options"
	wm iconname .s "SIM"
	wm geometry .s $PlaceSim

	mkpan_in

	# lower frame with 'start', 'cancel' and 'help' buttons
	frame .s.l -relief flat
	pack .s.l -side bottom -fill both

	  pack [button .s.l.rewind -text " Start " \
		-command "Rewind"  ] -side right -fill y -padx 4
	  pack [button .s.l.exit -text "Cancel" \
		-command "
			Stopsim;
			catch {rmfile pan_in9999999.trail}
			"
		] -side right -fill y -padx 4
	  pack [button .s.l.help -text " Help " -fg red \
		-command "roadmap1" ]  -side right -fill y -padx 4

	# upper frame with modes and options
	frame .s.u -relief flat
	pack .s.u -side top -fill both

	  frame .s.u.mode -relief raised -borderwidth 1m
	  pack .s.u.mode -side left -fill both -expand 1

	    frame .s.u.mode.fdis -relief flat
	    pack .s.u.mode.fdis -side top -fill x -expand 1

	      label .s.u.mode.fdis.fld0 \
		-font $HelvBig \
		-text "Display Mode" \
		-relief sunken -borderwidth 1m
	      pack .s.u.mode.fdis.fld0 -side top -fill x

#MSC Panel

	    frame .s.u.mode.fmsc -relief flat
	    pack  .s.u.mode.fmsc -side top -fill x

	      checkbutton .s.u.mode.fmsc.fld4a -text "MSC Panel - with:" \
		  -variable msc \
		  -relief flat
	      pack .s.u.mode.fmsc.fld4a -side left

	    frame .s.u.mode.msc -relief flat
	    pack  .s.u.mode.msc -side top -fill x

	      frame .s.u.mode.msc.lab -relief flat
	      pack  .s.u.mode.msc.lab -side top -fill x

	        frame .s.u.mode.msc.lab.dummy -width 18 -relief flat
	        pack .s.u.mode.msc.lab.dummy -side left -fill y

		frame .s.u.mode.msc.lab.radios -relief flat
		pack .s.u.mode.msc.lab.radios -side left -fill x
	
		  frame .s.u.mode.msc.lab.radios.fnum -relief flat
		  pack .s.u.mode.msc.lab.radios.fnum -side top -fill x

		    radiobutton .s.u.mode.msc.lab.radios.fnum.fld5 \
			  -text "    Step Number Labels" \
		  	  -variable SYMBOLIC -value 0 \
		  	  -relief flat
		    pack .s.u.mode.msc.lab.radios.fnum.fld5 -side left

		  frame .s.u.mode.msc.lab.radios.ftext -relief flat
		  pack .s.u.mode.msc.lab.radios.ftext -side top -fill x

		    radiobutton .s.u.mode.msc.lab.radios.ftext.fld6 \
			-text "    Source Text Labels" \
			-variable SYMBOLIC -value 1 \
		  	-relief flat
		    pack .s.u.mode.msc.lab.radios.ftext.fld6 -side left

		frame .s.u.mode.msc.lab.bracket
		pack .s.u.mode.msc.lab.bracket -side left -fill y
		
		  canvas .s.u.mode.msc.lab.bracket.c -width 10 -height 40
		  pack .s.u.mode.msc.lab.bracket.c -side top
		    .s.u.mode.msc.lab.bracket.c create line 5 15 10 15 10 38 5 38

	      frame .s.u.mode.msc.space -relief flat
	      pack  .s.u.mode.msc.space -side top -fill x

	        frame .s.u.mode.msc.space.dummy -width 18 -relief flat
	        pack .s.u.mode.msc.space.dummy -side left -fill y

		frame .s.u.mode.msc.space.radios -relief flat
		pack  .s.u.mode.msc.space.radios -side left -fill x
	
		  frame .s.u.mode.msc.space.radios.fnorm -relief flat
		  pack  .s.u.mode.msc.space.radios.fnorm -side top -fill x

		    radiobutton .s.u.mode.msc.space.radios.fnorm.fld7 \
			-text "    Normal Spacing" \
			-variable SparseMsc -value 1 \
			-relief flat
		    pack .s.u.mode.msc.space.radios.fnorm.fld7 -side left

	  	  frame .s.u.mode.msc.space.radios.fcond -relief flat
		  pack  .s.u.mode.msc.space.radios.fcond -side top -fill x

		    radiobutton .s.u.mode.msc.space.radios.fcond.fld8 \
			-text "    Condensed Spacing" \
			-variable SparseMsc -value 0 \
			-relief flat
		    pack .s.u.mode.msc.space.radios.fcond.fld8 -side left

		frame .s.u.mode.msc.space.bracket
		pack .s.u.mode.msc.space.bracket -side left -fill y
		
		  canvas .s.u.mode.msc.space.bracket.c -width 10 -height 40
		  pack .s.u.mode.msc.space.bracket.c -side top
		    .s.u.mode.msc.space.bracket.c create line 5 15 10 15 10 38 5 38

# Time Sequence Panel

	    frame .s.u.mode.ftsp -relief flat 
	    pack  .s.u.mode.ftsp -side top -fill x

	      checkbutton .s.u.mode.ftsp.fld4b \
		-text "Time Sequence Panel - with:" \
		-variable tsc \
		-relief flat
	      pack .s.u.mode.ftsp.fld4b -side left

	    frame .s.u.mode.tsp
	    pack  .s.u.mode.tsp -side top -fill x

	      frame .s.u.mode.tsp.proc
	      pack  .s.u.mode.tsp.proc -side top -fill x

		frame .s.u.mode.tsp.proc.dummy -width 18
		pack  .s.u.mode.tsp.proc.dummy -side left -fill y

		frame .s.u.mode.tsp.proc.radios -relief flat
	        pack  .s.u.mode.tsp.proc.radios -side left -fill y

	          frame .s.u.mode.tsp.proc.radios.is
	          pack  .s.u.mode.tsp.proc.radios.is -side top -fill x

		    radiobutton .s.u.mode.tsp.proc.radios.is.fld3 \
			    -text "    Interleaved Steps" \
			    -variable m_typ -value 2 \
		  	    -relief flat
		    pack .s.u.mode.tsp.proc.radios.is.fld3 -side left

		  frame .s.u.mode.tsp.proc.radios.1win -relief flat
		  pack .s.u.mode.tsp.proc.radios.1win -side top -fill x

		    radiobutton .s.u.mode.tsp.proc.radios.1win.fld1 \
			-text "    One Window per Process" \
			-variable m_typ -value 0 \
			-relief flat
		    pack .s.u.mode.tsp.proc.radios.1win.fld1 -side left

		  frame .s.u.mode.tsp.proc.radios.1trace -relief flat
		  pack  .s.u.mode.tsp.proc.radios.1trace -side top -fill x

		    radiobutton .s.u.mode.tsp.proc.radios.1trace.fld2 \
			-text "    One Trace per Process" \
			-variable m_typ -value 1 \
			-relief flat
		    pack .s.u.mode.tsp.proc.radios.1trace.fld2 -side left

		frame .s.u.mode.tsp.proc.bracket
		pack .s.u.mode.tsp.proc.bracket -side left -fill y

		set y 13
		  canvas .s.u.mode.tsp.proc.bracket.c -width 10 -height 66
		  pack .s.u.mode.tsp.proc.bracket.c -side top
		    .s.u.mode.tsp.proc.bracket.c create line    5  [expr 0 + $y] \
								10 [expr 0 + $y] \
								10 [expr 25 + $y] \
								5  [expr 25 + $y] \
								10 [expr 25 + $y] \
								10 [expr 50 + $y] \
								5  [expr 50 + $y]

	frame .s.u.mode.fdvp -relief flat
	pack .s.u.mode.fdvp -side top -fill x

	  checkbutton .s.u.mode.fdvp.fld4d -text "Data Values Panel" \
		-variable vv \
		-relief flat
	  pack .s.u.mode.fdvp.fld4d -side left

	frame .s.u.mode.vars
	pack .s.u.mode.vars -side top -fill x

	  frame .s.u.mode.vars.dummy -width 18
	  pack .s.u.mode.vars.dummy -side left -fill y

	  frame .s.u.mode.vars.chks -relief flat
	  pack  .s.u.mode.vars.chks -side left -fill y
	    
	    frame .s.u.mode.vars.chks.ftbc
	    pack  .s.u.mode.vars.chks.ftbc -side top -fill x

	      checkbutton .s.u.mode.vars.chks.ftbc.fld4c -text "    Track Buffered Channels" \
		-variable qv \
		-relief flat
	      pack .s.u.mode.vars.chks.ftbc.fld4c -side left

	    frame .s.u.mode.vars.chks.ftgv
	    pack  .s.u.mode.vars.chks.ftgv -side top -fill x

	      checkbutton .s.u.mode.vars.chks.ftgv.fld4d -text "    Track Global Variables" \
		-variable gvars \
		-relief flat
	      pack .s.u.mode.vars.chks.ftgv.fld4d -side left

	    frame .s.u.mode.vars.chks.ftlv
	    pack  .s.u.mode.vars.chks.ftlv -side top -fill x

	      checkbutton .s.u.mode.vars.chks.ftlv.fld4e -text "    Track Local Variables" \
		-variable lvars \
		-relief flat
	      pack .s.u.mode.vars.chks.ftlv.fld4e -side left

	    frame .s.u.mode.vars.chks.fshow
	    pack  .s.u.mode.vars.chks.fshow -side top -fill x

	      checkbutton .s.u.mode.vars.chks.fshow.fld4f \
		-text "    Display vars marked 'show' in MSC" \
		-variable showvars \
		-relief flat

	      pack .s.u.mode.vars.chks.fshow.fld4f -side left

	frame .s.u.mode.fexecbar -relief flat
	pack .s.u.mode.fexecbar -side top -fill x

	  checkbutton .s.u.mode.fexecbar.fld4c -text "Execution Bar Panel" \
		-variable ebc \
		-relief flat
          pack .s.u.mode.fexecbar.fld4c -side left

#Right upper frame
	frame .s.u.r -relief flat
	pack .s.u.r -side right -fill y -expand 1

#Simulation Style
	  frame .s.u.r.sim -relief raised -borderwidth 1m
	  pack .s.u.r.sim -side top -fill both -expand 1

	    frame .s.u.r.sim.flab -relief sunken
	    pack .s.u.r.sim.flab -side top -fill x

	      label .s.u.r.sim.flab.tl \
		-font $HelvBig \
		-text "Simulation Style" \
		-relief sunken -borderwidth 1m
	      pack .s.u.r.sim.flab.tl -side top -fill x

	    frame .s.u.r.sim.random
	    pack .s.u.r.sim.random -side top -fill x

	   	radiobutton .s.u.r.sim.random.rs -text "Random (using seed)" \
		-variable s_typ -value 0 \
		-relief flat \
		-command "enable_disable_sub_buttons"
		pack .s.u.r.sim.random.rs -side left

	    frame .s.u.r.sim.seedvalue
	    pack .s.u.r.sim.seedvalue -side top -fill x

	      frame .s.u.r.sim.seedvalue.dummy -width 18
	      pack .s.u.r.sim.seedvalue.dummy -side left -fill y

	      label .s.u.r.sim.seedvalue.label \
		-font $HelvBig \
		-text "Seed Value"
	      pack .s.u.r.sim.seedvalue.label -side left

	      entry .s.u.r.sim.seedvalue.entry -relief sunken -width 8
	      pack .s.u.r.sim.seedvalue.entry -side left

	    frame .s.u.r.sim.guided
	    pack .s.u.r.sim.guided -side top -fill x

		radiobutton .s.u.r.sim.guided.gs -text "Guided" \
		   -variable s_typ -value 1 \
		   -relief flat \
		   -command "enable_disable_sub_buttons"
		pack .s.u.r.sim.guided.gs -side left
		
		frame .s.u.r.sim.guided_type
		pack .s.u.r.sim.guided_type -side top -fill x

		  frame .s.u.r.sim.guided_type.dummy -width 18
		  pack .s.u.r.sim.guided_type.dummy -side left -fill y

		    frame .s.u.r.sim.guided_type.radios
		    pack .s.u.r.sim.guided_type.radios -side left

		      frame .s.u.r.sim.guided_type.radios.pan_trail
		      pack  .s.u.r.sim.guided_type.radios.pan_trail -side top -fill x

			radiobutton .s.u.r.sim.guided_type.radios.pan_trail.rb \
				-text "Using pan_in.trail" \
				-variable whichsim -value 0 \
				-relief flat
			pack .s.u.r.sim.guided_type.radios.pan_trail.rb -side left

		      frame .s.u.r.sim.guided_type.radios.trail_other
		      pack  .s.u.r.sim.guided_type.radios.trail_other -side top -fill x

			radiobutton .s.u.r.sim.guided_type.radios.trail_other.rb \
				-text "Use" \
				-variable whichsim -value 1 \
				-relief flat
		        pack .s.u.r.sim.guided_type.radios.trail_other.rb -side left

			entry .s.u.r.sim.guided_type.radios.trail_other.entry \
				-width 20
		        pack .s.u.r.sim.guided_type.radios.trail_other.entry -side left

			button .s.u.r.sim.guided_type.radios.trail_other.button -text "Browse" \
				-command select_trail_file
		        pack .s.u.r.sim.guided_type.radios.trail_other.button -side left	  

 	    frame .s.u.r.sim.skipstep
	    pack  .s.u.r.sim.skipstep -side top -fill x

	      label .s.u.r.sim.skipstep.label \
		-font $HelvBig \
		-text "Steps Skipped"
	      pack .s.u.r.sim.skipstep.label -side left

	      entry .s.u.r.sim.skipstep.entry -relief sunken -width 8
	      pack .s.u.r.sim.skipstep.entry -side left

	    frame .s.u.r.sim.interactive
	    pack .s.u.r.sim.interactive -side top -fill x

 		radiobutton .s.u.r.sim.interactive.is -text "Interactive" \
			-variable s_typ -value 2 \
			-relief flat \
		-command "enable_disable_sub_buttons"
	        pack .s.u.r.sim.interactive.is -side left

#A Full Queue
	  frame .s.u.r.fq -relief raised -borderwidth 1m
	  pack .s.u.r.fq -side top -fill both -expand 1

	    frame .s.u.r.fq.label -relief sunken
	    pack .s.u.r.fq.label -side top -fill x

	      label .s.u.r.fq.label.loss0 \
		-font $HelvBig \
		-text "A Full Queue" \
		-relief sunken -borderwidth 1m
	      pack .s.u.r.fq.label.loss0 -side top -fill x

	    frame .s.u.r.fq.block
	    pack .s.u.r.fq.block -side top -fill x

	      radiobutton .s.u.r.fq.block.loss1 -text "Blocks New Msgs" \
		-variable l_typ -value 0 \
		-relief flat
	      pack .s.u.r.fq.block.loss1 -side left

	    frame .s.u.r.fq.lose
	    pack .s.u.r.fq.lose -side top -fill x

	      radiobutton .s.u.r.fq.lose.loss2 -text "Loses New Msgs" \
		-variable l_typ -value 1 \
		-relief flat
	      pack .s.u.r.fq.lose.loss2 -side left

#Hide Queues in MSC
	  frame .s.u.r.hq -relief raised -borderwidth 1m
	  pack .s.u.r.hq -side top -fill both -expand 1

	    frame .s.u.r.hq.flabel -relief sunken
	    pack .s.u.r.hq.flabel -side top -fill x

		label .s.u.r.hq.flabel.txt  \
		  -font $HelvBig \
		  -text "Hide Queues in MSC" \
		  -relief sunken -borderwidth 1m
	    pack .s.u.r.hq.flabel.txt -side top -fill x

	for {set i 1} {$i < 4} {incr i} {
		frame .s.u.r.hq.q$i
		pack .s.u.r.hq.q$i -side top -fill x
		label .s.u.r.hq.q$i.qno \
			-font $HelvBig \
			-text "Queue nr:"
		pack .s.u.r.hq.q$i.qno -side left
		entry .s.u.r.hq.q$i.entry \
			-relief sunken -width 8
		pack .s.u.r.hq.q$i.entry -side left
	}




	.s.u.r.sim.seedvalue.entry insert end $seed
	.s.u.r.sim.skipstep.entry insert end $jumpsteps

	.s.u.r.hq.q1.entry insert end $hide_q1
	.s.u.r.hq.q2.entry insert end $hide_q2
	.s.u.r.hq.q3.entry insert end $hide_q3
	enable_disable_sub_buttons
}

proc enable_disable_sub_buttons {} {
	global s_typ
	switch -regexp $s_typ {
		0|2 { .s.u.r.sim.guided_type.radios.pan_trail.rb configure -state disabled
		      .s.u.r.sim.guided_type.radios.trail_other.rb configure -state disabled
		      .s.u.r.sim.guided_type.radios.trail_other.button configure -state disabled
		    }
		1   { .s.u.r.sim.guided_type.radios.pan_trail.rb configure -state normal
		      .s.u.r.sim.guided_type.radios.trail_other.rb configure -state normal
		      .s.u.r.sim.guided_type.radios.trail_other.button configure -state normal
		      .s.u.r.sim.guided_type.radios.pan_trail.rb select
		    }

	}
}

proc select_trail_file {} {
	global Trail_filename
	.s.u.r.sim.guided_type.radios.trail_other.rb select
	# try to use the predefined file selection dialog
	switch [info commands tk_getOpenFile] "" {
		# some old version of Tk so use our own file selection dialog
		set fileselect "FileSelect open"
	} default {
		set fileselect "tk_getOpenFile"
	}
	set init_dir [pwd]
	# get the file (return if the file selection dialog canceled)
	switch -- [set file [eval $fileselect -initialdir { { $init_dir } } ]] "" return
	.s.u.r.sim.guided_type.radios.trail_other.entry insert end $file
	raise .s
	
}

proc bld_s_options {} {
	global fvars gvars lvars svars qv
	global rvars l_typ showvars vv
	global s_typ seed jumpsteps s_options
	global hide_q1 hide_q2 hide_q3 ival whichsim trail_file trail_num

	set s_options "-X -p -v $ival(5)"

	if {$showvars && $gvars == 0 && $lvars == 0} {
		catch { tk_messageBox -icon info \
		-message "Display variables marked 'show' selected, \
		but no local or global vars are being tracked"
	}	}
	if {$showvars==1} { set s_options [format "%s -Y" $s_options] }
	if {$s_typ==2} { set s_options [format "%s -i" $s_options] }
	if {$vv && $gvars} { set s_options [format "%s -g" $s_options] }
	if {$vv && $lvars} { set s_options [format "%s -l" $s_options] }
	if {$svars} { set s_options [format "%s -s" $s_options] }
	if {$rvars} { set s_options [format "%s -r" $s_options] }
	if {$l_typ} { set s_options [format "%s -m" $s_options] }
	if {$hide_q1 != ""} { set s_options [format "%s -q%s" $s_options $hide_q1] }
	if {$hide_q2 != ""} { set s_options [format "%s -q%s" $s_options $hide_q2] }
	if {$hide_q3 != ""} { set s_options [format "%s -q%s" $s_options $hide_q3] }
	if {$s_typ==1} then {
		set trail_num ""
		#Guided
		if {$whichsim == 1} {
			#using user specified file
			if ![file exists $trail_file] {
				catch { tk_messageBox -icon info \
					-message "Trail file $trail_file does not exist."
				}
				return 0
			}
			# see if file is in current directory. if not, copy to 
			# pan_in9999999.trail in current directory
			set ind [string last "\/" $trail_file]
			if {$ind > -1} {
				if {[pwd] != [string range $trail_file 0 [expr $ind - 1]]} { 
					cpfile $trail_file pan_in9999999.trail
					set trail_file "pan_in9999999.trail"
				} else {
					#strip off path
					set trail_file [string range $trail_file \
						[expr $ind + 1] \
						[expr [string length $trail_file] - 1]]
				}
			}	
			#see if it's a 'pan_in<#>.trail' file
			set is_pan_in_trail_file 0
			if {[string range $trail_file 0 5] == "pan_in"} {
				set l [string length $trail_file]

				if {[string range $trail_file \
					[expr $l-6] [expr $l-1]] == ".trail"} {
					set num [string range $trail_file 6 [expr $l-7]]
					if [string is integer $num] {
						set trail_num $num
						set is_pan_in_trail_file 1
			}	}	}
			if !($is_pan_in_trail_file) {
				# not a 'pan_in<#>.trail' file - copy file to pan_in9999999.trail
				# in current directory
				cpfile $trail_file pan_in9999999.trail
				if [file exists pan_in9999999.trail] {
					set trail_num 9999999
				} else {
					catch {tk_messageBox -icon info \
						-message "Unable to create input file in $pwd \
							check write permissions."
					}
					return 0
				}
			}
		} else {
			if {![file exists pan_in.trail] && ![file exists pan_in.tra]} {
				catch { tk_messageBox -icon info \
					-message "Trail file \'pan_in.tra(il)\' does not exist."
				}
				return 0
			}
		}
			
		set s_options [format "%s -t%s" $s_options $trail_num]
	} else {
		if {[string length $seed] > 0} {
			set s_options [format "%s -n%s" $s_options $seed]
	}	}
	if {$s_typ!=2} then {
		if {[string length $jumpsteps] > 0} {
			set s_options [format "%s -j%s" $s_options $jumpsteps]
	}	}
	return 1
}

proc Stopsim {} {
	global stop dbox2 Sticky PlaceSim PlaceCanvas
	global stepper stepped howmany fd

	set stop 1
	set stepped 0
	set stepper 0
	add_log "<stop simulation>"
	if {[winfo exists .s]} {
		set PlaceSim [wm geometry .s]
		destroy .s
	}
	catch {set howmany 0}
	catch {stopbar}
	catch {	if {$Sticky($dbox2) == 0} {
			set PlaceCanvas(msc) [wm geometry .f$dbox2]
			destroy .f$dbox2
	}	}
	catch {
		puts $fd "q"
		flush $fd
	}
	update
}

proc Step_forw {} {
	global stepper stepped sbox simruns PlaceSim

	set stepped 1
	set stepper 1
	if {$simruns == 0} {
		if {[winfo exists .s]} {
			set PlaceSim [wm geometry .s]
			destroy .s
		}
		runsim
	} else {
		catch { .c$sbox.run configure \
		-text "Run" -command "Runsim" }
	}
}

proc Rewind {} {
	global Depth s_typ whichsim trail_file
	global Sdbox Spbox
	global seed jumpsteps simruns
	global hide_q1 hide_q2 hide_q3 trail_file

	catch { set jumpsteps [.s.u.r.sim.skipstep.entry get] }
	catch { set hide_q1 [.s.u.r.hq.q1.entry get] }
	catch { set hide_q2 [.s.u.r.hq.q2.entry get] }
	catch { set hide_q3 [.s.u.r.hq.q3.entry get] }

	if {$s_typ == 0} {
		catch { set seed [.s.u.r.sim.seedvalue.entry get] }
	}
	if {$s_typ == 1} {
		#Guided
		set Depth 0
		catch {
			foreach el [array names Spbox] {
				set Sdbox $Spbox($el)
				.c$Sdbox.z.t tag remove Rev 1.0 end
		}	}
		if {$whichsim == 1} {
			set trail_file ""
			catch {set trail_file [.s.u.r.sim.guided_type.radios.trail_other.entry get]}
		}
	}

	set simruns 0

	Step_forw
}

proc Runsim {} {
	global stepper stepped sbox

	catch { .c$sbox.run configure \
		-text "Suspend" -command "Step_forw" }
	set stepper 1
	set stepped 0
}

proc BreakPoint {} {
	global stepped sbox

	set stepped 1
	catch { .c$sbox.run configure \
		-text "BreakPoint" -command "Runsim" }
}

proc runsim {} {
	global Unix SPIN tk_major
	global s_options s_typ dbox2
	global stepper stepped
	global simruns m_typ
	global gvars lvars
	global fd stop Depth Seq
	global Sdbox Spbox pbox howmany Choice
	global sbox VERBOSE SYMBOLIC msc ebc vv tsc
	global Blue Yellow White Red Green
	global SmallFont BigFont Sticky SparseMsc
	global FG BG qv gvars lvars PlaceBox
	global dbox Vvbox 
	global whichsim trail_num

	set simruns 1
	set Vvbox 0
	set pno 0
	set Varnm("") ""
	set Queues("")	""
	set Depth 0
	set Seq(0) 0
	set Pstp 1
	set Seenpno 1
	set Banner "Select"

#	catch { unset Spbox(0) }
	catch {
		foreach el [array names pbox] {
			catch { destroy .c$pbox($el) }
			catch { unset pbox($el) }
		}
		foreach el [array names Spbox] {
			catch { destroy .c$Spbox($el) }
			catch { unset Spbox($el) }
		}
	}
	if ![bld_s_options] {
		return
	}

	add_log "<starting simulation>"
	add_log "$SPIN $s_options pan_in"
	update
	set s_options [format "%s pan_in" $s_options]

	mkpan_in

	set sbox [mkbox "Simulation Output" "SimOut" "sim.out" 80 10 100 100]

	pack append .c$sbox [button .c$sbox.stepf -text "Single Step" \
		-command "Step_forw" ] {left frame w}
	pack append .c$sbox [button .c$sbox.run -text "Run" \
		-command "Runsim" ] {left frame w}

	.c$sbox.b configure -text "Cancel" -command "Stopsim"

	set YSZ 12
	set XSZ 84
	set YNR 60
	set NPR 10
	set SMX 250
	set Easy 1
	set HAS 0
	set HAS_CYCLE 0
	set dontwait 0
	set notexecutable 0
	set lastexecutable 0

	if {$m_typ == 2} {
		if {$tsc} {
		set pbox(0) \
		[mkbox "Time Sequence" "Sequence" "seq.out" 80 10 100 325]
		set dbox $pbox(0)
	}	}
	if {$msc} {
		if {[hasWord "!!"] || [hasWord "\\?\\?"]} {
			set Easy 0
		}

		set maxx [expr [winfo screenwidth .]  - 500]	;# button widths
		set maxh [expr [winfo screenheight .] - (350+120)]	;# borders+buttons
		set dbox2 \
		[mkcanvas "Message Sequence Chart" "msc" $maxx 350 1]
		.f$dbox2.c configure -height $maxh \
			-scrollregion "[expr -$XSZ/2] 0 \
				[expr $NPR*$XSZ] [expr $SMX*$YSZ]"
	}
	set stop 0
	set good_trail 0
	if {$s_typ == 1} {
		if $whichsim {
			set filen "pan_in${trail_num}.trail"
			if [file exists $filen] {
				set good_trail 1
			}
		} else {
			if {[file exists pan_in.trail] || [file exists pan_in.tra]} {
				set good_trail 1
			}
		} 
		if $good_trail {
			catch { .c$sbox.z.t insert end "preparing trail, please wait..." }
			update
			rmfile trail.out
			catch {eval exec $SPIN $s_options >&trail.out} errmsg
		} else {
			set errmsg "error: no trail file for guided simulation"
			return
		}
		if {[string length $errmsg]>0} {
			add_log "$errmsg"
			catch {
			tk_messageBox -icon info -message $errmsg
			}
			catch {
				set fd [open trail.out r]
				while {[gets $fd line] > -1} {
					add_log "$line"
				}
				close $fd
			}
			Stopsim
			catch { destroy .c$sbox }
			catch { destroy .c$dbox }
			set simruns 0
			update
			return
		}
		set fd [open trail.out r]
		catch { .c$sbox.z.t insert end "done\n" }
	} else {
		update
		set fd [open "|$SPIN $s_options" r+]
		catch "flush $fd"
		update
	}

	if {$s_typ == 2} {
		Runsim
	}

	if {$ebc} { startbar "Xspin Bar Chart" }

	set pstp -1
	set bailout 0
	set realstring ""

	while {$stop == 0 && [eof $fd] == 0} {
	if {$bailout == 0 && [gets $fd line] > -1} {
		set pln 0
		set syntax 0
		set isvar 0
		set pname ""
		set i 0
		set VERBOSE 0
		set Fnm "pan_in"
		if {$Unix == 0} {
			if {[string first "processes created" $line] > 0} {
				set bailout 1
		}	}
		if {[string first "type return to proceed" $line] > 0} {
			puts $fd ""
			flush $fd
			update
			continue
		}
		set lastpstp $pstp
		set pmtch [scan $line \
			"%d: proc %d (%s line %d \"%s\" " \
			pstp pno pname pln Fnm]
		incr pmtch -1
		set i [string first "\[" $line]
		if {$i > 0} {
			set i [expr $i + 1]
			set j [string length $line]
			set j [expr $j - 2]
			set stmnt [string range $line $i $j]
		} else {
			set stmnt "-"
		}
		if {$pmtch != 4} {
			set pmtch [scan $line \
				"	proc %d (%s line %d \"%s\" " \
				pno pname pln Fnm]
		}
		if {$pmtch != 4} {
			if {[string first "spin: line" $line] == 0 } {
				scan $line "spin: line %d \"%s\" " pln Fnm
				if {[string first "pan_in" $Fnm] >= 0} {
				.inp.t tag add Rev $pln.0 $pln.end
				.inp.t tag configure Rev \
					-background $FG -foreground $BG
				.inp.t yview -pickplace $pln.0
				}
				if {[string first "assertion viol" $line] < 0} {
					set syntax 1
				}
			}
			if {[string first "Error: "   $line] >= 0 \
			||  [string first "warning: " $line] >= 0 } {
				set syntax 1
			}
		}
		if {$pmtch != 4 && $syntax == 0} {
			set pmtch [scan $line \
				"%d: proc - (%s line %d \"%s\" " \
				pstp pname pln Fnm]
			if { $pmtch == 4 } {
				set pno -1
			}
		}
		#	set Fnm [string trim $Fnm "\""]
		set pname [string trim $pname "()"]

		if {[string first "TRACK" $pname] >= 0} {
			set nwcol([expr $pno+1]) 1
		} elseif {[string length $pname] > 0} {
			if {[info exists nwcol([expr $pno+1])] \
			&&  $nwcol([expr $pno+1])} {
				unset Plabel($pno)
##
				set TMP1 [expr ($pno + 1)*$XSZ]
				set TMP2 [expr $Pstp*$YSZ]
				.f$dbox2.c create line \
					[expr $TMP1 - 20] $TMP2 \
					[expr $TMP1 + 20] $TMP2 \
					-width 2 \
					-fill $Red
				incr TMP2 4
				.f$dbox2.c create line \
					[expr $TMP1 - 20] $TMP2 \
					[expr $TMP1 + 20] $TMP2 \
					-width 2 \
					-fill $Red
##
			}
			set nwcol([expr $pno+1]) 0
		}
		if {$pmtch == 4 && $syntax == 0} {
			if {$ebc} {
				if {[string first "values:" $line] < 0} {
					stepbar $pno $pname
			}	}
			if {$m_typ == 1 && $tsc} {
				if { [info exists pbox($pno)] == 0 } {
					set pbox($pno) [mkbox \
						"Proc $pno ($pname)" \
						"Proc$pno" "proc.$pno.out" \
						60 10 \
						[expr 100+$pno*25] \
						[expr 325+$pno*35] ]
				}
				set dbox $pbox($pno)
			} elseif {$m_typ == 0 && $tsc} {
				if { [info exists Spbox($pno)] == 0 } {
					set Spbox($pno) \
						[mkbox "$pname (proc $pno)" \
						"$pname" "" \
						60 10 \
						[expr 100+$pno*25] \
						[expr 325+$pno*35] ]
					readinfile .c$Spbox($pno).z.t "pan_in"
				}
				set Sdbox $Spbox($pno)
			}
		} elseif { [string first "..." $line] > 0 && \
			   [regexp "^\\\t*MSC: (.*)" $line] == 0 } {
			set $line ""
			set syntax 1
			set pln 0
		} elseif {$s_typ == 2 \
		      && [string first "Select " $line] == 0 } {
			set Banner $line
			set pln 0
			set notexecutable 0
			set lastexecutable 0
			set has_timeout 0
		} elseif {$s_typ == 2 \
		      && [string first "choice" $line] >= 0 } {
			scan $line "	choice %d" howmany
			set NN [string first ":" $line]; incr NN 2
			set Choice($howmany) [string range $line $NN end]
			if {[string first "timeout" $Choice($howmany)] > 0} {
				set has_timeout 1
			}
			if {[string first "unexecutable," $line] >= 0} {
				incr notexecutable
			} else {
				set lastexecutable $howmany
			}
			set pln 0
		} elseif {$s_typ == 2 \
		      && [string first "Make Selection" $line] >= 0 } {
			scan $line "Make Selection %d" howmany
			if {$notexecutable == $howmany-1 && $has_timeout == 0} {
				set howmany $lastexecutable
				add_log "selected: $howmany (forced)"
				catch {
					foreach el [array names Choice] {
					unset Choice($el)
				} }
			} else {
				pickoption $Banner
				add_log "selected: $howmany"
			}
			puts $fd $howmany
			catch "flush $fd"
			set dontwait 1
			set pln 0
		} elseif { [regexp "^\\\t*MSC: (.*)" $line mch rstr] != 0 } {
			if {$realstring != ""} {
			set realstring "$realstring $rstr"
			} else {
			set realstring $rstr
			}
			# picked up in next cycle
		} elseif { [string first "processes" $line] > 0 \
		      ||   [string first "timeout" $line]  == 0 \
		      ||   [string first "=s==" $line]  > 0 \
		      ||   [string first "=r==" $line]  > 0 } {

			if { $m_typ == 1 && $tsc} {
				set dbox $pbox(0)
			} elseif { $m_typ == 0 && $tsc} {
				if { [info exists Spbox($pno)] == 0 } {
					set Spbox($pno) \
						[mkbox "$pname (proc $pno)" \
						"$pname" "" \
						60 10 \
						[expr 100+$pno*25] \
						[expr 325+$pno*35] ]
					readinfile .c$Spbox($pno).z.t "pan_in"
				}
				set Sdbox $Spbox($pno)
			}
			set pln 0;	# prevent tag update
		} elseif {$syntax == 0 && [string first " = " $line] > 0 } {
				set isvar [string first "=" $line]
				set isvar [expr $isvar + 1]
				set varvl [string range $line $isvar end]
				set isvar [expr $isvar - 2]
				set varnm [string range $line 0 $isvar]
				set varnm [string trim $varnm "	"]
				set Varnm($varnm) $varvl
				set isvar 1
		} elseif { [scan $line " %s %d " varnm qnr] == 2} {
			if {$syntax == 0 &&  [string compare $varnm "queue"] == 0} {
				set isvar [string last ":" $line]
				set isvar [expr $isvar + 1]
				set varvl [string range $line $isvar end]
				set XX [string first "(" $line]
				set YY [string last  ")" $line]
				set ZZ [string range $line $XX $YY]
				set Queues($qnr) $varvl
				if {[info exists Alias($qnr)]} {
				if {[string first $ZZ $Alias($qnr)] < 0} {
					set Alias($qnr) "$Alias($qnr), $ZZ"
				}
				} else {
					set Alias($qnr) $ZZ
				}
				set isvar 1
			}
		} elseif {[string length $line] == 0} {
			if {$dontwait == 0} { set stepper 0 }
			set pln 0
			set Depth [expr $Depth + 1]
			set Seq($Depth) [tell $fd]
			set dontwait 0
		}


	if {$syntax == 0} {
		if {[string first "terminates" $line] > 0} {
			set pln -1
			set stmnt "<stop>"
		}
##NEW
		if {$pln > 0 && [string first "pan_in" $Fnm] >= 0} {
			.inp.t tag remove hilite 0.0 end
			src_line $pln
		}
##END
		if {$m_typ == 0} {
			if {$pln > 0 && [string first "pan_in" $Fnm] >= 0} {
				catch {
				.c$Sdbox.z.t yview -pickplace $pln.0
				.c$Sdbox.z.t tag remove Rev 1.0 end
				.c$Sdbox.z.t tag add Rev $pln.0 $pln.end
				.c$Sdbox.z.t tag configure Rev \
					-background $FG -foreground $BG
			}	}
		} elseif {$m_typ == 1} {
			if { [info exists pbox($pno)] == 0 } {
				set pbox($pno) [mkbox \
					"Proc $pno ($pname)" \
					"Proc$pno" "proc.$pno.out" \
					60 10 \
					[expr 100+$pno*25] \
					[expr 325+$pno*35] ]
			}
			set dbox $pbox($pno)
			catch {
				.c$dbox.z.t yview -pickplace end
				.c$dbox.z.t insert end "$line\n"
			}
		} elseif {$m_typ == 2 && $pln != 0 \
		&&  [string first "unexecutable, " $line] < 0} {
			catch { .c$dbox.z.t yview -pickplace end }
			catch { .c$dbox.z.t insert end "$pno:$pln" }
			for {set i $pno} {$i > 0} {incr i -1} {
				catch { .c$dbox.z.t insert end "\t|" }
			}
			catch { .c$dbox.z.t insert end "\t|>$stmnt\n" }
		}
		if {$msc && $pln != 0} {
			set Mcont "--"
			set HAS 0
			if { [scan $stmnt "values: %d!%d" inq inp1] == 2 \
			||   [scan $stmnt "values: %d!%s" inq inp2] == 2 } {
				set HAS   [string first "!" $stmnt]
				incr HAS
				set Mcont [string range $stmnt $HAS end]
				set HAS 1
			} elseif { [scan $stmnt "values: %d?%d" inq inp1] == 2 \
			|| [scan $stmnt "values: %d?%s" inq inp2] == 2 } {
				set HAS   [string first "?" $stmnt]
				incr HAS
				set Mcont [string range $stmnt $HAS end]
				set HAS 2
			} elseif { [string first "-" $stmnt] == 0} {
				set HAS 3
				if {$HAS_CYCLE} {
					set stmnt [format "Cycle>>"]
				} else {
					set stmnt [format "<waiting>"]
				}
			} elseif { [string first "<stop>" $stmnt] == 0} {
				set HAS 3
				set stmnt [format "<stopped>"]
			}
			if {$pno+1 > $Seenpno} { set Seenpno [expr $pno+1] }
			set XLOC [expr (1+$pno)*$XSZ]
			set YLOC [expr $Pstp*$YSZ]
			if {[string first "printf('MSC: " $stmnt] == 0} {
				set VERBOSE 1
				set stmnt $realstring
				if {[string first "BREAK" $realstring] >= 0} {
					BreakPoint
				}
				set realstring ""
			} else {
				set VERBOSE 0
			}
			catch {
			if {$VERBOSE \
			||  $HAS != 0 \
			||  [info exists R($pstp,$pno)]} {

				if { $SparseMsc == 1 \
				||   [info exists Plabel($pno)] == 0 \
				||   ([info exists R($pstp,$pno)] == 0 \
				&&   ($HAS != 1 \
				||   [info exists HasBox($YLOC,[expr 1+$pno])])) } {
					incr Pstp
					for	{set i 1} \
						{$Pstp > 1 && $i <= $Seenpno} \
						{incr i} {
						if {[info exists HasBox($YLOC,$i)]} {
							continue
						}
						set TMP1 [expr $i*$XSZ]
						set lncol $Blue
						set lnwdt 1
						catch {
							if {$nwcol($i)} {
								set lncol "gray"
								set lnwdt 15
						}	}
						.f$dbox2.c create line \
						$TMP1 $YLOC $TMP1 \
						[expr $YLOC+$YSZ] \
						-width $lnwdt \
						-fill $lncol
					}
					if {[info exists HasBox($YLOC,[expr 1+$pno])]} {
						set YLOC [expr $Pstp*$YSZ]
				}	}
				if {$HAS == 1 || $HAS == 2} {
					set stmnt [string range $stmnt 8 end]
				}
				if { [info exists Plabel($pno)] == 0} {
					set Plabel($pno) 0
					if {$SparseMsc == 0} {
						set HasBox($YLOC,[expr 1+$pno]) 1
					}
					.f$dbox2.c create rectangle \
						[expr $XLOC-20] $YLOC \
						[expr $XLOC+20] \
						[expr $YLOC+$YSZ] \
						-outline $Red -fill $Yellow

						if {$pname != "TRACK"} {
							.f$dbox2.c create text $XLOC \
								[expr $YLOC+$YSZ/2] \
								-font $SmallFont \
								-text "$pname:$pno"
						} else {
							.f$dbox2.c create text $XLOC \
								[expr $YLOC+$YSZ/2] \
								-font $SmallFont \
								-text "<show>"
						}

					set YLOC [expr $Pstp*$YSZ]
					incr Pstp
					for	{set i 1} \
						{$Pstp > 1 && $i <= $Seenpno} \
						{incr i} {
						set TMP1 [expr $i*$XSZ]
						set lncol $Blue
						set lnwdt 1
						catch {
							if {$nwcol($i)} {
								set lncol "gray"
								set lnwdt 15
						}	}
						.f$dbox2.c create line \
						$TMP1 $YLOC $TMP1 \
						[expr $YLOC+$YSZ] \
						-width $lnwdt \
						-fill $lncol
					}
				}
				if {(1+$pno) > $NPR} {
					set NPR [expr $pno+2]
					.f$dbox2.c configure \
					 -scrollregion \
					 "[expr -$XSZ/2] 0 \
					  [expr $NPR*$XSZ] [expr $SMX*$YSZ]"
				}
				if {$Pstp > $SMX-2} {
					set SMX [expr 2*$SMX]
					.f$dbox2.c configure \
					 -scrollregion \
					 "[expr -$XSZ/2] 0 \
					  [expr $NPR*$XSZ] [expr $SMX*$YSZ]"
				}

				if { [info exists R($pstp,$pno)] == 0 } {
					if {$VERBOSE == 1} {
						if {[string first "~W " $stmnt] == 0} {
							set BoxFil $White
							set stmnt [string range $stmnt 3 end] 
						} else { if {[string first "~G " $stmnt] == 0} {
							set BoxFil $Green
							set stmnt [string range $stmnt 3 end]
						} else { if {[string first "~R " $stmnt] == 0} {
							set BoxFil $Red
							set stmnt [string range $stmnt 3 end]
						} else { if {[string first "~B " $stmnt] == 0} {
							set BoxFil $Blue
							set stmnt [string range $stmnt 3 end]
						} else { set BoxFil $Yellow } } } }
						set BoxLab $stmnt
						if {[string first "line " $stmnt] == 0} {
							scan $stmnt "line %d" pln
							set Fnm "pan_in"	;# not necessarily right...
						}
					} else {
						set BoxLab $pstp
						set BoxFil $White
					}
					if {$SparseMsc == 0} {
						set HasBox($YLOC,[expr 1+$pno]) 1
					}
					set R($pstp,$pno) \
						[.f$dbox2.c create rectangle \
						 [expr $XLOC-20] $YLOC \
						 [expr $XLOC+20] \
						 [expr $YLOC+$YSZ] \
						 -outline $Blue -fill $BoxFil]
					set T($pstp,$pno) \
						[.f$dbox2.c create text \
						 $XLOC \
						 [expr $YLOC+$YSZ/2] \
						-font $SmallFont \
						-text $BoxLab]
					#if {$Pstp > $YNR-2} {
					#	.f$dbox2.c yview \
					#	 [expr ($Pstp-$YNR)]
					#}
				}
				if { $HAS == 3 } {
					.f$dbox2.c itemconfigure \
					 $R($pstp,$pno) \
					 -outline $Red -fill $Yellow
				}

				if {$SYMBOLIC} {
					.f$dbox2.c itemconfigure $T($pstp,$pno) \
						-font $SmallFont -text "$stmnt"
				} else {
					if {$VERBOSE == 0 } {
						.f$dbox2.c bind $T($pstp,$pno) <Any-Enter> "
						.f$dbox2.c itemconfigure $T($pstp,$pno) \
							-font $BigFont -text {$stmnt}
						.inp.t tag remove hilite 0.0 end
						if {[string first "pan_in" $Fnm] >= 0} {
							src_line $pln
						}
						"
						.f$dbox2.c bind $T($pstp,$pno) <Any-Leave> "
						.f$dbox2.c itemconfigure $T($pstp,$pno) \
							-font $SmallFont -text {$pstp}
						"
					} else {
						.f$dbox2.c bind $T($pstp,$pno) <Any-Enter> "
						.inp.t tag remove hilite 0.0 end
						if {[string first "pan_in" $Fnm] >= 0} {
							src_line $pln
						}
						"
					}
				}
			}

			set YLOC [expr $YLOC+$YSZ/2]
			if {$HAS == 1} {
				if { [info exists Q_add($inq)] == 0 } {
					set Q_add($inq) 0
					set Q_del($inq) 0
				}
				set Slot $Q_add($inq)
				incr Q_add($inq) 1

				set Mesg_y($inq,$Slot) $YLOC
				set Mesg_x($inq,$Slot) $XLOC
				set Q_val($inq,$Slot) $Mcont
			
				set Rem($inq,$Slot) \
					[.f$dbox2.c create text \
					[expr $XLOC-40] $YLOC \
					-font $SmallFont -text $stmnt]
			} elseif { $HAS == 2 } {
				if {$Easy} {
					set Slot $Q_del($inq)
					incr Q_del($inq) 1
				} else {
					for {set Slot $Q_del($inq)} \
						{$Slot < $Q_add($inq)} \
						{incr Slot} {
					if {$Q_val($inq,$Slot) == "_X_"} {
							incr Q_del($inq) 1
						} else {
							break
					}	}

					for {set Slot $Q_del($inq)} \
						{$Slot < $Q_add($inq)} \
						{incr Slot} {
					if {$Mcont == $Q_val($inq,$Slot)} {
						set Q_val($inq,$Slot) "_X_"
						break
					}	}
				}
				if {$Slot >= $Q_add($inq)} {
					add_log "<<error: cannot match $stmnt>>"
				} else {
					set TMP1 $Mesg_x($inq,$Slot)
					set TMP2 $Mesg_y($inq,$Slot)
					if {$XLOC < $TMP1} {
						set Delta -20
					} else {
						set Delta 20
					}
					.f$dbox2.c create line \
						[expr $TMP1+$Delta] $TMP2 \
						[expr $XLOC-$Delta] $YLOC \
						-fill $Red -width 2 \
						-arrow last -arrowshape {5 5 5}

					if {$SparseMsc == 0} {
						set TMP3 5
					} else {
						set TMP3 0
					}

					.f$dbox2.c coords $Rem($inq,$Slot) \
						[expr ($TMP1 + $XLOC)/2] \
						[expr ($TMP2 + $YLOC)/2 - $TMP3]
					.f$dbox2.c raise $Rem($inq,$Slot)
				}
			} }
		}
		if {$pln == 0 && ($gvars || $lvars || $qv)} {
			if {$Vvbox == 0} {
				if {$vv} { set Vvbox [mkbox "Data Values" \
					"Vars" "var.out" 50 30 100 350] }
			} else {
				catch { .c$Vvbox.z.t delete 0.0 end }
			}
			if {$vv} {
if {$gvars || $lvars} {
			foreach el [lsort [array names Varnm]] {
				if {[string length $Varnm($el)] > 0} {
				catch { .c$Vvbox.z.t insert \
					end "$el = $Varnm($el)\n" }
			}	}
}
if {$qv} {
			foreach el [lsort [array names Queues]] {
				catch {
				.c$Vvbox.z.t insert end "queue $el ($Alias($el))\n"
				.c$Vvbox.z.t insert end "	$Queues($el)\n"
			}	}
}
			}
		}
	} else {
			set stepper 0
	}
		if {$isvar == 0} {
			if {$syntax == 1} {
				if {[string first "..." $line] < 0} {
					add_log "$line"
				catch { .c$sbox.z.t insert end "$line\n" }
				catch { .c$sbox.z.t yview -pickplace end }
				}
			} else {
				if {[string length $line] > 0} {
				catch { .c$sbox.z.t insert end "$line\n" }
				catch { .c$sbox.z.t yview -pickplace end }
				}
				if {$m_typ == 2 && \
					[string first "START OF CYCLE" $line] > 0} {
					catch { .c$dbox.z.t yview -pickplace end }
					catch { .c$dbox.z.t insert end "$line\n" }
					catch {
					set XLOC [expr $Seenpno*$XSZ+$XSZ/2]
					set YLOC [expr $Pstp*$YSZ+$YSZ/2]

					.f$dbox2.c create text \
						[expr $XLOC+$XSZ] $YLOC \
						-font $SmallFont \
						-text "Cycle/Waiting" \
						-fill $Red

					.f$dbox2.c create line \
						$XLOC $YLOC \
						[expr $XLOC+$XSZ/2] $YLOC \
						-fill $Red \
						-arrow first -arrowshape {5 5 5}
					}
					set HAS_CYCLE [expr $YLOC+1]
				}
				if {$m_typ == 2 && $HAS == 3 && $HAS_CYCLE != 0} {
					catch {
					set YLOC [expr $Pstp*$YSZ+$YSZ/2]
					set XLOC0 [expr $pno*$XSZ+$XSZ]
					set XLOC [expr $Seenpno*$XSZ+$XSZ]
					.f$dbox2.c create line \
						$XLOC0 [expr $YLOC-$YSZ/2] \
						$XLOC0 $YLOC \
						-fill $Red
					.f$dbox2.c create line \
						$XLOC0 $YLOC $XLOC $YLOC \
						-fill $Red

					set XLOC [expr $Seenpno*$XSZ+$XSZ]

					.f$dbox2.c create line \
						$XLOC $YLOC $XLOC \
						[expr $HAS_CYCLE-1] \
						-fill $Red
		}	}	}	}
		# mystery update:
		if {$tk_major >= 4 || $m_typ != 1} {
			update	;# tk 3.x can crash on this
		}

		if {$syntax == 0 \
		&&  $stop == 0 \
		&&  $stepped == 1 \
		&&  $stepper == 0 \
		&&  $dontwait == 0} {
			update	;# here it is harmless also with tk 3.x
			tkwait variable stepper
		}
	} else {
		if {$s_typ == 0 || $s_typ == 2} {
			add_log "<at end of run>"
		} else {
			add_log "<at end of trail>"
		}
		catch { addscales $dbox2 }
		if {$ebc} { barscales }
		update
		tkwait variable stepper
	}
	}
	# end of guided trail

	while {$stepper == 1} {
		tkwait variable stepper
	}
	teardown
	
	catch "close $fd"
	add_log "<done>"

	update
}

proc teardown {} {
	global m_typ pbox sbox dbox Spbox Vvbox
	global simruns stop stepped stepper howmany

	set simruns 0
	set stop 1
	set stepped 0
	set stepper 0
	catch { set howmany 0 }
	catch {
		if { $m_typ == 1 } {
			foreach el [array names pbox] {
				catch { destroy .c$pbox($el) }
				catch { unset pbox($el) }
			}
		} elseif { $m_typ == 0 } {
			foreach el [array names Spbox] {
				catch { destroy .c$Spbox($el) }
				catch { unset Spbox($el) }
		}	}
	}
	if {[winfo exists .c$sbox]} {
		set x "Simulation Output"
		set PlaceBox($x) [wm geometry .c$sbox]
		set k [string first "\+" $PlaceBox($x)]
		if {$k > 0} {
			set PlaceBox($x) [string range $PlaceBox($x) $k end]
		}
		destroy .c$sbox
	}
	catch { destroy .c$dbox }
	if {[winfo exists .c$Vvbox]} {
		set x "Data Values"
		set PlaceBox($x) [wm geometry .c$Vvbox]
		set k [string first "\+" $PlaceBox($x)]
		if {$k > 0} {
			set PlaceBox($x) [string range $PlaceBox($x) $k end]
		}
		destroy .c$Vvbox
	}
}

set PlaceMenu	"+150+150"

proc pickoption {nm} {
	global howmany Choice PlaceMenu

	catch {destroy .prompt}
	toplevel .prompt
	wm title .prompt "Select"
	wm iconname .prompt "Select"
	wm geometry .prompt $PlaceMenu

	text .prompt.t -relief raised -bd 2 \
		-width [string length $nm] -height 1 \
		-setgrid 1
	pack append .prompt .prompt.t { top expand fillx }
	.prompt.t insert end "$nm"
	for {set i 0} {$i <= $howmany} {incr i} {
		if {[info exists Choice($i)] \
		&&  $Choice($i) != 0 \
		&&  [string first "outside range" $Choice($i)] < 0 \
		&&  [string first "unexecutable," $Choice($i)] <= 0} {
			pack append .prompt \
			  [button .prompt.b$i -text "$i: $Choice($i)" \
			  -anchor w \
			  -command "set howmany $i" ] \
			  {top expand fillx}

			set j [string first "line " $Choice($i)]
			if {$j > 0} {
			  set k [string range $Choice($i) $j end]
			  scan $k "line %d" k
			  bind .prompt.b$i <Enter> "report $k"
			  bind .prompt.b$i <Leave> "report 0"
			  bind .prompt.b$i <ButtonRelease-1> "set howmany $i"
	}	}	}
	tkwait variable howmany
	set PlaceMenu [wm geometry .prompt]
	set k [string first "\+" $PlaceMenu]
	if {$k > 0} {
		set PlaceMenu [string range $PlaceMenu $k end]
	}
	catch { foreach el [array names Choice]  { unset Choice($el) } }
	destroy .prompt
}

proc report {n} {
	.inp.t tag remove hilite 0.0 end
	src_line $n
}

# validation options panel

set an_typ -1;	set cp_typ 0; set cyc_typ 0
set as_typ -1;  set ie_typ 1; set ebc 0
set ct_typ 0;	set et_typ 1
set st_typ 0;	set se_typ 0; set bf_typ 0
set oct_typ -1;	# remembers last setting used for compilation
set nv_typ 1
set po_typ -1;	set cm_typ 0; set vb_typ 0
set pr_typ 0;	set where 0
set vr_typ 0;	set xu_typ -1
set ur_typ 1;	set vbox 0
set killed 0;	set Job_Done 0;	set tcnt 0
set waitwhat "none"
set not_warned_yet 1

set LastGenerate	""
set LastCompile	""
set NextCompile	""

proc syntax_check {a T} {
	global SPIN BG FG

	mkpan_in
	add_log "$SPIN $a pan_in"
	catch {exec $SPIN $a pan_in >&pan.tmp} err ;# added -v
	set cnt 0
	set maxln 50
	set ef [open pan.tmp r]
	.inp.t tag remove hilite 0.0 end
	.inp.t tag remove sel 0.0 end
	set pln 0
	set allmsg ""
	while {[gets $ef line] > -1} {
		add_log "$line"
		set allmsg "$allmsg\n$line"
		if {[string first "spin: line" $line] >= 0} {
			scan $line "spin: line %d" pln
			src_line $pln
		}
		if {[string first "spin: warning, line" $line] >= 0} {
			scan $line "spin: warning, line %d" pln
			src_line $pln
		}
		incr cnt
	}
	close $ef
	if {$cnt == 0} { add_log "no syntax errors" } else {
		warner $T "$allmsg" 800
	}
	update
}

proc prescan {} {
	global an_typ cp_typ nv_typ po_typ
	global xu_typ as_typ ie_typ

	mkpan_in

	if {$an_typ == -1} {
		set an_typ 0
		set nv_typ [hasWord "never"]
		if {[hasWord "accept.*:"]} {
			set an_typ 1
			set cp_typ 2
		} elseif {[hasWord "progress.*:"]} {
			set an_typ 1
			set cp_typ 1
		}
	}
	if {$po_typ == -1} {
		if {[hasWord "_last"] \
		||  [hasWord "provided.*\\("] \
		||  [hasWord "enabled\\("]} {
			set po_typ 0
		} else {
			set po_typ 1
		}
	}
	if {$xu_typ == -1} {
		if {[hasWord "xr"] || [hasWord "xs"]} {
			set xu_typ 1
		} else {
			set xu_typ 0
		}
	}
	if {$as_typ == -1} {
		if {$an_typ == 0} {
			set as_typ [hasWord "assert"]
			set ie_typ 1
		} else {
			set as_typ 0
			set ie_typ 0
		}
	}
}

proc basicval2 {} {
	global e ival expl HelvBig PlaceSim
	global an_typ cp_typ nv_typ firstime
	global cyc_typ ct_typ lt_typ
	global et_typ st_typ se_typ bf_typ stop
	global vb_typ pr_typ vr_typ ur_typ xu_typ

	set nv_typ 1
	set an_typ 1
	set cp_typ 2

	dump_tl "pan.ltl"

	catch { .menu.run.m entryconfigure 8 -state normal }
	catch { .tl.results.top.rv configure -state normal }
	set stop 0
	set firstime 0
	set lt_typ 1

	catch {destroy .v}
	toplevel .v

	set k [string first "\+" $PlaceSim]
	if {$k > 0} {
		set PlaceSim [string range $PlaceSim $k end]
	}

	wm title .v "LTL Verification Options"
	wm iconname .v "VAL"
	wm geometry .v $PlaceSim

	prescan

	frame .v.correct -relief flat -borderwidth 1m
	frame .v.cframe  -relief raised -borderwidth 1m

	set z .v.correct

	frame $z.rframe  -relief raised -borderwidth 1m

	label $z.rframe.lb \
		-font $HelvBig \
		-text "Options" \
		-relief sunken -borderwidth 1m

	checkbutton $z.rframe.fc -text "With Weak Fairness" \
		-variable cyc_typ \
		-relief flat 
	checkbutton $z.rframe.xu -text "Check xr/xs Assertions" \
		-variable xu_typ \
		-relief flat

	pack append $z.rframe \
		$z.rframe.lb {top pady 4 frame w fillx} \
		$z.rframe.fc {top pady 4 frame w} \
		$z.rframe.xu {top pady 4 frame w filly}

	pack append $z $z.rframe {top frame nw filly}

	label .v.cframe.lb \
		-font $HelvBig \
		-text "Verification" \
		-relief sunken -borderwidth 1m

	radiobutton .v.cframe.ea -text "Exhaustive" \
		-variable ct_typ -value 0 \
		-relief flat 
	radiobutton .v.cframe.sa -text "Supertrace/Bitstate" \
		-variable ct_typ -value 1 \
		-relief flat 
	radiobutton .v.cframe.hc -text "Hash-Compact" \
		-variable ct_typ -value 2 \
		-relief flat 

	pack append .v.cframe .v.cframe.lb {top pady 4 frame nw fillx} \
		.v.cframe.ea {top pady 4 frame nw} \
		.v.cframe.sa {top pady 4 frame nw} \
		.v.cframe.hc {top pady 4 frame nw}

	frame .v.pf -relief raised -borderwidth 1m
	frame .v.pf.mesg -borderwidth 1m
	
	label .v.pf.mesg.loss0 \
		-font $HelvBig \
		-text "A Full Queue" \
		-relief sunken -borderwidth 1m
	radiobutton .v.pf.mesg.loss1 -text "Blocks New Msgs" \
		-variable l_typ -value 0 \
		-relief flat
	radiobutton .v.pf.mesg.loss2 -text "Loses New Msgs" \
		-variable l_typ -value 1 \
		-relief flat
	pack append .v.pf.mesg \
		.v.pf.mesg.loss0 {top pady 4 frame w expand fillx} \
		.v.pf.mesg.loss1 {top pady 4 frame w} \
		.v.pf.mesg.loss2 {top pady 4 frame w}
	pack append .v.pf \
		.v.pf.mesg   {left frame w expand fillx}

	pack append .v \
		.v.cframe  {top frame w fill}\
		.v.correct {top frame w fill}\
		.v.pf {top frame w expand fill}

	pack append .v [button .v.adv -text "\[Set Advanced Options]" \
		-command "advanced_val" ] {top fillx}
	pack append .v [button .v.run -text "Run" \
		-command {runval ".tl.results.t"} ] {right frame se}
	pack append .v [button .v.exit -text "Cancel" \
		-command "set PlaceSim [wm geometry .v]; \
		set stop 1; destroy .v"] {right frame se}
	pack append .v [button .v.help -text "Help" -fg red \
		-command "roadmap2f" ] {right frame se}
}

set PlaceBasic	"+100+100"
set PlaceAdv	"+150+100"

proc basicval {} {
	global e ival expl HelvBig PlaceBasic
	global an_typ nv_typ firstime as_typ ie_typ
	global cyc_typ ct_typ lt_typ as_typ ie_typ
	global et_typ st_typ se_typ bf_typ stop
	global vb_typ pr_typ vr_typ ur_typ xu_typ

	catch { .menu.run.m entryconfigure 8 -state normal }
	catch { .tl.results.top.rv configure -state normal }
	set stop 0
	set firstime 0
	set lt_typ 0

	catch {destroy .v}
	toplevel .v

	wm title .v "Basic Verification Options"
	wm iconname .v "VAL"
	wm geometry .v $PlaceBasic

	prescan

	frame .v.correct -relief flat -borderwidth 1m
	frame .v.cframe  -relief raised -borderwidth 1m

	set z .v.correct

	frame $z.rframe  -relief raised -borderwidth 1m

	label $z.rframe.lb \
		-font $HelvBig \
		-text "Correctness Properties" \
		-relief sunken -borderwidth 1m
	radiobutton $z.rframe.sp -text "Safety (state properties)" \
		-variable an_typ -value 0 \
		-relief flat \
		-command { set cyc_typ 0; set cp_typ 0
			if {$an_typ == 0} {
				set as_typ [hasWord "assert"]
				set ie_typ 1
			}
		 }
	frame $z.rframe.sf
	checkbutton $z.rframe.sf.as -text "Assertions" \
		-variable as_typ \
		-relief flat \
		-command {
			set an_typ 0
			if {![hasWord "assert"] && $as_typ==1} then {
				complain6
			}
		 }
	checkbutton $z.rframe.sf.ie -text "Invalid Endstates" \
		-variable ie_typ \
		-relief flat \
		-command { set an_typ 0 }

	frame $z.rframe.sf.fill -width 15
	pack append $z.rframe.sf \
		$z.rframe.sf.fill {left frame w} \
		$z.rframe.sf.as {top pady 4 frame w} \
		$z.rframe.sf.ie {top pady 4 frame w}

	radiobutton $z.rframe.cp -text "Liveness (cycles/sequences)" \
		-variable an_typ -value 1 \
		-relief flat \
		-command {
			set as_typ 0; set ie_typ 0
			if {[hasWord "accept"]} then { set cp_typ 2 }\
			elseif {[hasWord "progress"]} then { set cp_typ 1 } \
			else complain5
		}

	frame $z.rframe.sub
	radiobutton $z.rframe.sub.np -text "Non-Progress Cycles" \
		-variable cp_typ -value 1 \
		-relief flat \
		-command {
			set an_typ 1
			if {![hasWord "progress"] && $cp_typ==1} then {
				complain4
			}
		 }
	radiobutton $z.rframe.sub.ac -text "Acceptance Cycles" \
		-variable cp_typ -value 2 \
		-relief flat \
		-command {
			set an_typ 1
			if {![hasWord "accept"] && $cp_typ==2} then {
				complain1
			}
		}
	checkbutton $z.rframe.sub.fc -text "With Weak Fairness" \
		-variable cyc_typ \
		-relief flat  \
		-command { if {$an_typ==0} then "set cyc_typ 0; complain3" }

	checkbutton $z.rframe.nv -text "Apply Never Claim (If Present)" \
		-variable nv_typ \
		-relief flat \
		-command { if {![hasWord "never"] && $nv_typ==1} then "complain2" }
	checkbutton $z.rframe.ur -text "Report Unreachable Code" \
		-variable ur_typ \
		-relief flat
	checkbutton $z.rframe.xu -text "Check xr/xs Assertions" \
		-variable xu_typ \
		-relief flat

	frame $z.rframe.sub.fill -width 15
	pack append $z.rframe.sub \
		$z.rframe.sub.fill {left frame w} \
		$z.rframe.sub.np {top pady 4 frame w} \
		$z.rframe.sub.ac {top pady 4 frame w} \
		$z.rframe.sub.fc {top pady 4 frame w}

	pack append $z.rframe \
		$z.rframe.lb {top pady 4 frame w fillx} \
		$z.rframe.sp {top pady 4 frame w} \
			$z.rframe.sf {top pady 4 frame w} \
		$z.rframe.cp {top pady 4 frame w} \
			$z.rframe.sub {top pady 4 frame w} \
		$z.rframe.nv {top pady 4 frame w} \
		$z.rframe.ur {top pady 4 frame w} \
		$z.rframe.xu {top pady 4 frame w filly}

	pack append $z $z.rframe {top frame nw filly}

	label .v.cframe.lb \
		-font $HelvBig \
		-text "Search Mode" \
		-relief sunken -borderwidth 1m

	radiobutton .v.cframe.ea -text "Exhaustive" \
		-variable ct_typ -value 0 \
		-relief flat 
	radiobutton .v.cframe.sa -text "Supertrace/Bitstate" \
		-variable ct_typ -value 1 \
		-relief flat 
	radiobutton .v.cframe.hc -text "Hash-Compact" \
		-variable ct_typ -value 2 \
		-relief flat 

	pack append .v.cframe .v.cframe.lb {top pady 4 frame nw fillx} \
		.v.cframe.ea {top pady 4 frame nw} \
		.v.cframe.sa {top pady 4 frame nw} \
		.v.cframe.hc {top pady 4 frame nw}

	frame .v.pf -relief raised -borderwidth 1m
	frame .v.pf.mesg -borderwidth 1m
	
	label .v.pf.mesg.loss0 \
		-font $HelvBig \
		-text "A Full Queue" \
		-relief sunken -borderwidth 1m
	radiobutton .v.pf.mesg.loss1 -text "Blocks New Msgs" \
		-variable l_typ -value 0 \
		-relief flat
	radiobutton .v.pf.mesg.loss2 -text "Loses New Msgs" \
		-variable l_typ -value 1 \
		-relief flat
	pack append .v.pf.mesg \
		.v.pf.mesg.loss0 {top pady 4 frame w fillx} \
		.v.pf.mesg.loss1 {top pady 4 frame w} \
		.v.pf.mesg.loss2 {top pady 4 frame w}
	pack append .v.pf \
		.v.pf.mesg {left frame nw expand fill}

	pack append .v \
		.v.correct {left} \
		.v.cframe  {top frame n expand fill}\
		.v.pf {top frame n expand fill}

	pack append .v [button .v.nvr -text "\[Add Never Claim from File]" \
		-command "call_nvr" ] {top fillx}
	pack append .v [button .v.ltl -text "\[Verify an LTL Property]" \
		-command "destroy .v; call_tl" ] {top fillx}
	pack append .v [button .v.adv -text "\[Set Advanced Options]" \
		-command "advanced_val" ] {top fillx}
	pack append .v [button .v.run -text "Run" \
		-command {set PlaceBasic [wm geometry .v]; runval "0"} ] {right frame se}
	pack append .v [button .v.exit -text "Cancel" \
		-command {set PlaceBasic [wm geometry .v]; \
		set stop 1; destroy .v}] {right frame se}
	pack append .v [button .v.help -text "Help" -fg red \
		-command "roadmap2e" ] {right frame se}
}

set HasNever ""

proc call_nvr {} {
	global HasNever
	global xversion Fname nv_typ

	switch [info commands tk_getOpenFile] "" {
		set fileselect "FileSelect open"
	} default {
		set fileselect "tk_getOpenFile \
			-filetypes { \
				{ { Aut files }  .aut } \
				{ { Nvr files }  .nvr } \
				{ { All Files }   *   } \
				}"
	}

	set HasNever [eval $fileselect]

	if {$HasNever == ""} {
		wm title . "SPIN CONTROL $xversion -- File: $Fname"
		set nv_typ 0
	} else {
		set nv_typ 1
		set z [string last "\/" $HasNever]
		if {$z > 0} {
			incr z
			set HsN [string range $HasNever $z end]
		} else {
			set HsN $HasNever
		}
		wm title . "SPIN CONTROL $xversion -- File: $Fname  Claim: $HsN"
	}
}

proc advanced_val {} {
	global e ival expl HelvBig
	global nv_typ firstime PlaceAdv
	global cyc_typ ct_typ
	global et_typ st_typ se_typ bf_typ stop po_typ cm_typ
	global vb_typ pr_typ vr_typ ur_typ xu_typ

	catch { .menu.run.m entryconfigure 8 -state normal }
	catch { .tl.results.top.rv configure -state normal }
	set stop 0
	set firstime 0

	catch {destroy .av}
	toplevel .av

	wm title .av "Advanced Verification Options"
	wm iconname .av "VAL"
	wm geometry .av $PlaceAdv

	frame .av.pans
	frame .av.pans.correct -relief flat
	frame .av.memopts -relief flat;		# memory options panel
	frame .av.oframe  -relief raised -borderwidth 1m ;# error trail options
	frame .av.recomp  -relief raised -borderwidth 1m ;# recompilation

	prescan

	for {set x 0} {$x<=2} {incr x} {
		frame .av.memopts.choice$x -relief flat
		entry .av.memopts.choice$x.e1 -relief sunken -width 20
		label .av.memopts.choice$x.e2 -text $e($x) -relief flat
		.av.memopts.choice$x.e1 insert end $ival($x)

		pack append .av.memopts.choice$x \
			.av.memopts.choice$x.e2 {left  frame w fillx} \
			[button .av.memopts.choice$x.e3 -text $expl($x) \
			-command "d_list $x" ] {right frame e} \
			.av.memopts.choice$x.e1 {right frame e fillx}

		pack append .av.memopts \
			.av.memopts.choice$x { top frame w pady 5 fillx}
	}
	for {set x 7} {$x<=7} {incr x} {
		frame .av.memopts.choice$x -relief flat
		entry .av.memopts.choice$x.e1 -relief sunken -width 20
		label .av.memopts.choice$x.e2 -text $e($x) -relief flat
		.av.memopts.choice$x.e1 insert end $ival($x)

		pack append .av.memopts.choice$x \
			.av.memopts.choice$x.e2 {left  frame w fillx} \
			[button .av.memopts.choice$x.e3 -text $expl($x) \
			-command "d_list $x" ] {right frame e} \
			.av.memopts.choice$x.e1 {right frame e fillx}

		pack append .av.memopts \
			.av.memopts.choice$x { top frame w pady 5 fillx}
	}
	for {set x 3} {$x<=5} {incr x} {
		frame .av.memopts.choice$x -relief flat
		entry .av.memopts.choice$x.e1 -relief sunken -width 20
		label .av.memopts.choice$x.e2 -text $e($x) -relief flat
		.av.memopts.choice$x.e1 insert end $ival($x)

		pack append .av.memopts.choice$x \
			.av.memopts.choice$x.e2 {left  frame w fillx} \
			[button .av.memopts.choice$x.e3 -text $expl($x) \
			-command "d_list $x" ] {right frame e} \
			.av.memopts.choice$x.e1 {right frame e fillx}

		pack append .av.memopts \
			.av.memopts.choice$x { top frame w pady 5 fillx}
	}
	set z .av.pans.correct
	frame $z.rframe  -relief raised -borderwidth 1m
	label $z.rframe.lb3 \
		-font $HelvBig \
		-text "   Error Trapping   " \
		-relief sunken -borderwidth 1m
	radiobutton $z.rframe.c0 -text "Don't Stop at Errors" \
		-variable et_typ -value 0 \
		-relief flat 
	checkbutton $z.rframe.c0a -text "Save All Error-trails" \
		-variable st_typ \
		-relief flat 
	checkbutton $z.rframe.c0b -text "Find Shortest Trail (iterative)" \
		-variable se_typ \
		-relief flat
	checkbutton $z.rframe.c0c -text "Use Breadth-First Search" \
		-variable bf_typ \
		-relief flat
	frame  $z.rframe.basic1 

	frame $z.rframe.cc
	radiobutton $z.rframe.cc.c1 -text "Stop at Error Nr:" \
		-variable et_typ -value 1 \
		-relief flat 
	entry $z.rframe.cc.c2 -relief sunken -width 8
	$z.rframe.cc.c2 insert end "$ival(6)"
	pack append $z.rframe.cc \
		$z.rframe.cc.c1 {left}\
		$z.rframe.cc.c2 {right expand fillx}

	pack append $z.rframe \
		$z.rframe.lb3 { top expand fillx frame nw} \
		$z.rframe.cc  {top pady 4 frame w} \
		$z.rframe.c0  {top pady 4 frame w} \
		$z.rframe.c0a {top pady 4 frame w} \
		$z.rframe.c0b {top pady 4 frame w} \
		$z.rframe.c0c {top pady 4 frame w} \
		$z.rframe.basic1 {top frame w}
	pack append $z $z.rframe {top frame nw expand fill}

	frame .av.pans.pf -relief flat
	set z .av.pans.pf
	frame $z.mesg -relief raised -borderwidth 1m;		# queue loss options
	frame $z.pframe -relief raised -borderwidth 1m
	label $z.pframe.lb2 \
		-font $HelvBig \
		-text "   Type of Run   " \
		-relief sunken -borderwidth 1m
	checkbutton $z.pframe.po -text "Use Partial Order Reduction" \
		-variable po_typ \
		-relief flat 
	checkbutton $z.pframe.cm -text "Use Compression" \
		-variable cm_typ \
		-relief flat 
#	checkbutton $z.pframe.vb -text "Verbose (For Debugging Only)" \
#		-variable vb_typ \
#		-relief flat
	checkbutton $z.pframe.pr -text "Add Complexity Profiling" \
		-variable pr_typ \
		-relief flat
	checkbutton $z.pframe.vr -text "Compute Variable Ranges" \
		-variable vr_typ \
		-relief flat

	pack append $z.pframe \
		$z.pframe.lb2 {top fillx pady 4 frame w} \
		$z.pframe.po {top pady 4 frame w} \
		$z.pframe.cm {top pady 4 frame w} \
		$z.pframe.pr  {top pady 4 frame w} \
		$z.pframe.vr  {top pady 4 frame w}

	pack append .av.pans.pf \
		.av.pans.pf.pframe  {top frame nw expand fill}
	pack append .av.pans \
		.av.pans.correct {left frame nw expand fillx}\
		.av.pans.pf {left frame nw expand fillx}

	button .av.help -text "Help" -fg red -command "roadmap2d"
	button  .av.basic1 -text "Set" -fg red -command "stopval 1" 
	button  .av.basic0 -text "Cancel" -command "stopval 0" 

	pack append .av \
		.av.memopts {top frame w} \
		.av.pans {top fillx} \
		.av.help  {left frame w} \
		.av.basic1 {right frame e} \
		.av.basic0 {right frame e}
}

proc g_list {} {
	global FG BG

	catch {destroy .r}
	toplevel .r

	wm title .r "Options"
	wm iconname .r "Options"

	frame .r.top
		listbox .r.top.list -width  6 -height 3 -relief raised
		listbox .r.top.expl -width 40 -height 3  -relief flat
	pack append .r.top \
		.r.top.list {left}\
		.r.top.expl {left}
	frame .r.bot
		text .r.bot.text -width 40 -height 1 -relief flat
		.r.bot.text insert end "(Double-Click option or Cancel)"
		button .r.bot.quit -text "Cancel" -command "destroy .r"
	pack append .r.bot \
		.r.bot.text {top}\
		.r.bot.quit {frame s}

	frame .r.caps
		text .r.caps.cap1 -width 6 -height -1 -fg blue
		text .r.caps.cap2 -width 30 -height -1 -fg blue
		.r.caps.cap1 insert end "Option:"
		.r.caps.cap2 insert end "Meaning:"
	pack append .r.caps \
		.r.caps.cap1 {left} \
		.r.caps.cap2 {left}

	pack append .r \
		.r.caps  {frame w}\
		.r.top {top expand} \
		.r.bot {bottom expand}

	foreach i { "-o1" "-o2" "-o3" } {
		.r.top.list insert end $i
	}
 
	foreach i { \
		"disable dataflow-optimizations" \
		"disable dead variables elimination" \
		"disable statement merging" } {
		.r.top.expl insert end $i
	}
	bind .r.top.list <Double-Button-1> {
		set extra [selection get]
		.av.memopts.choice5.e1 insert end " $extra"
		destroy .r
	}
}

proc r_list {} {
	global FG BG

	catch {destroy .r}
	toplevel .r

	wm title .r "Options"
	wm iconname .r "Options"

	frame .r.top
		listbox .r.top.list -width  6 -height 8 -relief raised
		listbox .r.top.expl -width 40 -height 8  -relief flat
	pack append .r.top \
		.r.top.list {left}\
		.r.top.expl {left}
	frame .r.bot
		text .r.bot.text -width 40 -height 1 -relief flat
		.r.bot.text insert end "(Double-Click option or Cancel)"
		button .r.bot.quit -text "Cancel" -command "destroy .r"
	pack append .r.bot \
		.r.bot.text {top}\
		.r.bot.quit {frame s}

	frame .r.caps
		text .r.caps.cap1 -width 6 -height -1 -fg blue
		text .r.caps.cap2 -width 30 -height -1 -fg blue
		.r.caps.cap1 insert end "Option:"
		.r.caps.cap2 insert end "Meaning:"
	pack append .r.caps \
		.r.caps.cap1 {left} \
		.r.caps.cap2 {left}

	pack append .r \
		.r.caps  {frame w}\
		.r.top {top expand} \
		.r.bot {bottom expand}

	foreach i { "-d" "-q" "-I" "-h?" "-s" "-A" "-E" "-w?" } {
		.r.top.list insert end $i
	}
 
	foreach i { \
		"print state tables and stop" \
		"require all chans to be empty in valid endstates" \
		"try to find shortest trail" \
		"choose another seed for hash 1..32 (default 1)" \
		"use 1-bit hashing (default is 2-bit)" \
		"ignore assertion violation errors" \
		"ignore invalid endstate errors" \
		"set explicit -w parameter" \
		"" } {
		.r.top.expl insert end $i
	}
	bind .r.top.list <Double-Button-1> {
		set extra [selection get]
		.av.memopts.choice4.e1 insert end " $extra"
		destroy .r
	}
}

proc d_list {nr} {

	if {$nr == 0} { roadmap2a; return }
	if {$nr == 1} { roadmap2b; return }
	if {$nr == 2} { roadmap2c; return }
	if {$nr == 4} { r_list; return }
	if {$nr == 5} { g_list; return }
	if {$nr == 7} { roadmap2k; return }
#	if {$nr != 3} { roadmap2; return }

	catch {destroy .b}
	toplevel .b

	wm title .b "Options"
	wm iconname .b "Options"

	frame .b.top
		scrollbar .b.top.scroll -command ".b.top.list yview"
		listbox   .b.top.list -yscroll ".b.top.scroll set" -relief raised
	pack append .b.top \
		.b.top.scroll {right filly}\
		.b.top.list {left expand}

	frame .b.bot
		text .b.bot.text -width 21 -height 1 -relief flat
		.b.bot.text insert end "(Double-Click option)"
		button .b.bot.quit -text "Cancel" -command "destroy .b"
		button .b.bot.expl -text "Explanations" -command "roadmap6"
	pack append .b.bot \
		.b.bot.text {top frame nw}\
		.b.bot.expl {left}\
		.b.bot.quit {left}


	pack append .b \
		.b.top {top frame nw expand} \
		.b.bot {bottom}

	foreach i { \
		"-DBCOMP" \
		"-DCTL" \
		"-DGLOB_ALPHA" \
		"-DMA=?" \
		"-DNFAIR=?" \
		"-DNIBIS" \
		"-DNOBOUNDCHECK" \
		"-DNOREDUCE" \
		"-DNOCOMP" \
		"-DNOSTUTTER" \
		"-DNOVSZ" \
		"-DPRINTF" \
		"-DRANDSTORE=?" \
		"-DR_XPT" \
		"-DSDUMP" \
		"-DSVDUMP" \
		"-DVECTORSZ=?" \
		"-DW_XPT=?" \
		"-DXUSAFE" \
		} {
		.b.top.list insert end $i
	}
	bind .b.top.list <Double-Button-1> {
		set directive [selection get]
		.av.memopts.choice3.e1 insert end " $directive"
		destroy .b
	}
}

proc complain1 {} {
	set m "warning: there are no accept labels"
	add_log $m
	catch { tk_messageBox -icon info -message $m }
}

proc complain2 {} {
	set m "warning: there is no never claim"
	add_log $m
	catch { tk_messageBox -icon info -message $m }
}

proc complain3 {} {
	set m "weak fairness is irrelevant to state properties"
	add_log $m
	catch { tk_messageBox -icon info -message $m }
}

proc complain4 {} {
	set m "warning: there are no progress labels"
	add_log $m
	catch { tk_messageBox -icon info -message $m }
}

proc complain5 {} {
	global an_typ
	set m "warning: there are neither accept nor progress labels"
	add_log $m
	set an_typ 0
	catch { tk_messageBox -icon info -message $m }
}

proc complain6 {} {
	set m "warning: there are no assert statements in the spec"
	add_log $m
	catch { tk_messageBox -icon info -message $m }
}

proc complain7 {} {
	set m "warning: Breadth-First Search implies a restriction to Safety properties"
	add_log $m
	catch { tk_messageBox -icon info -message $m }
}

proc complain8 {} {
	set m "error: cannot combine -DMA and -DBITSTATE"
	add_log $m
	catch { tk_messageBox -icon info -message $m }
}

proc stopval {how} {
	global stop ival PlaceAdv

	if {$how} {
	set ival(0) "[.av.memopts.choice0.e1 get]"
	set ival(1) "[.av.memopts.choice1.e1 get]"
	set ival(2) "[.av.memopts.choice2.e1 get]"
	set ival(3) "[.av.memopts.choice3.e1 get]"
	set ival(4) "[.av.memopts.choice4.e1 get]"
	set ival(5) "[.av.memopts.choice5.e1 get]"
	set ival(7) "[.av.memopts.choice7.e1 get]"
	set ival(6) "[.av.pans.correct.rframe.cc.c2 get]"
	}
	set stop 1
	if {[winfo exists .av]} {
		set PlaceAdv [wm geometry .av]
		set k [string first "\+" $PlaceAdv]
		if {$k > 0} {
			set PlaceAdv [string range $PlaceAdv $k end]
		}
		destroy .av
	}
}

proc log {n} {
	set m 1
	set cnt 0
	while {$m<$n} {
		set m [expr $m*2]
		incr cnt
	}
	return $cnt
}

proc bld_v_options {} {
	global an_typ cp_typ cyc_typ as_typ ie_typ
	global et_typ st_typ se_typ l_typ bf_typ
	global ct_typ ival v_options a_options
	global c_options po_typ cm_typ vb_typ
	global pr_typ vr_typ ur_typ xu_typ
	global ol_typ oct_typ nv_typ lt_typ

	set ol_typ $l_typ
	set oct_typ $ct_typ

	set a_options "-a -X"
	if {$l_typ==1}  { set a_options [format "%s -m" $a_options] }
	if {$lt_typ==1} { set a_options [format "%s -N pan.ltl" $a_options] }

	set Mbytes $ival(0)
	catch { set Mbytes [.av.memopts.choice0.e1 get] }

	# the Mstate scale resolution is in thousands: 2^10
	set Mstate [expr 10+[log $ival(1)]]
	catch { set Mstate [expr 10+[log [.av.memopts.choice1.e1 get]]] }
	set Mdepth $ival(2)
	catch { set Mdepth [.av.memopts.choice2.e1 get] }
	catch { set ival(0) "[.av.memopts.choice0.e1 get]" }
	catch { set ival(1) "[.av.memopts.choice1.e1 get]" }
	catch { set ival(2) "[.av.memopts.choice2.e1 get]" }
	catch { set ival(3) "[.av.memopts.choice3.e1 get]" }
	catch { set ival(4) "[.av.memopts.choice4.e1 get]" }
	catch { set ival(5) "[.av.memopts.choice5.e1 get]" }
	catch { set ival(7) "[.av.memopts.choice7.e1 get]" }

	if {$ct_typ == 2} {	;# hash-compact
		set c_options [format "-DHC -DMEMLIM=%d" $Mbytes]

		# in exhaustive mode: #hashtable ~~ #states

		set v_options "-X -m$Mdepth -w$Mstate"

		if {$Mstate >= $Mbytes} {
		catch {
		tk_messageBox -icon info \
			-message "The Estimated Statespace size exceeds \
the maximum that the Memory limit you set would allow."
		}
			return 0
		}
	} elseif {$ct_typ==1}	{
		set c_options [format "-DBITSTATE -DMEMLIM=%d" $Mbytes]

		# in supertrace mode: #bits ~~ 128x #states
		# (effectively the #bytes will be ~~ 16x #states)

		set Mstate [expr 7+$Mstate]
		set v_options "-X -m$Mdepth -w$Mstate"

		if {$Mstate-3 >= $Mbytes} {
		catch {
		tk_messageBox -icon info \
			-message "The Estimated Statespace size exceeds \
maximum allowed by the Memory limit that you set would allow."
		}
			return 0
		}
	} else {
		set c_options [format "-DMEMLIM=%d" $Mbytes]

		# in exhaustive mode: #hashtable ~~ #states

		set v_options "-X -m$Mdepth -w$Mstate"

		if {$Mstate >= $Mbytes} {
		catch {
		tk_messageBox -icon info \
			-message "The Estimated Statespace size exceeds \
the maximum that the Physical Memory limit allows."
		}
			return 0
		}
	}
	set c_options [format "-D_POSIX_SOURCE %s" $c_options]
	if {$an_typ==0}	{ set c_options [format "%s -DSAFETY" $c_options] }
	if {$an_typ==1 && $cp_typ==1}	{ set c_options [format "%s -DNP" $c_options] }
	if {$po_typ==0}	{ set c_options [format "%s -DNOREDUCE" $c_options] }
	if {$cm_typ==1 && $ct_typ!=1}	{ set c_options [format "%s -DCOLLAPSE" $c_options] }
	if {$vb_typ==1}	{ set c_options [format "%s -DCHECK" $c_options] }
	if {$nv_typ==0}	{ set c_options [format "%s -DNOCLAIM" $c_options] }
	if {$se_typ!=0}	{ set c_options [format "%s -DREACH" $c_options] }
	if {$bf_typ!=0}	{
		if {$an_typ != 0} {
			complain7
			set c_options [format "%s -DBFS -DSAFETY" $c_options]
		} else {
			set c_options [format "%s -DBFS" $c_options]
	}	}
	if {$xu_typ==0 && $po_typ!=0}	{ set c_options [format "%s -DXUSAFE" $c_options] }
	if {$pr_typ==1}	{ set c_options [format "%s -DPEG" $c_options] }
	if {$vr_typ==1}	{ set c_options [format "%s -DVAR_RANGES" $c_options] }
	if {$cyc_typ==1}	{
		set c_options [format "%s -DNFAIR=3" $c_options]
	} else {
		set c_options [format "%s -DNOFAIR" $c_options]
	}
	set foo $ival(3)
	catch { set foo [.av.memopts.choice3.e1 get] }

	if {[string first "-DBITSTATE" $c_options] > 0 && [string first "-DMA" $foo] > 0} {
		complain8
	}
	set c_options [format "%s %s" $c_options $foo ]

	set foo $ival(4)
	catch { set foo [.av.memopts.choice4.e1 get] }
	set v_options [format "%s %s" $v_options $foo ] 

	set foo $ival(5)
	catch { set foo [.av.memopts.choice.5.e1 get] }
	set a_options [format "%s %s" $a_options $foo ]

	if {$an_typ==0 && $as_typ==0} { set v_options [format "%s -A" $v_options] }
	if {$an_typ==0 && $ie_typ==0} { set v_options [format "%s -E" $v_options] }
	if {$an_typ==1 && $cp_typ==1} { set v_options [format "%s -l" $v_options] }
	if {$an_typ==1 && $cp_typ==2} { set v_options [format "%s -a" $v_options] }
	if {$cyc_typ==1} { set v_options [format "%s -f" $v_options] }
	if {$ur_typ==0}	{ set v_options [format "%s -n" $v_options] }
	if {$st_typ==1}	{ set v_options [format "%s -e" $v_options] }
	if {$se_typ!=0}	{ set v_options [format "%s -i" $v_options] }
	if {$et_typ==0}	{ set v_options [format "%s -c0" $v_options] }
	if {$et_typ==1}	{ set v_options [format "%s -c%s" $v_options $ival(6)] }
	if {$ct_typ==1 && $ival(7) != 2} { set v_options [format "%s -k%s" $v_options $ival(7)] }
	return 1
}

set mt 0
set skipmax 10

proc runval {havedest} {
	global Unix CC SPIN Fname PlaceSim
	global v_options a_options notignored
	global c_options Job_Done mt skipmax
	global stop s_typ vbox waitwhat not_warned_yet
	global LastGenerate LastCompile NextCompile

	set stop 0
	if {[bld_v_options] == 0} {
		advanced_val
		return
	}
	if {[winfo exists .v]} {
		set PlaceSim [wm geometry .v]
		destroy .v
	}
	catch {destroy .av}
	if {[string first "\?" $c_options] > 0} {
		add_log "error: undefined '?' in optional compiler directives"
		return
	}
	if {[string first "\?" $v_options] > 0} {
		add_log "error: undefined '?' in extra runtime options"
		return
	}
	add_log "<starting verification>"
	if {$havedest != "0"} {
		$havedest insert end "<starting verification>\n"
	}

	set nochange [no_change]
	if {$nochange == 0} { set LastGenerate "" }

	if {$LastGenerate == $a_options} {
		add_log "<no code regeneration necessary>"
		if {$havedest != "0"} {
			$havedest insert end "<no code regeneration necessary>\n"
		}
		set errmsg 0
	} else {
		set LastCompile ""
		add_log "$SPIN $a_options pan_in"; update
		if {$havedest != "0"} {
			$havedest insert end "$SPIN $a_options pan_in\n"
		}
		if {$Unix} {
			catch {eval exec $SPIN $a_options pan_in} errmsg
		} else {
			catch {eval exec $SPIN $a_options pan_in >&pan.tmp}
			set errmsg [msg_file pan.tmp 0]
		}
		if {[string length $errmsg]>0} {
			set foo [string first "Exit-Status 0" $errmsg]
			if {$foo<0} {
				add_log "$errmsg"
				if {$havedest != "0"} {
					$havedest insert end "$errmsg\n"
				}
				update
				return
			}
			incr foo -2
			set errmsg [string range $errmsg 0 $foo]
			add_log "$errmsg"
			if {$havedest != "0"} {
				$havedest insert end "$errmsg\n"
			}
	}	}
	set LastGenerate $a_options

	set NextCompile "$CC -o pan $c_options pan.c"

	if {$havedest != "0"} {
		catch { $havedest yview -pickplace end }
	}
	if {$LastCompile == $NextCompile && [file exists pan]} {
		add_log "<no recompilation necessary>"
		if {$havedest != "0"} {
			$havedest insert end "<no recompilation necessary>\n"
		}
		set errmsg 0
	} else {
		add_log $NextCompile
		if {$havedest != "0"} {
			$havedest insert end "$NextCompile\n"
		}
		catch {
			warner "Compiling" "Please wait until compilation of the \
executable produced by spin completes." 300
		}
		update
		if {$Unix} {
			rmfile "./pan"
			catch {eval exec $NextCompile >pan.tmp 2>pan.err}
		} else {
			rmfile "pan.exe"
			catch {eval exec $NextCompile >pan.tmp 2>pan.err}
		}

		set errmsg [msg_file pan.tmp 0]
		if {[string length $errmsg] == 0} {
			set errmsg [msg_file pan.err 0]
		} else {
			set errmsg "$errmsg\n[msg_file pan.err 0]"
		}

		catch {destroy .warn}

		auto_reset
		if {$Unix} {
			if {[auto_execok "./pan"] == "" \
			||  [auto_execok "./pan"] == 0} {
				add_log "$errmsg"
				add_log "compilation failed"
				if {$havedest != "0"} {
					$havedest insert end "<compilation failed>\n"
				}
				update
				return
			}
		} else {
			if {[auto_execok "pan"] == "" \
			||  [auto_execok "pan"] == 0} {
				add_log "$errmsg"
				add_log "compilation failed"
				if {$havedest != "0"} {
					$havedest insert end "<compilation failed>\n"
				}
				update
				return
	}	}	}

	set LastCompile $NextCompile
	set NextCompile ""

	if {$Unix} {
		set PREFIX "time ./pan -v"
	} else {
		set PREFIX "pan -v"
	}
	add_log "$PREFIX $v_options"; update
	if {$havedest != "0"} {
		$havedest insert end "$PREFIX $v_options\n"
		catch { $havedest yview -pickplace end }
	}
	set errmsg ""
	update
	rmfile pan.out
	set errmsg [catch {eval exec $PREFIX $v_options >&pan.out &}]
	if {$errmsg} {
		add_log "$errmsg"
		add_log "could not run verification"
		if {$havedest != "0"} {
			$havedest insert end "<could not run verification>\n"
		}
		update
		return
	}

	set not_warned_yet 1
	if {$havedest != "0"} {
		set vbox $havedest
	} else {
		set vv [mkbox "Verification Output" "VerOut" "$Fname.out" 80 20]
		set vbox .c$vv.z.t
	}
	update
	set mt 0
	after 5000 outcheck $vbox
	update
}

proc outcheck {vbox} {
	global stop where not_warned_yet runtime mt Unix Fname FG skipmax

	set firstline 1
	set have_trail 0
	set po_red_viol 0

	if {[winfo exists $vbox] == 0} {
		add_log "<verification output panel $vbox was closed>"
		return
	}

	set erline 0; set lnr 0
	set nomem 0; set nerr 0

	if {$stop == 0} {
	  catch { set nt [file mtime pan.out] }
	  if {$mt == $nt && $skipmax > 0} {
		incr skipmax -1
	  } else {
	  set mt $nt
	  set skipmax 10
	  set fd [open pan.out r]
	  while {[gets $fd line] > -1} {
		if {$firstline} {
			set firstline 0
			set nerr 0
			set trunc 0
			set nomem 0
			.inp.t tag remove hilite 0.0 end
			catch { $vbox delete 0.0 end }
			set lnr 0
		}
		catch { $vbox insert end "$line\n" }
		incr lnr
		catch { $vbox yview -pickplace end }
		update

		if {[string first "line" $line]>=0} {
			scan $line "\tline %d" where
			catch { src_line $where }
		}
		if {[string first "State-vector" $line] == 0 \
		||  ([string first "error:" $line] == 0 \
		&&   [string first "error: max search depth too small" $line] != 0)} {
			set stop 1	;# run must have completed
			set nerr [string first "errors:" $line]
			if {$nerr > 0} {
			set part [string range $line $nerr end]
			scan $part "errors: %d" nerr
			if {$nerr == 0} {
				catch { .tl.results.top.title configure\
					-text "Verification Result: valid" -fg $FG
				}
			} else {
				catch { .tl.results.top.title configure\
					-text "Verification Result: not valid" -fg red
				}
			}
			set erline $lnr
			incr erline -1
			}
		}
		if {[string first "search depth too small" $line]>0} {
			set trunc 1
		}
		if {[string first "wrote pan_in.trail" $line]>0} {
			set have_trail 1
		}
		if {[string first "violated: access to chan" $line]>0} {
			set po_red_viol 1
		}
		if {[string first "out of memory" $line]>0} {
			set nomem 1
		}
		if {[string first "A=atomic;" $line]>0} {
			set stop 1
		}
		update
	  }
	  catch "close $fd"
	} }
	if {$nomem || $po_red_viol} { set erline 0 }

	if {$stop || ($have_trail && $po_red_viol==0 && ($nerr>0 || $trunc>0))} {
		catch { $vbox yview 0.0 }
		add_log "<verification done>"
		if {$nerr > 0 || $trunc == 1 || $nomem == 1} {
			if {[file exists pan_in.trail]} {
				cpfile pan_in.trail $Fname.trail
			} elseif {[file exists pan_in.tra]} {
				cpfile pan_in.tra $Fname.trail
			}
			catch { repeatbox $nerr $trunc $nomem }
		}
	} else {
		if {$not_warned_yet} {
			set runtime 0
			set stop 0
			set line "Running verification -- waiting for output"
			catch { $vbox insert end "$line\n" }
			set line "\t(kill background process 'pan' to abort run)"
			catch { $vbox insert end "$line\n" }
			if {$Unix == 0} {
			set line "\t(use ctl-alt-del to kill pan)"
			catch { $vbox insert end "$line\n" }
			} else {
			set line "\t(use /bin/ps to find pid; then: kill -2 pid)"
			catch { $vbox insert end "$line\n" }
			catch { $vbox yview -pickplace end }
			}
			set not_warned_yet 0
		} else {
			incr runtime 5
			if {$stop} {
				add_log "<done>"
				return
			} else {
			if {$runtime%60 == 0} {
				set rt [expr $runtime / 60]
				add_log "verification now running for approx $rt min.."
			}}
			update
		}
		after 5000 outcheck $vbox
	}
}

proc src_line {s} {
	global FG BG
	scan $s %d tgt_lnr

	if {$tgt_lnr > 0} {
	.inp.t tag add hilite $tgt_lnr.0 $tgt_lnr.end
	.inp.t tag configure hilite -background $FG -foreground $BG
		if {$tgt_lnr > 10} {
	.inp.t yview -pickplace [expr $tgt_lnr-10]
		} else {
	.inp.t yview -pickplace [expr $tgt_lnr-1]
		}
	}
}

proc repeatbox { {nerr} {trunc} {nomem}} {
	global s_typ PlaceWarn whichsim

	if {$nerr <= 0 && $trunc <= 0 && $nomem <= 0} { return }

	catch {destroy .rep}
	toplevel .rep

	wm title .rep "Suggested Action"
	wm iconname .rep "Suggest"
	wm geometry .rep $PlaceWarn
	button .rep.b0 -text "Close" -command {destroy .rep}
	button .rep.b1 -text "Run Guided Simulation.." \
		-command {destroy .rep; Rewind }
	button .rep.b2 -text "Setup Guided Simulation.." \
		-command {destroy .rep; simulation }

	if {$nerr>0} {
		message .rep.t -width 500 -text "\
Optionally, repeat the run with a different search\
depth to find a shorter path to the error.

Or, perform a GUIDED simulation to retrace\
the error found in this run, and skip\
the first series of steps if the error was\
found at a depth greater than about 100 steps)."
		set s_typ 1
		set whichsim 0

		pack append .rep .rep.t {top expand fill}
		pack append .rep .rep.b0 {right}
		pack append .rep .rep.b1 {right}
		pack append .rep .rep.b2 {right}
	} else {

		if {$nomem>0} {
			message .rep.t -width 500 -text "\
Make sure the Physical Memory parameter (under Advanced\
Options) is set to the maximum physical memory available.\
If not, repeat the verification with the true maximum.\
(Don't set it higher than the physical limit though.)\
Otherwise, use compression, or switch to a\
Supertrace Verification."
		} else {

			if {$trunc} {

			message .rep.t -width 500 -text "\
If the search was incomplete (truncated)\
because the max search depth was too small,\
try to increase the depth limit (it is set\
in Advanced Options of the Verification Parameters\
Panel), and repeat the verification."
			}
		}
		pack append .rep .rep.t {top expand fill}
		pack append .rep .rep.b0 {right}
	}
}

# Main startup and arg processing
# this is at the end - to make sure all
# proc declarations were seen

if {$argc == 1} {
	set Fname "$argv"
	wm title . "SPIN CONTROL $xversion -- File: $Fname"
	cleanup 0
	cpfile $argv.trail pan_in.trail
	reopen
}

focus .inp.t
update