+++ /dev/null
-#!/bin/sh
-# 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-2005. #
-# See the README.html file for full installation notes. #
-# http://spinroot.com/spin/whatispin.html #
-#======================================================================#
-set xversion "5.1.0 -- 24 April 2008"
-
-# -- 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 "spin" ;# use a full path-name if necessary, e.g. c:/cygwin/bin/spin.exe
- set DOT "dot" ;# 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 . +41+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 5" $version] < 0 \
- && [string first "Spin Version 4" $version] < 0 \
- && [string first "Spin Version 3" $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]
-
- fconfigure $fd -translation lf
- 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 check_xsp {f} {
- set ff ${f}.xsp
- if [catch {set fd [open $ff r]} errmsg] {
- # add_log "no file $ff"
- return
- }
- add_log "reading $ff file"
- update
- while {[gets $fd line] > -1} {
- if {[string first "X:" $line] == 0} {
- set C [string range $line 3 end]
- add_log "X: $C"
- update
- catch { eval exec $C } errmsg
- if {$errmsg != ""} { add_log $errmsg }
- }
- if {[string first "L:" $line] == 0} {
- set N [string range $line 3 end]
- catch {.log.t configure -height $N -bg black -fg gold}
- }
- }
-}
-
-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
- raise .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 $pattern"
- 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 "statement" $line] < 0
- && [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 1
-set vv 1
-set qv 1
-set gvars 1
-set lvars 0
-set hide_q1 ""
-set hide_q2 ""
-set hide_q3 ""
-set PlaceSim "+200+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
-
- catch { .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
-
- raise .s
-}
-
-
-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
-
- catch { .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
-
- tkwait visibility .s
- raise .s
-}
-
-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" 71 11 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"
-
- raise .c$sbox
-
- 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 .] - 400] ;# button widths
- set maxh [expr [winfo screenheight .] - (5+120)] ;# borders+buttons
- set dbox2 \
- [mkcanvas "Sequence Chart" "msc" $maxx 5 1]
- .f$dbox2.c configure -height $maxh \
- -scrollregion "[expr -$XSZ/2] 0 \
- [expr $NPR*$XSZ] [expr 100+$SMX*$YSZ]"
-
- raise .f$dbox2
- }
-
- raise .c$sbox
-
- 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 ""
-
- update
- raise .c$sbox
- lower .
-
- 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"
-
- raise .c$sbox
-
- 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 i [string first "<merge" $line]
- if {$i > 0} {
- set line [string range $line 0 $i]
- }
-
- 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" 71 19 100 350] }
- } else {
- catch { .c$Vvbox.z.t delete 0.0 end }
- }
- if {$vv} {
- if {$gvars || $lvars} {
- raise .c$Vvbox
- 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
- if {$n > 0} { 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}
-
- tkwait visibility .v
- raise .v
-}
-
-set PlaceBasic "+200+10"
-set PlaceAdv "+150+10"
-
-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}
-
- tkwait visibility .v
- raise .v
-}
-
-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}
-
- raise .av
-}
-
-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
-
- check_xsp $argv
-}
-
-focus .inp.t
-update
projects / lttv.git / blobdiff