# The next line is executed by /bin/sh, but not tcl \
exec wish "$0" -- $*
## iSpin GUI -- http::/spinroot.com/
## (c) 2010-2014 All Rights Reserved
## This software is for educational purposes only.
## No guarantee whatsoever is expressed or implied
## by the distribution of this code.
package re Tk; # MH, tclkit8.6.4
wm title . "ispin"
wm geometry . 1200x600+20+20
set xversion "iSpin Version 1.1.4 -- 27 November 2014"
set version "Spin Version unknown"; # updated below
set Unix 1; # updated below
### Tools
set SPIN spin ;# essential
set CC gcc ;# essential
set DOT dot ;# recommended, for automata view
# set DOT "C:/Program\ Files\ \(x86\)/Graphviz2.36/bin/dot"
set SWARM swarm ;# optional, for swarm verification panel
set CURL curl ;# optional, for version check information
set CC_alt1 gcc-4
set CC_alt2 gcc-3
set RM "rm -f"
set KILL "kill -2"
## check if we have the right version of Spin
if {[auto_execok $SPIN] == "" \
|| [auto_execok $SPIN] == 0} {
puts "No executable $SPIN found..."
puts "iSpin requires Spin Version 6.0 or later"
exit 0
} else {
catch { set fd [open "|$SPIN -V" r] } errmsg
if {$fd == -1} {
puts "$errmsg"
exit 0
} else {
set version "Spin Version unknown"
if {[gets $fd line] > -1} {
set version "$line"
}
catch "close $fd"
}
if {[string first "Spin Version " $version] < 0 \
|| [string first "Spin Version 5" $version] >= 0 \
|| [string first "Spin Version 4" $version] >= 0 \
|| [string first "Spin Version 3" $version] >= 0 } {
puts "iSpin requires Spin Version 6.0 or later"
puts "You have: $version"
exit 0
} }
if {[file isfile $CC] == 0} { ;# symbolic link
if {[auto_execok $CC_alt1] != ""} {
set CC $CC_alt1
} elseif {[auto_execok $CC_alt2] != ""} {
set CC $CC_alt2
} }
if [info exists tcl_platform] {
set sys $tcl_platform(platform)
if {[string match windows $sys]} {
set Unix 0 ;# Windows
} }
### Some other configurable items
set ScrollBarSize 10
### Colors
set MBG azure ;# menu
set MFG black
set XBB ivory ;# MSC canvas color
set XBG black ;# MSC rectangle border
set XFG gold ;# MSC rectangles
set XTX black ;# MSC text
set XAR blue ;# MSC arrows
set XPR gray ;# MSC process line color
set TBG azure ;#WhiteSmoke ;# text window
set TFG black
set CBG black ;# command window
set CFG azure ;# gold
set NBG darkblue ;# main tabs
set NFG gold
set SFG red ;# text selections - standout from TBG
set LTLbg darkblue
set LTL_Panel 0 ;# mostly overtaken by extensions in 6.0
set V_Panel_1 0 ;# Advanced verification options 1: Error trapping
set V_Panel_3 0 ;# ditto 3: Default Parameters
### Fonts
set HV0 "helvetica 11"
set HV1 "helvetica 13"
### end of configurable items ##########################################
## ##
## The first part of this code is based on the BWidget-1.9.2 package ##
## To skip ahead to where the iSpin specific code starts, ##
## search for "iSpin GUI code" which starts about half-way down ##
## ##
########################################################################
#######
## The BWidget Toolkit comes with the following
## license text that is reproduced here.
#######
## BWidget ToolKit
## Copyright (c) 1998-1999 UNIFIX.
## Copyright (c) 2001-2002 ActiveState Corp.
##
## The following terms apply to all files associated with the software
## unless explicitly disclaimed in individual files.
##
## The authors hereby grant permission to use, copy, modify, distribute,
## and license this software and its documentation for any purpose, provided
## that existing copyright notices are retained in all copies and that this
## notice is included verbatim in any distributions. No written agreement,
## license, or royalty fee is required for any of the authorized uses.
## Modifications to this software may be copyrighted by their authors
## and need not follow the licensing terms described here, provided that
## the new terms are clearly indicated on the first page of each file where
## they apply.
##
## IN NO EVENT SHALL THE AUTHORS OR DISTRIBUTORS BE LIABLE TO ANY PARTY
## FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES
## ARISING OUT OF THE USE OF THIS SOFTWARE, ITS DOCUMENTATION, OR ANY
## DERIVATIVES THEREOF, EVEN IF THE AUTHORS HAVE BEEN ADVISED OF THE
## POSSIBILITY OF SUCH DAMAGE.
##
## THE AUTHORS AND DISTRIBUTORS SPECIFICALLY DISCLAIM ANY WARRANTIES,
## INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY,
## FITNESS FOR A PARTICULAR PURPOSE, AND NON-INFRINGEMENT. THIS SOFTWARE
## IS PROVIDED ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE
## NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR
## MODIFICATIONS.
##
## GOVERNMENT USE: If you are acquiring this software on behalf of the
## U.S. government, the Government shall have only "Restricted Rights"
## in the software and related documentation as defined in the Federal
## Acquisition Regulations (FARs) in Clause 52.227.19 (c) (2). If you
## are acquiring the software on behalf of the Department of Defense, the
## software shall be classified as "Commercial Computer Software" and the
## Government shall have only "Restricted Rights" as defined in Clause
## 252.227-7013 (c) (1) of DFARs. Notwithstanding the foregoing, the
## authors grant the U.S. Government and others acting in its behalf
## permission to use and distribute the software in accordance with the
## terms specified in this license.
#######
namespace eval Widget {}
proc Widget::_opt_defaults {{prio widgetDefault}} {
if {$::tcl_version >= 8.4} {
set plat [tk windowingsystem]
} else {
set plat $::tcl_platform(platform)
}
switch -exact $plat {
"aqua" {
}
"win32" -
"windows" {
option add *ListBox.background SystemWindow $prio
option add *Dialog.padY 0 $prio
option add *Dialog.anchor e $prio
}
"x11" -
default {
option add *Scrollbar.width 12 $prio
option add *Scrollbar.borderWidth 1 $prio
option add *Dialog.separator 1 $prio
option add *MainFrame.relief raised $prio
option add *MainFrame.separator none $prio
}
}
}
Widget::_opt_defaults
bind Entry <<TraverseIn>> { %W selection range 0 end; %W icursor end }
bind all <Key-Tab> { Widget::traverseTo [Widget::focusNext %W] }
bind all <<PrevWindow>> { Widget::traverseTo [Widget::focusPrev %W] }
# ----------------------------------------------------------------------------
# widget.tcl -- part of Unifix BWidget Toolkit
# ----------------------------------------------------------------------------
# Uses newer string operations
package require Tcl 8.1.1
namespace eval Widget {
variable _optiontype
variable _class
variable _tk_widget
# This controls whether we try to use themed widgets from Tile
variable _theme 0
variable _aqua [expr {($::tcl_version >= 8.4) &&
[string equal [tk windowingsystem] "aqua"]}]
array set _optiontype {
TkResource Widget::_test_tkresource
BwResource Widget::_test_bwresource
Enum Widget::_test_enum
Int Widget::_test_int
Boolean Widget::_test_boolean
String Widget::_test_string
Flag Widget::_test_flag
Synonym Widget::_test_synonym
Color Widget::_test_color
Padding Widget::_test_padding
}
proc use {} {}
}
proc Widget::tkinclude { class tkwidget subpath args } {
foreach {cmd lopt} $args {
switch -- $cmd {
remove {
foreach option $lopt {
set remove($option) 1
}
}
include {
foreach option $lopt {
set include($option) 1
}
}
prefix {
set prefix [lindex $lopt 0]
foreach option [lrange $lopt 1 end] {
set rename($option) "-$prefix[string range $option 1 end]"
}
}
rename -
readonly -
initialize {
array set $cmd $lopt
}
default {
return -code error "invalid argument \"$cmd\""
}
}
}
namespace eval $class {}
upvar 0 ${class}::opt classopt
upvar 0 ${class}::map classmap
upvar 0 ${class}::map$subpath submap
upvar 0 ${class}::optionExports exports
set foo [$tkwidget ".ericFoo###"]
# create resources informations from tk widget resources
foreach optdesc [_get_tkwidget_options $tkwidget] {
set option [lindex $optdesc 0]
if { (![info exists include] || [info exists include($option)]) &&
![info exists remove($option)] } {
if { [llength $optdesc] == 3 } {
# option is a synonym
set syn [lindex $optdesc 1]
if { ![info exists remove($syn)] } {
# original option is not removed
if { [info exists rename($syn)] } {
set classopt($option) [list Synonym $rename($syn)]
} else {
set classopt($option) [list Synonym $syn]
}
}
} else {
if { [info exists rename($option)] } {
set realopt $option
set option $rename($option)
} else {
set realopt $option
}
if { [info exists initialize($option)] } {
set value $initialize($option)
} else {
set value [lindex $optdesc 1]
}
if { [info exists readonly($option)] } {
set ro $readonly($option)
} else {
set ro 0
}
set classopt($option) \
[list TkResource $value $ro [list $tkwidget $realopt]]
# Add an option database entry for this option
set optionDbName ".[lindex [_configure_option $realopt ""] 0]"
if { ![string equal $subpath ":cmd"] } {
set optionDbName "$subpath$optionDbName"
}
option add *${class}$optionDbName $value widgetDefault
lappend exports($option) "$optionDbName"
# Store the forward and backward mappings for this
# option <-> realoption pair
lappend classmap($option) $subpath "" $realopt
set submap($realopt) $option
}
}
}
::destroy $foo
}
proc Widget::bwinclude { class subclass subpath args } {
foreach {cmd lopt} $args {
switch -- $cmd {
remove {
foreach option $lopt {
set remove($option) 1
}
}
include {
foreach option $lopt {
set include($option) 1
}
}
prefix {
set prefix [lindex $lopt 0]
foreach option [lrange $lopt 1 end] {
set rename($option) "-$prefix[string range $option 1 end]"
}
}
rename -
readonly -
initialize {
array set $cmd $lopt
}
default {
return -code error "invalid argument \"$cmd\""
}
}
}
namespace eval $class {}
upvar 0 ${class}::opt classopt
upvar 0 ${class}::map classmap
upvar 0 ${class}::map$subpath submap
upvar 0 ${class}::optionExports exports
upvar 0 ${subclass}::opt subclassopt
upvar 0 ${subclass}::optionExports subexports
# create resources informations from BWidget resources
foreach {option optdesc} [array get subclassopt] {
set subOption $option
if { (![info exists include] || [info exists include($option)]) &&
![info exists remove($option)] } {
set type [lindex $optdesc 0]
if { [string equal $type "Synonym"] } {
# option is a synonym
set syn [lindex $optdesc 1]
if { ![info exists remove($syn)] } {
if { [info exists rename($syn)] } {
set classopt($option) [list Synonym $rename($syn)]
} else {
set classopt($option) [list Synonym $syn]
}
}
} else {
if { [info exists rename($option)] } {
set realopt $option
set option $rename($option)
} else {
set realopt $option
}
if { [info exists initialize($option)] } {
set value $initialize($option)
} else {
set value [lindex $optdesc 1]
}
if { [info exists readonly($option)] } {
set ro $readonly($option)
} else {
set ro [lindex $optdesc 2]
}
set classopt($option) \
[list $type $value $ro [lindex $optdesc 3]]
# Add an option database entry for this option
foreach optionDbName $subexports($subOption) {
if { ![string equal $subpath ":cmd"] } {
set optionDbName "$subpath$optionDbName"
}
# Only add the option db entry if we are overriding the
# normal widget default
if { [info exists initialize($option)] } {
option add *${class}$optionDbName $value \
widgetDefault
}
lappend exports($option) "$optionDbName"
}
# Store the forward and backward mappings for this
# option <-> realoption pair
lappend classmap($option) $subpath $subclass $realopt
set submap($realopt) $option
}
}
}
}
proc Widget::declare { class optlist } {
variable _optiontype
namespace eval $class {}
upvar 0 ${class}::opt classopt
upvar 0 ${class}::optionExports exports
upvar 0 ${class}::optionClass optionClass
foreach optdesc $optlist {
set option [lindex $optdesc 0]
set optdesc [lrange $optdesc 1 end]
set type [lindex $optdesc 0]
if { ![info exists _optiontype($type)] } {
# invalid resource type
return -code error "invalid option type \"$type\""
}
if { [string equal $type "Synonym"] } {
# test existence of synonym option
set syn [lindex $optdesc 1]
if { ![info exists classopt($syn)] } {
return -code error "unknow option \"$syn\" for Synonym \"$option\""
}
set classopt($option) [list Synonym $syn]
continue
}
# all other resource may have default value, readonly flag and
# optional arg depending on type
set value [lindex $optdesc 1]
set ro [lindex $optdesc 2]
set arg [lindex $optdesc 3]
if { [string equal $type "BwResource"] } {
# We don't keep BwResource. We simplify to type of sub BWidget
set subclass [lindex $arg 0]
set realopt [lindex $arg 1]
if { ![string length $realopt] } {
set realopt $option
}
upvar 0 ${subclass}::opt subclassopt
if { ![info exists subclassopt($realopt)] } {
return -code error "unknow option \"$realopt\""
}
set suboptdesc $subclassopt($realopt)
if { $value == "" } {
# We initialize default value
set value [lindex $suboptdesc 1]
}
set type [lindex $suboptdesc 0]
set ro [lindex $suboptdesc 2]
set arg [lindex $suboptdesc 3]
set optionDbName ".[lindex [_configure_option $option ""] 0]"
option add *${class}${optionDbName} $value widgetDefault
set exports($option) $optionDbName
set classopt($option) [list $type $value $ro $arg]
continue
}
# retreive default value for TkResource
if { [string equal $type "TkResource"] } {
set tkwidget [lindex $arg 0]
set foo [$tkwidget ".ericFoo##"]
set realopt [lindex $arg 1]
if { ![string length $realopt] } {
set realopt $option
}
set tkoptions [_get_tkwidget_options $tkwidget]
if { ![string length $value] } {
# We initialize default value
set ind [lsearch $tkoptions [list $realopt *]]
set value [lindex [lindex $tkoptions $ind] end]
}
set optionDbName ".[lindex [_configure_option $option ""] 0]"
option add *${class}${optionDbName} $value widgetDefault
set exports($option) $optionDbName
set classopt($option) [list TkResource $value $ro \
[list $tkwidget $realopt]]
set optionClass($option) [lindex [$foo configure $realopt] 1]
::destroy $foo
continue
}
set optionDbName ".[lindex [_configure_option $option ""] 0]"
option add *${class}${optionDbName} $value widgetDefault
set exports($option) $optionDbName
# for any other resource type, we keep original optdesc
set classopt($option) [list $type $value $ro $arg]
}
}
proc Widget::define { class filename args } {
variable ::BWidget::use
set use($class) $args
set use($class,file) $filename
lappend use(classes) $class
if {[set x [lsearch -exact $args "-classonly"]] > -1} {
set args [lreplace $args $x $x]
} else {
interp alias {} ::${class} {} ${class}::create
proc ::${class}::use {} {}
bind $class <Destroy> [list Widget::destroy %W]
}
foreach class $args { ${class}::use }
}
proc Widget::create { class path {rename 1} } {
if {$rename} { rename $path ::$path:cmd }
proc ::$path { cmd args } \
[subst {return \[eval \[linsert \$args 0 ${class}::\$cmd [list $path]\]\]}]
return $path
}
proc Widget::addmap { class subclass subpath options } {
upvar 0 ${class}::opt classopt
upvar 0 ${class}::optionExports exports
upvar 0 ${class}::optionClass optionClass
upvar 0 ${class}::map classmap
upvar 0 ${class}::map$subpath submap
foreach {option realopt} $options {
if { ![string length $realopt] } {
set realopt $option
}
set val [lindex $classopt($option) 1]
set optDb ".[lindex [_configure_option $realopt ""] 0]"
if { ![string equal $subpath ":cmd"] } {
set optDb "$subpath$optDb"
}
option add *${class}${optDb} $val widgetDefault
lappend exports($option) $optDb
# Store the forward and backward mappings for this
# option <-> realoption pair
lappend classmap($option) $subpath $subclass $realopt
set submap($realopt) $option
}
}
proc Widget::syncoptions { class subclass subpath options } {
upvar 0 ${class}::sync classync
foreach {option realopt} $options {
if { ![string length $realopt] } {
set realopt $option
}
set classync($option) [list $subpath $subclass $realopt]
}
}
proc Widget::init { class path options } {
variable _inuse
variable _class
variable _optiontype
upvar 0 ${class}::opt classopt
upvar 0 ${class}::$path:opt pathopt
upvar 0 ${class}::$path:mod pathmod
upvar 0 ${class}::map classmap
upvar 0 ${class}::$path:init pathinit
if { [info exists pathopt] } {
unset pathopt
}
if { [info exists pathmod] } {
unset pathmod
}
set fpath $path
set rdbclass [string map [list :: ""] $class]
if { ![winfo exists $path] } {
set fpath ".#BWidget.#Class#$class"
# encapsulation frame to not pollute '.' childspace
if {![winfo exists ".#BWidget"]} { frame ".#BWidget" }
if { ![winfo exists $fpath] } {
frame $fpath -class $rdbclass
}
}
foreach {option optdesc} [array get classopt] {
set pathmod($option) 0
if { [info exists classmap($option)] } {
continue
}
set type [lindex $optdesc 0]
if { [string equal $type "Synonym"] } {
continue
}
if { [string equal $type "TkResource"] } {
set alt [lindex [lindex $optdesc 3] 1]
} else {
set alt ""
}
set optdb [lindex [_configure_option $option $alt] 0]
set def [option get $fpath $optdb $rdbclass]
if { [string length $def] } {
set pathopt($option) $def
} else {
set pathopt($option) [lindex $optdesc 1]
}
}
if {![info exists _inuse($class)]} { set _inuse($class) 0 }
incr _inuse($class)
set _class($path) $class
foreach {option value} $options {
if { ![info exists classopt($option)] } {
unset pathopt
unset pathmod
return -code error "unknown option \"$option\""
}
set optdesc $classopt($option)
set type [lindex $optdesc 0]
if { [string equal $type "Synonym"] } {
set option [lindex $optdesc 1]
set optdesc $classopt($option)
set type [lindex $optdesc 0]
}
# this may fail if a wrong enum element was used
if {[catch {
$_optiontype($type) $option $value [lindex $optdesc 3]
} msg]} {
if {[info exists pathopt]} {
unset pathopt
}
unset pathmod
return -code error $msg
}
set pathopt($option) $msg
set pathinit($option) $pathopt($option)
}
}
proc Widget::parseArgs {class options} {
variable _optiontype
upvar 0 ${class}::opt classopt
upvar 0 ${class}::map classmap
foreach {option val} $options {
if { ![info exists classopt($option)] } {
error "unknown option \"$option\""
}
set optdesc $classopt($option)
set type [lindex $optdesc 0]
if { [string equal $type "Synonym"] } {
set option [lindex $optdesc 1]
set optdesc $classopt($option)
set type [lindex $optdesc 0]
}
if { [string equal $type "TkResource"] } {
# Make sure that the widget used for this TkResource exists
Widget::_get_tkwidget_options [lindex [lindex $optdesc 3] 0]
}
set val [$_optiontype($type) $option $val [lindex $optdesc 3]]
if { [info exists classmap($option)] } {
foreach {subpath subclass realopt} $classmap($option) {
lappend maps($subpath) $realopt $val
}
} else {
lappend maps($class) $option $val
}
}
return [array get maps]
}
proc Widget::initFromODB {class path options} {
variable _inuse
variable _class
upvar 0 ${class}::$path:opt pathopt
upvar 0 ${class}::$path:mod pathmod
upvar 0 ${class}::map classmap
if { [info exists pathopt] } {
unset pathopt
}
if { [info exists pathmod] } {
unset pathmod
}
set fpath [_get_window $class $path]
set rdbclass [string map [list :: ""] $class]
if { ![winfo exists $path] } {
set fpath ".#BWidget.#Class#$class"
# encapsulation frame to not pollute '.' childspace
if {![winfo exists ".#BWidget"]} { frame ".#BWidget" }
if { ![winfo exists $fpath] } {
frame $fpath -class $rdbclass
}
}
foreach {option optdesc} [array get ${class}::opt] {
set pathmod($option) 0
if { [info exists classmap($option)] } {
continue
}
set type [lindex $optdesc 0]
if { [string equal $type "Synonym"] } {
continue
}
if { [string equal $type "TkResource"] } {
set alt [lindex [lindex $optdesc 3] 1]
} else {
set alt ""
}
set optdb [lindex [_configure_option $option $alt] 0]
set def [option get $fpath $optdb $rdbclass]
if { [string length $def] } {
set pathopt($option) $def
} else {
set pathopt($option) [lindex $optdesc 1]
}
}
if {![info exists _inuse($class)]} { set _inuse($class) 0 }
incr _inuse($class)
set _class($path) $class
array set pathopt $options
}
proc Widget::destroy { path } {
variable _class
variable _inuse
if {![info exists _class($path)]} { return }
set class $_class($path)
upvar 0 ${class}::$path:opt pathopt
upvar 0 ${class}::$path:mod pathmod
upvar 0 ${class}::$path:init pathinit
if {[info exists _inuse($class)]} { incr _inuse($class) -1 }
if {[info exists pathopt]} {
unset pathopt
}
if {[info exists pathmod]} {
unset pathmod
}
if {[info exists pathinit]} {
unset pathinit
}
if {![string equal [info commands $path] ""]} { rename $path "" }
## Unset any variables used in this widget.
foreach var [info vars ::${class}::$path:*] { unset $var }
unset _class($path)
}
proc Widget::configure { path options } {
set len [llength $options]
if { $len <= 1 } {
return [_get_configure $path $options]
} elseif { $len % 2 == 1 } {
return -code error "incorrect number of arguments"
}
variable _class
variable _optiontype
set class $_class($path)
upvar 0 ${class}::opt classopt
upvar 0 ${class}::map classmap
upvar 0 ${class}::$path:opt pathopt
upvar 0 ${class}::$path:mod pathmod
set window [_get_window $class $path]
foreach {option value} $options {
if { ![info exists classopt($option)] } {
return -code error "unknown option \"$option\""
}
set optdesc $classopt($option)
set type [lindex $optdesc 0]
if { [string equal $type "Synonym"] } {
set option [lindex $optdesc 1]
set optdesc $classopt($option)
set type [lindex $optdesc 0]
}
if { ![lindex $optdesc 2] } {
set newval [$_optiontype($type) $option $value [lindex $optdesc 3]]
if { [info exists classmap($option)] } {
set window [_get_window $class $window]
foreach {subpath subclass realopt} $classmap($option) {
if { [string length $subclass] && ! [string equal $subclass ":cmd"] } {
if { [string equal $subpath ":cmd"] } {
set subpath ""
}
set curval [${subclass}::cget $window$subpath $realopt]
${subclass}::configure $window$subpath $realopt $newval
} else {
set curval [$window$subpath cget $realopt]
$window$subpath configure $realopt $newval
}
}
} else {
set curval $pathopt($option)
set pathopt($option) $newval
}
set pathmod($option) [expr {![string equal $newval $curval]}]
}
}
return {}
}
proc Widget::cget { path option } {
variable _class
if { ![info exists _class($path)] } {
return -code error "unknown widget $path"
}
set class $_class($path)
if { ![info exists ${class}::opt($option)] } {
return -code error "unknown option \"$option\""
}
set optdesc [set ${class}::opt($option)]
set type [lindex $optdesc 0]
if {[string equal $type "Synonym"]} {
set option [lindex $optdesc 1]
}
if { [info exists ${class}::map($option)] } {
foreach {subpath subclass realopt} [set ${class}::map($option)] {break}
set path "[_get_window $class $path]$subpath"
return [$path cget $realopt]
}
upvar 0 ${class}::$path:opt pathopt
set pathopt($option)
}
proc Widget::subcget { path subwidget } {
variable _class
set class $_class($path)
upvar 0 ${class}::$path:opt pathopt
upvar 0 ${class}::map$subwidget submap
upvar 0 ${class}::$path:init pathinit
set result {}
foreach realopt [array names submap] {
if { [info exists pathinit($submap($realopt))] } {
lappend result $realopt $pathopt($submap($realopt))
}
}
return $result
}
proc Widget::hasChanged { path option pvalue } {
variable _class
upvar $pvalue value
set class $_class($path)
upvar 0 ${class}::$path:mod pathmod
set value [Widget::cget $path $option]
set result $pathmod($option)
set pathmod($option) 0
return $result
}
proc Widget::hasChangedX { path option args } {
variable _class
set class $_class($path)
upvar 0 ${class}::$path:mod pathmod
set result $pathmod($option)
set pathmod($option) 0
foreach option $args {
lappend result $pathmod($option)
set pathmod($option) 0
}
set result
}
proc Widget::setoption { path option value } {
Widget::configure $path [list $option $value]
}
proc Widget::getoption { path option } {
return [Widget::cget $path $option]
}
proc Widget::getMegawidgetOption {path option} {
variable _class
set class $_class($path)
upvar 0 ${class}::${path}:opt pathopt
set pathopt($option)
}
proc Widget::setMegawidgetOption {path option value} {
variable _class
set class $_class($path)
upvar 0 ${class}::${path}:opt pathopt
set pathopt($option) $value
}
proc Widget::_get_window { class path } {
set idx [string last "#" $path]
if { $idx != -1 && [string equal [string range $path [expr {$idx+1}] end] $class] } {
return [string range $path 0 [expr {$idx-1}]]
} else {
return $path
}
}
proc Widget::_get_configure { path options } {
variable _class
set class $_class($path)
upvar 0 ${class}::opt classopt
upvar 0 ${class}::map classmap
upvar 0 ${class}::$path:opt pathopt
upvar 0 ${class}::$path:mod pathmod
set len [llength $options]
if { !$len } {
set result {}
foreach option [lsort [array names classopt]] {
set optdesc $classopt($option)
set type [lindex $optdesc 0]
if { [string equal $type "Synonym"] } {
set syn $option
set option [lindex $optdesc 1]
set optdesc $classopt($option)
set type [lindex $optdesc 0]
} else {
set syn ""
}
if { [string equal $type "TkResource"] } {
set alt [lindex [lindex $optdesc 3] 1]
} else {
set alt ""
}
set res [_configure_option $option $alt]
if { $syn == "" } {
lappend result [concat $option $res [list [lindex $optdesc 1]] [list [cget $path $option]]]
} else {
lappend result [list $syn [lindex $res 0]]
}
}
return $result
} elseif { $len == 1 } {
set option [lindex $options 0]
if { ![info exists classopt($option)] } {
return -code error "unknown option \"$option\""
}
set optdesc $classopt($option)
set type [lindex $optdesc 0]
if { [string equal $type "Synonym"] } {
set option [lindex $optdesc 1]
set optdesc $classopt($option)
set type [lindex $optdesc 0]
}
if { [string equal $type "TkResource"] } {
set alt [lindex [lindex $optdesc 3] 1]
} else {
set alt ""
}
set res [_configure_option $option $alt]
return [concat $option $res [list [lindex $optdesc 1]] [list [cget $path $option]]]
}
}
proc Widget::_configure_option { option altopt } {
variable _optiondb
variable _optionclass
if { [info exists _optiondb($option)] } {
set optdb $_optiondb($option)
} else {
set optdb [string range $option 1 end]
}
if { [info exists _optionclass($option)] } {
set optclass $_optionclass($option)
} elseif { [string length $altopt] } {
if { [info exists _optionclass($altopt)] } {
set optclass $_optionclass($altopt)
} else {
set optclass [string range $altopt 1 end]
}
} else {
set optclass [string range $option 1 end]
}
return [list $optdb $optclass]
}
proc Widget::_get_tkwidget_options { tkwidget } {
variable _tk_widget
variable _optiondb
variable _optionclass
set widget ".#BWidget.#$tkwidget"
# encapsulation frame to not pollute '.' childspace
if {![winfo exists ".#BWidget"]} { frame ".#BWidget" }
if { ![winfo exists $widget] || ![info exists _tk_widget($tkwidget)] } {
set widget [$tkwidget $widget]
# JDC: Withdraw toplevels, otherwise visible
if {[string equal $tkwidget "toplevel"]} {
wm withdraw $widget
}
set config [$widget configure]
foreach optlist $config {
set opt [lindex $optlist 0]
if { [llength $optlist] == 2 } {
set refsyn [lindex $optlist 1]
# search for class
set idx [lsearch $config [list * $refsyn *]]
if { $idx == -1 } {
if { [string index $refsyn 0] == "-" } {
# search for option (tk8.1b1 bug)
set idx [lsearch $config [list $refsyn * *]]
} else {
# last resort
set idx [lsearch $config [list -[string tolower $refsyn] * *]]
}
if { $idx == -1 } {
# fed up with "can't read classopt()"
return -code error "can't find option of synonym $opt"
}
}
set syn [lindex [lindex $config $idx] 0]
# JDC: used 4 (was 3) to get def from optiondb
set def [lindex [lindex $config $idx] 4]
lappend _tk_widget($tkwidget) [list $opt $syn $def]
} else {
# JDC: used 4 (was 3) to get def from optiondb
set def [lindex $optlist 4]
lappend _tk_widget($tkwidget) [list $opt $def]
set _optiondb($opt) [lindex $optlist 1]
set _optionclass($opt) [lindex $optlist 2]
}
}
}
return $_tk_widget($tkwidget)
}
proc Widget::_test_tkresource { option value arg } {
foreach {tkwidget realopt} $arg break
set path ".#BWidget.#$tkwidget"
set old [$path cget $realopt]
$path configure $realopt $value
set res [$path cget $realopt]
$path configure $realopt $old
return $res
}
proc Widget::_test_bwresource { option value arg } {
return -code error "bad option type BwResource in widget"
}
proc Widget::_test_synonym { option value arg } {
return -code error "bad option type Synonym in widget"
}
proc Widget::_test_color { option value arg } {
if {[catch {winfo rgb . $value} color]} {
return -code error "bad $option value \"$value\": must be a colorname \
or #RRGGBB triplet"
}
return $value
}
proc Widget::_test_string { option value arg } {
set value
}
proc Widget::_test_flag { option value arg } {
set len [string length $value]
set res ""
for {set i 0} {$i < $len} {incr i} {
set c [string index $value $i]
if { [string first $c $arg] == -1 } {
return -code error "bad [string range $option 1 end] value \"$value\": characters must be in \"$arg\""
}
if { [string first $c $res] == -1 } {
append res $c
}
}
return $res
}
proc Widget::_test_enum { option value arg } {
if { [lsearch $arg $value] == -1 } {
set last [lindex $arg end]
set sub [lreplace $arg end end]
if { [llength $sub] } {
set str "[join $sub ", "] or $last"
} else {
set str $last
}
return -code error "bad [string range $option 1 end] value \"$value\": must be $str"
}
return $value
}
proc Widget::_test_int { option value arg } {
if { ![string is int -strict $value] || \
([string length $arg] && \
![expr [string map [list %d $value] $arg]]) } {
return -code error "bad $option value\
\"$value\": must be integer ($arg)"
}
return $value
}
proc Widget::_test_boolean { option value arg } {
if { ![string is boolean -strict $value] } {
return -code error "bad $option value \"$value\": must be boolean"
}
# Get the canonical form of the boolean value (1 for true, 0 for false)
return [string is true $value]
}
proc Widget::_test_padding { option values arg } {
set len [llength $values]
if {$len < 1 || $len > 2} {
return -code error "bad pad value \"$values\":\
must be positive screen distance"
}
foreach value $values {
if { ![string is int -strict $value] || \
([string length $arg] && \
![expr [string map [list %d $value] $arg]]) } {
return -code error "bad pad value \"$value\":\
must be positive screen distance ($arg)"
}
}
return $values
}
proc Widget::_get_padding { path option {index 0} } {
set pad [Widget::cget $path $option]
set val [lindex $pad $index]
if {$val == ""} { set val [lindex $pad 0] }
return $val
}
proc Widget::focusNext { w } {
set cur $w
while 1 {
# Descend to just before the first child of the current widget.
set parent $cur
set children [winfo children $cur]
set i -1
# Look for the next sibling that isn't a top-level.
while 1 {
incr i
if {$i < [llength $children]} {
set cur [lindex $children $i]
if {[string equal [winfo toplevel $cur] $cur]} {
continue
} else {
break
}
}
set cur $parent
if {[string equal [winfo toplevel $cur] $cur]} {
break
}
set parent [winfo parent $parent]
set children [winfo children $parent]
set i [lsearch -exact $children $cur]
}
if {[string equal $cur $w] || [focusOK $cur]} {
return $cur
}
}
}
proc Widget::focusPrev { w } {
set cur $w
set origParent [winfo parent $w]
while 1 {
if {[string equal [winfo toplevel $cur] $cur]} {
set parent $cur
set children [winfo children $cur]
set i [llength $children]
} else {
set parent [winfo parent $cur]
set children [winfo children $parent]
set i [lsearch -exact $children $cur]
}
while {$i > 0} {
incr i -1
set cur [lindex $children $i]
if {[string equal [winfo toplevel $cur] $cur]} {
continue
}
set parent $cur
set children [winfo children $parent]
set i [llength $children]
}
set cur $parent
if {[string equal $cur $w]} {
return $cur
}
if {[string equal $cur $origParent]
&& [info procs ::$origParent] != ""} {
continue
}
if {[focusOK $cur]} {
return $cur
}
}
}
proc Widget::focusOK { w } {
set code [catch {$w cget -takefocus} value]
if { $code == 1 } {
return 0
}
if {($code == 0) && ($value != "")} {
if {$value == 0} {
return 0
} elseif {$value == 1} {
return [winfo viewable $w]
} else {
set value [uplevel \#0 $value $w]
if {$value != ""} {
return $value
}
}
}
if {![winfo viewable $w]} {
return 0
}
set code [catch {$w cget -state} value]
if {($code == 0) && ($value == "disabled")} {
return 0
}
set code [catch {$w cget -editable} value]
if {($code == 0) && ($value == 0)} {
return 0
}
set top [winfo toplevel $w]
foreach tags [bindtags $w] {
if { ![string equal $tags $top] &&
![string equal $tags "all"] &&
[regexp Key [bind $tags]] } {
return 1
}
}
return 0
}
proc Widget::traverseTo { w } {
set focus [focus]
if {![string equal $focus ""]} {
event generate $focus <<TraverseOut>>
}
focus $w
event generate $w <<TraverseIn>>
}
proc Widget::getVariable { path varName {newVarName ""} } {
variable _class
set class $_class($path)
if {![string length $newVarName]} { set newVarName $varName }
uplevel 1 [list upvar \#0 ${class}::$path:$varName $newVarName]
}
proc Widget::options { path args } {
if {[llength $args]} {
foreach option $args {
lappend options [_get_configure $path $option]
}
} else {
set options [_get_configure $path {}]
}
set result [list]
foreach list $options {
if {[llength $list] < 5} { continue }
lappend result [lindex $list 0] [lindex $list end]
}
return $result
}
proc Widget::exists { path } {
variable _class
return [info exists _class($path)]
}
# ----------------------------------------------------------------------------
# utils.tcl -- part of Unifix BWidget Toolkit
# ----------------------------------------------------------------------------
namespace eval BWidget {
variable _top
variable _gstack {}
variable _fstack {}
proc use {} {}
}
proc BWidget::get3dcolor { path bgcolor } {
foreach val [winfo rgb $path $bgcolor] {
lappend dark [expr {60*$val/100}]
set tmp1 [expr {14*$val/10}]
if { $tmp1 > 65535 } {
set tmp1 65535
}
set tmp2 [expr {(65535+$val)/2}]
lappend light [expr {($tmp1 > $tmp2) ? $tmp1:$tmp2}]
}
return [list [eval format "#%04x%04x%04x" $dark] [eval format "#%04x%04x%04x" $light]]
}
# ----------------------------------------------------------------------------
# panedw.tcl -- part of Unifix BWidget Toolkit
# ----------------------------------------------------------------------------
namespace eval PanedWindow {
Widget::define PanedWindow panedw
namespace eval Pane {
Widget::declare PanedWindow::Pane {
{-minsize Int 0 0 "%d >= 0"}
{-weight Int 1 0 "%d >= 0"}
}
}
Widget::declare PanedWindow {
{-side Enum top 1 {top left bottom right}}
{-width Int 10 1 "%d >=3"}
{-pad Int 4 1 "%d >= 0"}
{-background TkResource "" 0 frame}
{-bg Synonym -background}
{-activator Enum "" 1 {line button}}
{-weights Enum extra 1 {extra available}}
}
variable _panedw
}
proc PanedWindow::create { path args } {
variable _panedw
Widget::init PanedWindow $path $args
frame $path -background [Widget::cget $path -background] -class PanedWindow
set _panedw($path,nbpanes) 0
set _panedw($path,weights) ""
set _panedw($path,configuredone) 0
set activator [Widget::getoption $path -activator]
if {[string equal $activator ""]} {
if { $::tcl_platform(platform) != "windows" } {
Widget::setMegawidgetOption $path -activator button
} else {
Widget::setMegawidgetOption $path -activator line
}
}
if {[string equal [Widget::getoption $path -activator] "line"]} {
Widget::setMegawidgetOption $path -width 3
}
bind $path <Configure> [list PanedWindow::_realize $path %w %h]
bind $path <Destroy> [list PanedWindow::_destroy $path]
return [Widget::create PanedWindow $path]
}
proc PanedWindow::configure { path args } {
variable _panedw
set res [Widget::configure $path $args]
if { [Widget::hasChanged $path -background bg] && $_panedw($path,nbpanes) > 0 } {
$path:cmd configure -background $bg
$path.f0 configure -background $bg
for {set i 1} {$i < $_panedw($path,nbpanes)} {incr i} {
set frame $path.sash$i
$frame configure -background $bg
$frame.sep configure -background $bg
$frame.but configure -background $bg
$path.f$i configure -background $bg
$path.f$i.frame configure -background $bg
}
}
return $res
}
proc PanedWindow::cget { path option } {
return [Widget::cget $path $option]
}
proc PanedWindow::add { path args } {
variable _panedw
set num $_panedw($path,nbpanes)
Widget::init PanedWindow::Pane $path.f$num $args
set bg [Widget::getoption $path -background]
set wbut [Widget::getoption $path -width]
set pad [Widget::getoption $path -pad]
set width [expr {$wbut+2*$pad}]
set side [Widget::getoption $path -side]
set weight [Widget::getoption $path.f$num -weight]
lappend _panedw($path,weights) $weight
if { $num > 0 } {
set frame [frame $path.sash$num -relief flat -bd 0 \
-highlightthickness 0 -width $width -height $width -bg $bg]
set sep [frame $frame.sep -bd 5 -relief raised \
-highlightthickness 0 -bg $bg]
set but [frame $frame.but -bd 1 -relief raised \
-highlightthickness 0 -bg $bg -width $wbut -height $wbut]
set sepsize 2
set activator [Widget::getoption $path -activator]
if {$activator == "button"} {
set activator $but
set placeButton 1
} else {
set activator $sep
$sep configure -bd 1
set placeButton 0
}
if {[string equal $side "top"] || [string equal $side "bottom"]} {
place $sep -relx 0.5 -y 0 -width $sepsize -relheight 1.0 -anchor n
if { $placeButton } {
if {[string equal $side "top"]} {
place $but -relx 0.5 -y [expr {6+$wbut/2}] -anchor c
} else {
place $but -relx 0.5 -rely 1.0 -y [expr {-6-$wbut/2}] \
-anchor c
}
}
$activator configure -cursor sb_h_double_arrow
grid $frame -column [expr {2*$num-1}] -row 0 -sticky ns
grid columnconfigure $path [expr {2*$num-1}] -weight 0
} else {
place $sep -x 0 -rely 0.5 -height $sepsize -relwidth 1.0 -anchor w
if { $placeButton } {
if {[string equal $side "left"]} {
place $but -rely 0.5 -x [expr {6+$wbut/2}] -anchor c
} else {
place $but -rely 0.5 -relx 1.0 -x [expr {-6-$wbut/2}] \
-anchor c
}
}
$activator configure -cursor sb_v_double_arrow
grid $frame -row [expr {2*$num-1}] -column 0 -sticky ew
grid rowconfigure $path [expr {2*$num-1}] -weight 0
}
bind $activator <ButtonPress-1> \
[list PanedWindow::_beg_move_sash $path $num %X %Y]
} else {
if { [string equal $side "top"] || \
[string equal $side "bottom"] } {
grid rowconfigure $path 0 -weight 1
} else {
grid columnconfigure $path 0 -weight 1
}
}
set pane [frame $path.f$num -bd 0 -relief flat \
-highlightthickness 0 -bg $bg]
set user [frame $path.f$num.frame -bd 0 -relief flat \
-highlightthickness 0 -bg $bg]
if { [string equal $side "top"] || [string equal $side "bottom"] } {
grid $pane -column [expr {2*$num}] -row 0 -sticky nsew
grid columnconfigure $path [expr {2*$num}] -weight $weight
} else {
grid $pane -row [expr {2*$num}] -column 0 -sticky nsew
grid rowconfigure $path [expr {2*$num}] -weight $weight
}
pack $user -fill both -expand yes
incr _panedw($path,nbpanes)
if {$_panedw($path,configuredone)} {
_realize $path [winfo width $path] [winfo height $path]
}
return $user
}
proc PanedWindow::getframe { path index } {
if { [winfo exists $path.f$index.frame] } {
return $path.f$index.frame
}
}
proc PanedWindow::_beg_move_sash { path num x y } {
variable _panedw
set fprev $path.f[expr {$num-1}]
set fnext $path.f$num
set wsash [expr {[Widget::getoption $path -width] + 2*[Widget::getoption $path -pad]}]
$path.sash$num.but configure -relief sunken
set top [toplevel $path.sash -borderwidth 1 -relief raised]
set minszg [Widget::getoption $fprev -minsize]
set minszd [Widget::getoption $fnext -minsize]
set side [Widget::getoption $path -side]
if { [string equal $side "top"] || [string equal $side "bottom"] } {
$top configure -cursor sb_h_double_arrow
set h [winfo height $path]
set yr [winfo rooty $path.sash$num]
set xmin [expr {$wsash/2+[winfo rootx $fprev]+$minszg}]
set xmax [expr {-$wsash/2-1+[winfo rootx $fnext]+[winfo width $fnext]-$minszd}]
wm overrideredirect $top 1
wm geom $top "2x${h}+$x+$yr"
update idletasks
grab set $top
bind $top <ButtonRelease-1> [list PanedWindow::_end_move_sash $path $top $num $xmin $xmax %X rootx width]
bind $top <Motion> [list PanedWindow::_move_sash $top $xmin $xmax %X +%%d+$yr]
_move_sash $top $xmin $xmax $x "+%d+$yr"
} else {
$top configure -cursor sb_v_double_arrow
set w [winfo width $path]
set xr [winfo rootx $path.sash$num]
set ymin [expr {$wsash/2+[winfo rooty $fprev]+$minszg}]
set ymax [expr {-$wsash/2-1+[winfo rooty $fnext]+[winfo height $fnext]-$minszd}]
wm overrideredirect $top 1
wm geom $top "${w}x2+$xr+$y"
update idletasks
grab set $top
bind $top <ButtonRelease-1> [list PanedWindow::_end_move_sash \
$path $top $num $ymin $ymax %Y rooty height]
bind $top <Motion> [list PanedWindow::_move_sash \
$top $ymin $ymax %Y +$xr+%%d]
_move_sash $top $ymin $ymax $y "+$xr+%d"
}
}
proc PanedWindow::_move_sash { top min max v form } {
if { $v < $min } {
set v $min
} elseif { $v > $max } {
set v $max
}
wm geom $top [format $form $v]
}
proc PanedWindow::_end_move_sash { path top num min max v rootv size } {
variable _panedw
destroy $top
if { $v < $min } {
set v $min
} elseif { $v > $max } {
set v $max
}
set fprev $path.f[expr {$num-1}]
set fnext $path.f$num
$path.sash$num.but configure -relief raised
set wsash [expr {[Widget::getoption $path -width] + 2*[Widget::getoption $path -pad]}]
set dv [expr {$v-[winfo $rootv $path.sash$num]-$wsash/2}]
set w1 [winfo $size $fprev]
set w2 [winfo $size $fnext]
for {set i 0} {$i < $_panedw($path,nbpanes)} {incr i} {
if { $i == $num-1} {
$fprev configure -$size [expr {[winfo $size $fprev]+$dv}]
} elseif { $i == $num } {
$fnext configure -$size [expr {[winfo $size $fnext]-$dv}]
} else {
$path.f$i configure -$size [winfo $size $path.f$i]
}
}
}
proc PanedWindow::_realize { path width height } {
variable _panedw
set x 0
set y 0
set hc [winfo reqheight $path]
set hmax 0
for {set i 0} {$i < $_panedw($path,nbpanes)} {incr i} {
$path.f$i configure \
-width [winfo reqwidth $path.f$i.frame] \
-height [winfo reqheight $path.f$i.frame]
place $path.f$i.frame -x 0 -y 0 -relwidth 1 -relheight 1
}
bind $path <Configure> {}
_apply_weights $path
set _panedw($path,configuredone) 1
return
}
proc PanedWindow::_apply_weights { path } {
variable _panedw
set weights [Widget::getoption $path -weights]
if {[string equal $weights "extra"]} {
return
}
set side [Widget::getoption $path -side]
if {[string equal $side "top"] || [string equal $side "bottom"] } {
set size width
} else {
set size height
}
set wsash [expr {[Widget::getoption $path -width] + 2*[Widget::getoption $path -pad]}]
set rs [winfo $size $path]
set s [expr {$rs - ($_panedw($path,nbpanes) - 1) * $wsash}]
set tw 0.0
foreach w $_panedw($path,weights) {
set tw [expr {$tw + $w}]
}
for {set i 0} {$i < $_panedw($path,nbpanes)} {incr i} {
set rw [lindex $_panedw($path,weights) $i]
set ps [expr {int($rw / $tw * $s)}]
$path.f$i configure -$size $ps
}
return
}
proc PanedWindow::_destroy { path } {
variable _panedw
for {set i 0} {$i < $_panedw($path,nbpanes)} {incr i} {
Widget::destroy $path.f$i
}
unset _panedw($path,nbpanes)
Widget::destroy $path
}
# ------------------------------------------------------------------------------
# arrow.tcl -- part of Unifix BWidget Toolkit
# ------------------------------------------------------------------------------
namespace eval ArrowButton {
Widget::define ArrowButton arrow
Widget::tkinclude ArrowButton button .c \
include [list \
-borderwidth -bd \
-relief -highlightbackground \
-highlightcolor -highlightthickness -takefocus]
Widget::declare ArrowButton [list \
[list -type Enum button 0 [list arrow button]] \
[list -dir Enum top 0 [list top bottom left right]] \
[list -width Int 15 0 "%d >= 0"] \
[list -height Int 15 0 "%d >= 0"] \
[list -ipadx Int 0 0 "%d >= 0"] \
[list -ipady Int 0 0 "%d >= 0"] \
[list -clean Int 2 0 "%d >= 0 && %d <= 2"] \
[list -activeforeground TkResource "" 0 button] \
[list -activebackground TkResource "" 0 button] \
[list -disabledforeground TkResource "" 0 button] \
[list -foreground TkResource "" 0 button] \
[list -background TkResource "" 0 button] \
[list -state TkResource "" 0 button] \
[list -troughcolor TkResource "" 0 scrollbar] \
[list -arrowbd Int 1 0 "%d >= 0 && %d <= 2"] \
[list -arrowrelief Enum raised 0 [list raised sunken]] \
[list -command String "" 0] \
[list -armcommand String "" 0] \
[list -disarmcommand String "" 0] \
[list -repeatdelay Int 0 0 "%d >= 0"] \
[list -repeatinterval Int 0 0 "%d >= 0"] \
[list -fg Synonym -foreground] \
[list -bg Synonym -background] \
]
bind BwArrowButtonC <Enter> {ArrowButton::_enter %W}
bind BwArrowButtonC <Leave> {ArrowButton::_leave %W}
bind BwArrowButtonC <ButtonPress-1> {ArrowButton::_press %W}
bind BwArrowButtonC <ButtonRelease-1> {ArrowButton::_release %W}
bind BwArrowButtonC <Key-space> {ArrowButton::invoke %W; break}
bind BwArrowButtonC <Return> {ArrowButton::invoke %W; break}
bind BwArrowButton <Configure> {ArrowButton::_redraw_whole %W %w %h}
bind BwArrowButton <Destroy> {ArrowButton::_destroy %W}
variable _grab
variable _moved
array set _grab {current "" pressed "" oldstate "normal" oldrelief ""}
}
proc ArrowButton::create { path args } {
# Initialize configuration mappings and parse arguments
array set submaps [list ArrowButton [list ] .c [list ]]
array set submaps [Widget::parseArgs ArrowButton $args]
# Create the class frame (so we can do the option db queries)
frame $path -class ArrowButton -borderwidth 0 -highlightthickness 0
Widget::initFromODB ArrowButton $path $submaps(ArrowButton)
# Create the canvas with the initial options
eval [list canvas $path.c] $submaps(.c)
# Compute the width and height of the canvas from the width/height
# of the ArrowButton and the borderwidth/hightlightthickness.
set w [Widget::getMegawidgetOption $path -width]
set h [Widget::getMegawidgetOption $path -height]
set bd [Widget::cget $path -borderwidth]
set ht [Widget::cget $path -highlightthickness]
set pad [expr {2*($bd+$ht)}]
$path.c configure -width [expr {$w-$pad}] -height [expr {$h-$pad}]
bindtags $path [list $path BwArrowButton [winfo toplevel $path] all]
bindtags $path.c [list $path.c BwArrowButtonC [winfo toplevel $path.c] all]
pack $path.c -expand yes -fill both
set ::ArrowButton::_moved($path) 0
return [Widget::create ArrowButton $path]
}
proc ArrowButton::configure { path args } {
set res [Widget::configure $path $args]
set ch1 [expr {[Widget::hasChanged $path -width w] |
[Widget::hasChanged $path -height h] |
[Widget::hasChanged $path -borderwidth bd] |
[Widget::hasChanged $path -highlightthickness ht]}]
set ch2 [expr {[Widget::hasChanged $path -type val] |
[Widget::hasChanged $path -ipadx val] |
[Widget::hasChanged $path -ipady val] |
[Widget::hasChanged $path -arrowbd val] |
[Widget::hasChanged $path -clean val] |
[Widget::hasChanged $path -dir val]}]
if { $ch1 } {
set pad [expr {2*($bd+$ht)}]
$path.c configure \
-width [expr {$w-$pad}] -height [expr {$h-$pad}] \
-borderwidth $bd -highlightthickness $ht
set ch2 1
}
if { $ch2 } {
_redraw_whole $path [winfo width $path] [winfo height $path]
} else {
_redraw_relief $path
_redraw_state $path
}
return $res
}
proc ArrowButton::cget { path option } {
return [Widget::cget $path $option]
}
proc ArrowButton::invoke { path } {
if { ![string equal [winfo class $path] "ArrowButton"] } {
set path [winfo parent $path]
}
if { ![string equal [Widget::getoption $path -state] "disabled"] } {
set oldstate [Widget::getoption $path -state]
if { [string equal [Widget::getoption $path -type] "button"] } {
set oldrelief [Widget::getoption $path -relief]
configure $path -state active -relief sunken
} else {
set oldrelief [Widget::getoption $path -arrowrelief]
configure $path -state active -arrowrelief sunken
}
update idletasks
if {[llength [set cmd [Widget::getoption $path -armcommand]]]} {
uplevel \#0 $cmd
}
after 10
if { [string equal [Widget::getoption $path -type] "button"] } {
configure $path -state $oldstate -relief $oldrelief
} else {
configure $path -state $oldstate -arrowrelief $oldrelief
}
if {[llength [set cmd [Widget::getoption $path -disarmcommand]]]} {
uplevel \#0 $cmd
}
if {[llength [set cmd [Widget::getoption $path -command]]]} {
uplevel \#0 $cmd
}
}
}
proc ArrowButton::_redraw { path width height } {
variable _moved
set _moved($path) 0
set type [Widget::getoption $path -type]
set dir [Widget::getoption $path -dir]
set bd [expr {[$path.c cget -borderwidth] + [$path.c cget -highlightthickness] + 1}]
set clean [Widget::getoption $path -clean]
if { [string equal $type "arrow"] } {
if { [set id [$path.c find withtag rect]] == "" } {
$path.c create rectangle $bd $bd [expr {$width-$bd-1}] [expr {$height-$bd-1}] -tags rect
} else {
$path.c coords $id $bd $bd [expr {$width-$bd-1}] [expr {$height-$bd-1}]
}
$path.c lower rect
set arrbd [Widget::getoption $path -arrowbd]
set bd [expr {$bd+$arrbd-1}]
} else {
$path.c delete rect
}
# w and h are max width and max height of arrow
set w [expr {$width - 2*([Widget::getoption $path -ipadx]+$bd)}]
set h [expr {$height - 2*([Widget::getoption $path -ipady]+$bd)}]
if { $w < 2 } {set w 2}
if { $h < 2 } {set h 2}
if { $clean > 0 } {
# arrange for base to be odd
if { [string equal $dir "top"] || [string equal $dir "bottom"] } {
if { !($w % 2) } {
incr w -1
}
if { $clean == 2 } {
# arrange for h = (w+1)/2
set h2 [expr {($w+1)/2}]
if { $h2 > $h } {
set w [expr {2*$h-1}]
} else {
set h $h2
}
}
} else {
if { !($h % 2) } {
incr h -1
}
if { $clean == 2 } {
# arrange for w = (h+1)/2
set w2 [expr {($h+1)/2}]
if { $w2 > $w } {
set h [expr {2*$w-1}]
} else {
set w $w2
}
}
}
}
set x0 [expr {($width-$w)/2}]
set y0 [expr {($height-$h)/2}]
set x1 [expr {$x0+$w-1}]
set y1 [expr {$y0+$h-1}]
switch $dir {
top {
set xd [expr {($x0+$x1)/2}]
if { [set id [$path.c find withtag poly]] == "" } {
$path.c create polygon $x0 $y1 $x1 $y1 $xd $y0 -tags poly
} else {
$path.c coords $id $x0 $y1 $x1 $y1 $xd $y0
}
if { [string equal $type "arrow"] } {
if { [set id [$path.c find withtag bot]] == "" } {
$path.c create line $x0 $y1 $x1 $y1 $xd $y0 -tags bot
} else {
$path.c coords $id $x0 $y1 $x1 $y1 $xd $y0
}
if { [set id [$path.c find withtag top]] == "" } {
$path.c create line $x0 $y1 $xd $y0 -tags top
} else {
$path.c coords $id $x0 $y1 $xd $y0
}
$path.c itemconfigure top -width $arrbd
$path.c itemconfigure bot -width $arrbd
} else {
$path.c delete top
$path.c delete bot
}
}
bottom {
set xd [expr {($x0+$x1)/2}]
if { [set id [$path.c find withtag poly]] == "" } {
$path.c create polygon $x1 $y0 $x0 $y0 $xd $y1 -tags poly
} else {
$path.c coords $id $x1 $y0 $x0 $y0 $xd $y1
}
if { [string equal $type "arrow"] } {
if { [set id [$path.c find withtag top]] == "" } {
$path.c create line $x1 $y0 $x0 $y0 $xd $y1 -tags top
} else {
$path.c coords $id $x1 $y0 $x0 $y0 $xd $y1
}
if { [set id [$path.c find withtag bot]] == "" } {
$path.c create line $x1 $y0 $xd $y1 -tags bot
} else {
$path.c coords $id $x1 $y0 $xd $y1
}
$path.c itemconfigure top -width $arrbd
$path.c itemconfigure bot -width $arrbd
} else {
$path.c delete top
$path.c delete bot
}
}
left {
set yd [expr {($y0+$y1)/2}]
if { [set id [$path.c find withtag poly]] == "" } {
$path.c create polygon $x1 $y0 $x1 $y1 $x0 $yd -tags poly
} else {
$path.c coords $id $x1 $y0 $x1 $y1 $x0 $yd
}
if { [string equal $type "arrow"] } {
if { [set id [$path.c find withtag bot]] == "" } {
$path.c create line $x1 $y0 $x1 $y1 $x0 $yd -tags bot
} else {
$path.c coords $id $x1 $y0 $x1 $y1 $x0 $yd
}
if { [set id [$path.c find withtag top]] == "" } {
$path.c create line $x1 $y0 $x0 $yd -tags top
} else {
$path.c coords $id $x1 $y0 $x0 $yd
}
$path.c itemconfigure top -width $arrbd
$path.c itemconfigure bot -width $arrbd
} else {
$path.c delete top
$path.c delete bot
}
}
right {
set yd [expr {($y0+$y1)/2}]
if { [set id [$path.c find withtag poly]] == "" } {
$path.c create polygon $x0 $y1 $x0 $y0 $x1 $yd -tags poly
} else {
$path.c coords $id $x0 $y1 $x0 $y0 $x1 $yd
}
if { [string equal $type "arrow"] } {
if { [set id [$path.c find withtag top]] == "" } {
$path.c create line $x0 $y1 $x0 $y0 $x1 $yd -tags top
} else {
$path.c coords $id $x0 $y1 $x0 $y0 $x1 $yd
}
if { [set id [$path.c find withtag bot]] == "" } {
$path.c create line $x0 $y1 $x1 $yd -tags bot
} else {
$path.c coords $id $x0 $y1 $x1 $yd
}
$path.c itemconfigure top -width $arrbd
$path.c itemconfigure bot -width $arrbd
} else {
$path.c delete top
$path.c delete bot
}
}
}
}
proc ArrowButton::_redraw_state { path } {
set state [Widget::getoption $path -state]
if { [string equal [Widget::getoption $path -type] "button"] } {
switch $state {
normal {set bg -background; set fg -foreground}
active {set bg -activebackground; set fg -activeforeground}
disabled {set bg -background; set fg -disabledforeground}
}
set fg [Widget::getoption $path $fg]
$path.c configure -background [Widget::getoption $path $bg]
$path.c itemconfigure poly -fill $fg -outline $fg
} else {
switch $state {
normal {set stipple ""; set bg [Widget::getoption $path -background] }
active {set stipple ""; set bg [Widget::getoption $path -activebackground] }
disabled {set stipple gray50; set bg black }
}
set thrc [Widget::getoption $path -troughcolor]
$path.c configure -background [Widget::getoption $path -background]
$path.c itemconfigure rect -fill $thrc -outline $thrc
$path.c itemconfigure poly -fill $bg -outline $bg -stipple $stipple
}
}
proc ArrowButton::_redraw_relief { path } {
variable _moved
if { [string equal [Widget::getoption $path -type] "button"] } {
if { [string equal [Widget::getoption $path -relief] "sunken"] } {
if { !$_moved($path) } {
$path.c move poly 1 1
set _moved($path) 1
}
} else {
if { $_moved($path) } {
$path.c move poly -1 -1
set _moved($path) 0
}
}
} else {
set col3d [BWidget::get3dcolor $path [Widget::getoption $path -background]]
switch [Widget::getoption $path -arrowrelief] {
raised {set top [lindex $col3d 1]; set bot [lindex $col3d 0]}
sunken {set top [lindex $col3d 0]; set bot [lindex $col3d 1]}
}
$path.c itemconfigure top -fill $top
$path.c itemconfigure bot -fill $bot
}
}
proc ArrowButton::_redraw_whole { path width height } {
_redraw $path $width $height
_redraw_relief $path
_redraw_state $path
}
proc ArrowButton::_enter { path } {
variable _grab
set path [winfo parent $path]
set _grab(current) $path
if { ![string equal [Widget::getoption $path -state] "disabled"] } {
set _grab(oldstate) [Widget::getoption $path -state]
configure $path -state active
if { $_grab(pressed) == $path } {
if { [string equal [Widget::getoption $path -type] "button"] } {
set _grab(oldrelief) [Widget::getoption $path -relief]
configure $path -relief sunken
} else {
set _grab(oldrelief) [Widget::getoption $path -arrowrelief]
configure $path -arrowrelief sunken
}
}
}
}
proc ArrowButton::_leave { path } {
variable _grab
set path [winfo parent $path]
set _grab(current) ""
if { ![string equal [Widget::getoption $path -state] "disabled"] } {
configure $path -state $_grab(oldstate)
if { $_grab(pressed) == $path } {
if { [string equal [Widget::getoption $path -type] "button"] } {
configure $path -relief $_grab(oldrelief)
} else {
configure $path -arrowrelief $_grab(oldrelief)
}
}
}
}
proc ArrowButton::_press { path } {
variable _grab
set path [winfo parent $path]
if { ![string equal [Widget::getoption $path -state] "disabled"] } {
set _grab(pressed) $path
if { [string equal [Widget::getoption $path -type] "button"] } {
set _grab(oldrelief) [Widget::getoption $path -relief]
configure $path -relief sunken
} else {
set _grab(oldrelief) [Widget::getoption $path -arrowrelief]
configure $path -arrowrelief sunken
}
if {[llength [set cmd [Widget::getoption $path -armcommand]]]} {
uplevel \#0 $cmd
if { [set delay [Widget::getoption $path -repeatdelay]] > 0 ||
[set delay [Widget::getoption $path -repeatinterval]] > 0 } {
after $delay [list ArrowButton::_repeat $path]
}
}
}
}
proc ArrowButton::_release { path } {
variable _grab
set path [winfo parent $path]
if { $_grab(pressed) == $path } {
set _grab(pressed) ""
if { [string equal [Widget::getoption $path -type] "button"] } {
configure $path -relief $_grab(oldrelief)
} else {
configure $path -arrowrelief $_grab(oldrelief)
}
if {[llength [set cmd [Widget::getoption $path -disarmcommand]]]} {
uplevel \#0 $cmd
}
if { $_grab(current) == $path &&
![string equal [Widget::getoption $path -state] "disabled"] &&
[llength [set cmd [Widget::getoption $path -command]]]} {
uplevel \#0 $cmd
}
}
}
proc ArrowButton::_repeat { path } {
variable _grab
if { $_grab(current) == $path && $_grab(pressed) == $path &&
![string equal [Widget::getoption $path -state] "disabled"] &&
[llength [set cmd [Widget::getoption $path -armcommand]]]} {
uplevel \#0 $cmd
}
if { $_grab(pressed) == $path &&
([set delay [Widget::getoption $path -repeatinterval]] > 0 ||
[set delay [Widget::getoption $path -repeatdelay]] > 0) } {
after $delay [list ArrowButton::_repeat $path]
}
}
proc ArrowButton::_destroy { path } {
variable _moved
Widget::destroy $path
unset _moved($path)
}
# ---------------------------------------------------------------------------
# notebook.tcl -- part of Unifix BWidget Toolkit
# ---------------------------------------------------------------------------
namespace eval NoteBook {
Widget::define NoteBook notebook ArrowButton
namespace eval Page {
Widget::declare NoteBook::Page {
{-state Enum normal 0 {normal disabled}}
{-createcmd String "" 0}
{-raisecmd String "" 0}
{-leavecmd String "" 0}
{-image TkResource "" 0 label}
{-text String "" 0}
{-foreground String "" 0}
{-background String "" 0}
{-activeforeground String "" 0}
{-activebackground String "" 0}
{-disabledforeground String "" 0}
}
}
Widget::bwinclude NoteBook ArrowButton .c.fg \
include {-foreground -background -activeforeground \
-activebackground -disabledforeground -repeatinterval \
-repeatdelay -borderwidth} \
initialize {-borderwidth 1}
Widget::bwinclude NoteBook ArrowButton .c.fd \
include {-foreground -background -activeforeground \
-activebackground -disabledforeground -repeatinterval \
-repeatdelay -borderwidth} \
initialize {-borderwidth 1}
Widget::declare NoteBook {
{-foreground TkResource "" 0 button}
{-background TkResource "" 0 button}
{-activebackground TkResource "" 0 button}
{-activeforeground TkResource "" 0 button}
{-disabledforeground TkResource "" 0 button}
{-font TkResource "" 0 button}
{-side Enum top 0 {top bottom}}
{-homogeneous Boolean 0 0}
{-borderwidth Int 1 0 "%d >= 1 && %d <= 2"}
{-internalborderwidth Int 10 0 "%d >= 0"}
{-width Int 0 0 "%d >= 0"}
{-height Int 0 0 "%d >= 0"}
{-repeatdelay BwResource "" 0 ArrowButton}
{-repeatinterval BwResource "" 0 ArrowButton}
{-fg Synonym -foreground}
{-bg Synonym -background}
{-bd Synonym -borderwidth}
{-ibd Synonym -internalborderwidth}
{-arcradius Int 2 0 "%d >= 0 && %d <= 8"}
{-tabbevelsize Int 0 0 "%d >= 0 && %d <= 8"}
{-tabpady Padding {0 6} 0 "%d >= 0"}
}
Widget::addmap NoteBook "" .c {-background {}}
variable _warrow 12
bind NoteBook <Configure> [list NoteBook::_resize %W]
bind NoteBook <Destroy> [list NoteBook::_destroy %W]
}
proc NoteBook::create { path args } {
variable $path
upvar 0 $path data
Widget::init NoteBook $path $args
set data(base) 0
set data(select) ""
set data(pages) {}
set data(pages) {}
set data(cpt) 0
set data(realized) 0
set data(wpage) 0
_compute_height $path
# Create the canvas
set w [expr {[Widget::cget $path -width]+4}]
set h [expr {[Widget::cget $path -height]+$data(hpage)+4}]
frame $path -class NoteBook -borderwidth 0 -highlightthickness 0 \
-relief flat
eval [list canvas $path.c] [Widget::subcget $path .c] \
[list -relief flat -borderwidth 0 -highlightthickness 0 \
-width $w -height $h]
pack $path.c -expand yes -fill both
# Removing the Canvas global bindings from our canvas as
# application specific bindings on that tag may interfere with its
# operation here. [SF item #459033]
set bindings [bindtags $path.c]
set pos [lsearch -exact $bindings Canvas]
if {$pos >= 0} {
set bindings [lreplace $bindings $pos $pos]
}
bindtags $path.c $bindings
# Create the arrow button
eval [list ArrowButton::create $path.c.fg] [Widget::subcget $path .c.fg] \
[list -highlightthickness 0 -type button -dir left \
-armcommand [list NoteBook::_xview $path -1]]
eval [list ArrowButton::create $path.c.fd] [Widget::subcget $path .c.fd] \
[list -highlightthickness 0 -type button -dir right \
-armcommand [list NoteBook::_xview $path 1]]
Widget::create NoteBook $path
set bg [Widget::cget $path -background]
foreach {data(dbg) data(lbg)} [BWidget::get3dcolor $path $bg] {break}
return $path
}
proc NoteBook::configure { path args } {
variable $path
upvar 0 $path data
set res [Widget::configure $path $args]
set redraw 0
set opts [list -font -homogeneous -tabpady]
foreach {cf ch cp} [eval Widget::hasChangedX $path $opts] {break}
if {$cf || $ch || $cp} {
if { $cf || $cp } {
_compute_height $path
}
_compute_width $path
set redraw 1
}
set chibd [Widget::hasChanged $path -internalborderwidth ibd]
set chbg [Widget::hasChanged $path -background bg]
if {$chibd || $chbg} {
foreach page $data(pages) {
$path.f$page configure \
-borderwidth $ibd -background $bg
}
}
if {$chbg} {
set col [BWidget::get3dcolor $path $bg]
set data(dbg) [lindex $col 0]
set data(lbg) [lindex $col 1]
set redraw 1
}
if { [Widget::hasChanged $path -foreground fg] ||
[Widget::hasChanged $path -borderwidth bd] ||
[Widget::hasChanged $path -arcradius radius] ||
[Widget::hasChanged $path -tabbevelsize bevel] ||
[Widget::hasChanged $path -side side] } {
set redraw 1
}
set wc [Widget::hasChanged $path -width w]
set hc [Widget::hasChanged $path -height h]
if { $wc || $hc } {
$path.c configure \
-width [expr {$w + 4}] \
-height [expr {$h + $data(hpage) + 4}]
}
if { $redraw } {
_redraw $path
}
return $res
}
proc NoteBook::cget { path option } {
return [Widget::cget $path $option]
}
proc NoteBook::compute_size { path } {
variable $path
upvar 0 $path data
set wmax 0
set hmax 0
update idletasks
foreach page $data(pages) {
set w [winfo reqwidth $path.f$page]
set h [winfo reqheight $path.f$page]
set wmax [expr {$w>$wmax ? $w : $wmax}]
set hmax [expr {$h>$hmax ? $h : $hmax}]
}
configure $path -width $wmax -height $hmax
# Sven... well ok so this is called twice in some cases...
NoteBook::_redraw $path
# Sven end
}
proc NoteBook::insert { path index page args } {
variable $path
upvar 0 $path data
if { [lsearch -exact $data(pages) $page] != -1 } {
return -code error "page \"$page\" already exists"
}
set f $path.f$page
Widget::init NoteBook::Page $f $args
set data(pages) [linsert $data(pages) $index $page]
# If the page doesn't exist, create it; if it does reset its bg and ibd
if { ![winfo exists $f] } {
frame $f \
-relief flat \
-background [Widget::cget $path -background] \
-borderwidth [Widget::cget $path -internalborderwidth]
set data($page,realized) 0
} else {
$f configure \
-background [Widget::cget $path -background] \
-borderwidth [Widget::cget $path -internalborderwidth]
}
_compute_height $path
_compute_width $path
_draw_page $path $page 1
_redraw $path
return $f
}
proc NoteBook::delete { path page {destroyframe 1} } {
variable $path
upvar 0 $path data
set pos [_test_page $path $page]
set data(pages) [lreplace $data(pages) $pos $pos]
_compute_width $path
$path.c delete p:$page
if { $data(select) == $page } {
set data(select) ""
}
if { $pos < $data(base) } {
incr data(base) -1
}
if { $destroyframe } {
destroy $path.f$page
unset data($page,width) data($page,realized)
}
_redraw $path
}
proc NoteBook::itemconfigure { path page args } {
_test_page $path $page
set res [_itemconfigure $path $page $args]
_redraw $path
return $res
}
proc NoteBook::itemcget { path page option } {
_test_page $path $page
return [Widget::cget $path.f$page $option]
}
proc NoteBook::bindtabs { path event script } {
if { $script != "" } {
append script " \[NoteBook::_get_page_name [list $path] current 1\]"
$path.c bind "page" $event $script
} else {
$path.c bind "page" $event {}
}
}
proc NoteBook::move { path page index } {
variable $path
upvar 0 $path data
set pos [_test_page $path $page]
set data(pages) [linsert [lreplace $data(pages) $pos $pos] $index $page]
_redraw $path
}
proc NoteBook::raise { path {page ""} } {
variable $path
upvar 0 $path data
if { $page != "" } {
_test_page $path $page
_select $path $page
}
return $data(select)
}
proc NoteBook::see { path page } {
variable $path
upvar 0 $path data
set pos [_test_page $path $page]
if { $pos < $data(base) } {
set data(base) $pos
_redraw $path
} else {
set w [expr {[winfo width $path]-1}]
set fpage [expr {[_get_x_page $path $pos] + $data($page,width) + 6}]
set idx $data(base)
while { $idx < $pos && $fpage > $w } {
set fpage [expr {$fpage - $data([lindex $data(pages) $idx],width)}]
incr idx
}
if { $idx != $data(base) } {
set data(base) $idx
_redraw $path
}
}
}
proc NoteBook::page { path first {last ""} } {
variable $path
upvar 0 $path data
if { $last == "" } {
return [lindex $data(pages) $first]
} else {
return [lrange $data(pages) $first $last]
}
}
proc NoteBook::pages { path {first ""} {last ""}} {
variable $path
upvar 0 $path data
if { ![string length $first] } {
return $data(pages)
}
if { ![string length $last] } {
return [lindex $data(pages) $first]
} else {
return [lrange $data(pages) $first $last]
}
}
proc NoteBook::index { path page } {
variable $path
upvar 0 $path data
return [lsearch -exact $data(pages) $page]
}
proc NoteBook::_destroy { path } {
variable $path
upvar 0 $path data
foreach page $data(pages) {
Widget::destroy $path.f$page
}
Widget::destroy $path
unset data
}
proc NoteBook::getframe { path page } {
return $path.f$page
}
proc NoteBook::_test_page { path page } {
variable $path
upvar 0 $path data
if { [set pos [lsearch -exact $data(pages) $page]] == -1 } {
return -code error "page \"$page\" does not exists"
}
return $pos
}
proc NoteBook::_getoption { path page option } {
set value [Widget::cget $path.f$page $option]
if {![string length $value]} {
set value [Widget::cget $path $option]
}
return $value
}
proc NoteBook::_itemconfigure { path page lres } {
variable $path
upvar 0 $path data
set res [Widget::configure $path.f$page $lres]
if { [Widget::hasChanged $path.f$page -text foo] } {
_compute_width $path
} elseif { [Widget::hasChanged $path.f$page -image foo] } {
_compute_height $path
_compute_width $path
}
if { [Widget::hasChanged $path.f$page -state state] &&
$state == "disabled" && $data(select) == $page } {
set data(select) ""
}
return $res
}
proc NoteBook::_compute_width { path } {
variable $path
upvar 0 $path data
set wmax 0
set wtot 0
set hmax $data(hpage)
set font [Widget::cget $path -font]
if { ![info exists data(textid)] } {
set data(textid) [$path.c create text 0 -100 -font $font -anchor nw]
}
set id $data(textid)
$path.c itemconfigure $id -font $font
foreach page $data(pages) {
$path.c itemconfigure $id -text [Widget::cget $path.f$page -text]
# Get the bbox for this text to determine its width, then substract
# 6 from the width to account for canvas bbox oddness w.r.t. widths of
# simple text.
foreach {x1 y1 x2 y2} [$path.c bbox $id] break
set x2 [expr {$x2 - 6}]
set wtext [expr {$x2 - $x1 + 20}]
if { [set img [Widget::cget $path.f$page -image]] != "" } {
set wtext [expr {$wtext + [image width $img] + 4}]
set himg [expr {[image height $img] + 6}]
if { $himg > $hmax } {
set hmax $himg
}
}
set wmax [expr {$wtext > $wmax ? $wtext : $wmax}]
incr wtot $wtext
set data($page,width) $wtext
}
if { [Widget::cget $path -homogeneous] } {
foreach page $data(pages) {
set data($page,width) $wmax
}
set wtot [expr {$wmax * [llength $data(pages)]}]
}
set data(hpage) $hmax
set data(wpage) $wtot
}
proc NoteBook::_compute_height { path } {
variable $path
upvar 0 $path data
set font [Widget::cget $path -font]
set pady0 [Widget::_get_padding $path -tabpady 0]
set pady1 [Widget::_get_padding $path -tabpady 1]
set metrics [font metrics $font -linespace]
set imgh 0
set lines 1
foreach page $data(pages) {
set img [Widget::cget $path.f$page -image]
set text [Widget::cget $path.f$page -text]
set len [llength [split $text \n]]
if {$len > $lines} { set lines $len}
if {$img != ""} {
set h [image height $img]
if {$h > $imgh} { set imgh $h }
}
}
set height [expr {$metrics * $lines}]
if {$imgh > $height} { set height $imgh }
set data(hpage) [expr {$height + $pady0 + $pady1}]
}
proc NoteBook::_get_x_page { path pos } {
variable _warrow
variable $path
upvar 0 $path data
set base $data(base)
# notebook tabs start flush with the left side of the notebook
set x 0
if { $pos < $base } {
foreach page [lrange $data(pages) $pos [expr {$base-1}]] {
incr x [expr {-$data($page,width)}]
}
} elseif { $pos > $base } {
foreach page [lrange $data(pages) $base [expr {$pos-1}]] {
incr x $data($page,width)
}
}
return $x
}
proc NoteBook::_xview { path inc } {
variable $path
upvar 0 $path data
if { $inc == -1 } {
set base [expr {$data(base)-1}]
set dx $data([lindex $data(pages) $base],width)
} else {
set dx [expr {-$data([lindex $data(pages) $data(base)],width)}]
set base [expr {$data(base)+1}]
}
if { $base >= 0 && $base < [llength $data(pages)] } {
set data(base) $base
$path.c move page $dx 0
_draw_area $path
_draw_arrows $path
}
}
proc NoteBook::_highlight { type path page } {
variable $path
upvar 0 $path data
if { [string equal [Widget::cget $path.f$page -state] "disabled"] } {
return
}
switch -- $type {
on {
$path.c itemconfigure "$page:poly" \
-fill [_getoption $path $page -activebackground]
$path.c itemconfigure "$page:text" \
-fill [_getoption $path $page -activeforeground]
}
off {
$path.c itemconfigure "$page:poly" \
-fill [_getoption $path $page -background]
$path.c itemconfigure "$page:text" \
-fill [_getoption $path $page -foreground]
}
}
}
proc NoteBook::_select { path page } {
variable $path
upvar 0 $path data
if {![string equal [Widget::cget $path.f$page -state] "normal"]} { return }
set oldsel $data(select)
if {[string equal $page $oldsel]} { return }
if { ![string equal $oldsel ""] } {
set cmd [Widget::cget $path.f$oldsel -leavecmd]
if { ![string equal $cmd ""] } {
set code [catch {uplevel \#0 $cmd} res]
if { $code == 1 || $res == 0 } {
return -code $code $res
}
}
set data(select) ""
_draw_page $path $oldsel 0
}
set data(select) $page
if { ![string equal $page ""] } {
if { !$data($page,realized) } {
set data($page,realized) 1
set cmd [Widget::cget $path.f$page -createcmd]
if { ![string equal $cmd ""] } {
uplevel \#0 $cmd
}
}
set cmd [Widget::cget $path.f$page -raisecmd]
if { ![string equal $cmd ""] } {
uplevel \#0 $cmd
}
_draw_page $path $page 0
}
_draw_area $path
}
proc NoteBook::_redraw { path } {
variable $path
upvar 0 $path data
if { !$data(realized) } { return }
_compute_height $path
foreach page $data(pages) {
_draw_page $path $page 0
}
_draw_area $path
_draw_arrows $path
}
proc NoteBook::_draw_page { path page create } {
variable $path
upvar 0 $path data
# --- calcul des coordonnees et des couleurs de l'onglet ------------------
set pos [lsearch -exact $data(pages) $page]
set bg [_getoption $path $page -background]
# lookup the tab colors
set fgt $data(lbg)
set fgb $data(dbg)
set h $data(hpage)
set xd [_get_x_page $path $pos]
set xf [expr {$xd + $data($page,width)}]
# Set the initial text offsets -- a few pixels down, centered left-to-right
set textOffsetY [expr [Widget::_get_padding $path -tabpady 0] + 3]
set textOffsetX 9
set top 2
set arcRadius [Widget::cget $path -arcradius]
set xBevel [Widget::cget $path -tabbevelsize]
if { $data(select) != $page } {
if { $pos == 0 } {
# The leftmost page is a special case -- it is drawn with its
# tab a little indented. To achieve this, we incr xd. We also
# decr textOffsetX, so that the text doesn't move left/right.
incr xd 2
incr textOffsetX -2
}
} else {
# The selected page's text is raised higher than the others
incr top -2
}
# Precompute some coord values that we use a lot
set topPlusRadius [expr {$top + $arcRadius}]
set rightPlusRadius [expr {$xf + $arcRadius}]
set leftPlusRadius [expr {$xd + $arcRadius}]
# Sven
set side [Widget::cget $path -side]
set tabsOnBottom [string equal $side "bottom"]
set h1 [expr {[winfo height $path]}]
set bd [Widget::cget $path -borderwidth]
if {$bd < 1} { set bd 1 }
if { $tabsOnBottom } {
# adjust to keep bottom edge in view
incr h1 -1
set top [expr {$top * -1}]
set topPlusRadius [expr {$topPlusRadius * -1}]
# Hrm... the canvas has an issue with drawing diagonal segments
# of lines from the bottom to the top, so we have to draw this line
# backwards (ie, lt is actually the bottom, drawn from right to left)
set lt [list \
$rightPlusRadius [expr {$h1-$h-1}] \
[expr {$rightPlusRadius - $xBevel}] [expr {$h1 + $topPlusRadius}] \
[expr {$xf - $xBevel}] [expr {$h1 + $top}] \
[expr {$leftPlusRadius + $xBevel}] [expr {$h1 + $top}] \
]
set lb [list \
[expr {$leftPlusRadius + $xBevel}] [expr {$h1 + $top}] \
[expr {$xd + $xBevel}] [expr {$h1 + $topPlusRadius}] \
$xd [expr {$h1-$h-1}] \
]
# Because we have to do this funky reverse order thing, we have to
# swap the top/bottom colors too.
set tmp $fgt
set fgt $fgb
set fgb $tmp
} else {
set lt [list \
$xd $h \
[expr {$xd + $xBevel}] $topPlusRadius \
[expr {$leftPlusRadius + $xBevel}] $top \
[expr {$xf + 1 - $xBevel}] $top \
]
set lb [list \
[expr {$xf + 1 - $xBevel}] [expr {$top + 1}] \
[expr {$rightPlusRadius - $xBevel}] $topPlusRadius \
$rightPlusRadius $h \
]
}
set img [Widget::cget $path.f$page -image]
set ytext $top
if { $tabsOnBottom } {
# The "+ 2" below moves the text closer to the bottom of the tab,
# so it doesn't look so cramped. I should be able to achieve the
# same goal by changing the anchor of the text and using this formula:
# ytext = $top + $h1 - $textOffsetY
# but that doesn't quite work (I think the linespace from the text
# gets in the way)
incr ytext [expr {$h1 - $h + 2}]
}
incr ytext $textOffsetY
set xtext [expr {$xd + $textOffsetX}]
if { $img != "" } {
# if there's an image, put it on the left and move the text right
set ximg $xtext
incr xtext [expr {[image width $img] + 2}]
}
if { $data(select) == $page } {
set bd [Widget::cget $path -borderwidth]
if {$bd < 1} { set bd 1 }
set fg [_getoption $path $page -foreground]
} else {
set bd 1
if { [Widget::cget $path.f$page -state] == "normal" } {
set fg [_getoption $path $page -foreground]
} else {
set fg [_getoption $path $page -disabledforeground]
}
}
# --- creation ou modification de l'onglet --------------------------------
# Sven
if { $create } {
# Create the tab region
eval [list $path.c create polygon] [concat $lt $lb] [list \
-tags [list page p:$page $page:poly] \
-outline $bg \
-fill $bg \
]
eval [list $path.c create line] $lt [list \
-tags [list page p:$page $page:top top] -fill $fgt -width $bd]
eval [list $path.c create line] $lb [list \
-tags [list page p:$page $page:bot bot] -fill $fgb -width $bd]
$path.c create text $xtext $ytext \
-text [Widget::cget $path.f$page -text] \
-font [Widget::cget $path -font] \
-fill $fg \
-anchor nw \
-tags [list page p:$page $page:text]
$path.c bind p:$page <ButtonPress-1> \
[list NoteBook::_select $path $page]
$path.c bind p:$page <Enter> \
[list NoteBook::_highlight on $path $page]
$path.c bind p:$page <Leave> \
[list NoteBook::_highlight off $path $page]
} else {
$path.c coords "$page:text" $xtext $ytext
$path.c itemconfigure "$page:text" \
-text [Widget::cget $path.f$page -text] \
-font [Widget::cget $path -font] \
-fill $fg
}
eval [list $path.c coords "$page:poly"] [concat $lt $lb]
eval [list $path.c coords "$page:top"] $lt
eval [list $path.c coords "$page:bot"] $lb
$path.c itemconfigure "$page:poly" -fill $bg -outline $bg
$path.c itemconfigure "$page:top" -fill $fgt -width $bd
$path.c itemconfigure "$page:bot" -fill $fgb -width $bd
# Sven end
if { $img != "" } {
# Sven
set id [$path.c find withtag $page:img]
if { [string equal $id ""] } {
set id [$path.c create image $ximg $ytext \
-anchor nw \
-tags [list page p:$page $page:img]]
}
$path.c coords $id $ximg $ytext
$path.c itemconfigure $id -image $img
# Sven end
} else {
$path.c delete $page:img
}
if { $data(select) == $page } {
$path.c raise p:$page
} elseif { $pos == 0 } {
if { $data(select) == "" } {
$path.c raise p:$page
} else {
$path.c lower p:$page p:$data(select)
}
} else {
set pred [lindex $data(pages) [expr {$pos-1}]]
if { $data(select) != $pred || $pos == 1 } {
$path.c lower p:$page p:$pred
} else {
$path.c lower p:$page p:[lindex $data(pages) [expr {$pos-2}]]
}
}
}
proc NoteBook::_draw_arrows { path } {
variable _warrow
variable $path
upvar 0 $path data
set w [expr {[winfo width $path]-1}]
set h [expr {$data(hpage)-1}]
set nbpages [llength $data(pages)]
set xl 0
set xr [expr {$w-$_warrow+1}]
set side [Widget::cget $path -side]
if { [string equal $side "bottom"] } {
set h1 [expr {[winfo height $path]-1}]
set bd [Widget::cget $path -borderwidth]
if {$bd < 1} { set bd 1 }
set y0 [expr {$h1 - $data(hpage) + $bd}]
} else {
set y0 1
}
if { $data(base) > 0 } {
# Sven
if { ![llength [$path.c find withtag "leftarrow"]] } {
$path.c create window $xl $y0 \
-width $_warrow \
-height $h \
-anchor nw \
-window $path.c.fg \
-tags "leftarrow"
} else {
$path.c coords "leftarrow" $xl $y0
$path.c itemconfigure "leftarrow" -width $_warrow -height $h
}
# Sven end
} else {
$path.c delete "leftarrow"
}
if { $data(base) < $nbpages-1 &&
$data(wpage) + [_get_x_page $path 0] + 6 > $w } {
# Sven
if { ![llength [$path.c find withtag "rightarrow"]] } {
$path.c create window $xr $y0 \
-width $_warrow \
-height $h \
-window $path.c.fd \
-anchor nw \
-tags "rightarrow"
} else {
$path.c coords "rightarrow" $xr $y0
$path.c itemconfigure "rightarrow" -width $_warrow -height $h
}
# Sven end
} else {
$path.c delete "rightarrow"
}
}
proc NoteBook::_draw_area { path } {
variable $path
upvar 0 $path data
set w [expr {[winfo width $path] - 1}]
set h [expr {[winfo height $path] - 1}]
set bd [Widget::cget $path -borderwidth]
if {$bd < 1} { set bd 1 }
set x0 [expr {$bd - 1}]
set arcRadius [Widget::cget $path -arcradius]
# Sven
set side [Widget::cget $path -side]
if {"$side" == "bottom"} {
set y0 0
set y1 [expr {$h - $data(hpage)}]
set yo $y1
} else {
set y0 $data(hpage)
set y1 $h
set yo [expr {$h-$y0}]
}
# Sven end
set dbg $data(dbg)
set sel $data(select)
if { $sel == "" } {
set xd [expr {$w/2}]
set xf $xd
set lbg $data(dbg)
} else {
set xd [_get_x_page $path [lsearch -exact $data(pages) $data(select)]]
set xf [expr {$xd + $data($sel,width) + $arcRadius + 1}]
set lbg $data(lbg)
}
# Sven
if { [llength [$path.c find withtag rect]] == 0} {
$path.c create line $xd $y0 $x0 $y0 $x0 $y1 \
-tags "rect toprect1"
$path.c create line $w $y0 $xf $y0 \
-tags "rect toprect2"
$path.c create line 1 $h $w $h $w $y0 \
-tags "rect botrect"
}
if {"$side" == "bottom"} {
$path.c coords "toprect1" $w $y0 $x0 $y0 $x0 $y1
$path.c coords "toprect2" $x0 $y1 $xd $y1
$path.c coords "botrect" $xf $y1 $w $y1 $w $y0
$path.c itemconfigure "toprect1" -fill $lbg -width $bd
$path.c itemconfigure "toprect2" -fill $dbg -width $bd
$path.c itemconfigure "botrect" -fill $dbg -width $bd
} else {
$path.c coords "toprect1" $xd $y0 $x0 $y0 $x0 $y1
$path.c coords "toprect2" $w $y0 $xf $y0
$path.c coords "botrect" $x0 $h $w $h $w $y0
$path.c itemconfigure "toprect1" -fill $lbg -width $bd
$path.c itemconfigure "toprect2" -fill $lbg -width $bd
$path.c itemconfigure "botrect" -fill $dbg -width $bd
}
$path.c raise "rect"
# Sven end
if { $sel != "" } {
# Sven
if { [llength [$path.c find withtag "window"]] == 0 } {
$path.c create window 2 [expr {$y0+1}] \
-width [expr {$w-3}] \
-height [expr {$yo-3}] \
-anchor nw \
-tags "window" \
-window $path.f$sel
}
$path.c coords "window" 2 [expr {$y0+1}]
$path.c itemconfigure "window" \
-width [expr {$w-3}] \
-height [expr {$yo-3}] \
-window $path.f$sel
# Sven end
} else {
$path.c delete "window"
}
}
proc NoteBook::_resize { path } {
variable $path
upvar 0 $path data
if {!$data(realized)} {
if { [set width [Widget::cget $path -width]] == 0 ||
[set height [Widget::cget $path -height]] == 0 } {
compute_size $path
}
set data(realized) 1
}
NoteBook::_redraw $path
}
proc NoteBook::_get_page_name { path {item current} {tagindex end-1} } {
return [string range [lindex [$path.c gettags $item] $tagindex] 2 end]
}
# -----------------------------------------------------------------------------
# scrollw.tcl -- part of Unifix BWidget Toolkit
# -----------------------------------------------------------------------------
namespace eval ScrolledWindow {
Widget::define ScrolledWindow scrollw
Widget::declare ScrolledWindow {
{-background TkResource "" 0 button}
{-scrollbar Enum both 0 {none both vertical horizontal}}
{-auto Enum both 0 {none both vertical horizontal}}
{-sides Enum se 0 {ne en nw wn se es sw ws}}
{-size Int 0 1 "%d >= 0"}
{-ipad Int 1 1 "%d >= 0"}
{-managed Boolean 1 1}
{-relief TkResource flat 0 frame}
{-borderwidth TkResource 0 0 frame}
{-bg Synonym -background}
{-bd Synonym -borderwidth}
}
Widget::addmap ScrolledWindow "" :cmd {-relief {} -borderwidth {}}
}
proc ScrolledWindow::create { path args } {
Widget::init ScrolledWindow $path $args
Widget::getVariable $path data
set bg [Widget::cget $path -background]
set sbsize [Widget::cget $path -size]
set sw [eval [list frame $path \
-relief flat -borderwidth 0 -background $bg \
-highlightthickness 0 -takefocus 0] \
[Widget::subcget $path :cmd]]
scrollbar $path.hscroll \
-highlightthickness 0 -takefocus 0 \
-orient horiz \
-relief sunken \
-bg $bg
scrollbar $path.vscroll \
-highlightthickness 0 -takefocus 0 \
-orient vert \
-relief sunken \
-bg $bg
set data(realized) 0
_setData $path \
[Widget::cget $path -scrollbar] \
[Widget::cget $path -auto] \
[Widget::cget $path -sides]
if {[Widget::cget $path -managed]} {
set data(hsb,packed) $data(hsb,present)
set data(vsb,packed) $data(vsb,present)
} else {
set data(hsb,packed) 0
set data(vsb,packed) 0
}
if {$sbsize} {
$path.vscroll configure -width $sbsize
$path.hscroll configure -width $sbsize
} else {
set sbsize [$path.vscroll cget -width]
}
set data(ipad) [Widget::cget $path -ipad]
if {$data(hsb,packed)} {
grid $path.hscroll -column 1 -row $data(hsb,row) \
-sticky ew -ipady $data(ipad)
}
if {$data(vsb,packed)} {
grid $path.vscroll -column $data(vsb,column) -row 1 \
-sticky ns -ipadx $data(ipad)
}
grid columnconfigure $path 1 -weight 1
grid rowconfigure $path 1 -weight 1
bind $path <Configure> [list ScrolledWindow::_realize $path]
bind $path <Destroy> [list ScrolledWindow::_destroy $path]
return [Widget::create ScrolledWindow $path]
}
proc ScrolledWindow::getframe { path } {
return $path
}
proc ScrolledWindow::setwidget { path widget } {
Widget::getVariable $path data
if {[info exists data(widget)] && [winfo exists $data(widget)]
&& ![string equal $data(widget) $widget]} {
grid remove $data(widget)
$data(widget) configure -xscrollcommand "" -yscrollcommand ""
}
set data(widget) $widget
grid $widget -in $path -row 1 -column 1 -sticky news
$path.hscroll configure -command [list $widget xview]
$path.vscroll configure -command [list $widget yview]
$widget configure \
-xscrollcommand [list ScrolledWindow::_set_hscroll $path] \
-yscrollcommand [list ScrolledWindow::_set_vscroll $path]
}
proc ScrolledWindow::configure { path args } {
Widget::getVariable $path data
set res [Widget::configure $path $args]
if { [Widget::hasChanged $path -background bg] } {
$path configure -background $bg
catch {$path.hscroll configure -background $bg}
catch {$path.vscroll configure -background $bg}
}
if {[Widget::hasChanged $path -scrollbar scrollbar] | \
[Widget::hasChanged $path -auto auto] | \
[Widget::hasChanged $path -sides sides]} {
_setData $path $scrollbar $auto $sides
foreach {vmin vmax} [$path.hscroll get] { break }
set data(hsb,packed) [expr {$data(hsb,present) && \
(!$data(hsb,auto) || ($vmin != 0 || $vmax != 1))}]
foreach {vmin vmax} [$path.vscroll get] { break }
set data(vsb,packed) [expr {$data(vsb,present) && \
(!$data(vsb,auto) || ($vmin != 0 || $vmax != 1))}]
set data(ipad) [Widget::cget $path -ipad]
if {$data(hsb,packed)} {
grid $path.hscroll -column 1 -row $data(hsb,row) \
-sticky ew -ipady $data(ipad)
} else {
if {![info exists data(hlock)]} {
set data(hsb,packed) 0
grid remove $path.hscroll
}
}
if {$data(vsb,packed)} {
grid $path.vscroll -column $data(vsb,column) -row 1 \
-sticky ns -ipadx $data(ipad)
} else {
if {![info exists data(hlock)]} {
set data(vsb,packed) 0
grid remove $path.vscroll
}
}
}
return $res
}
proc ScrolledWindow::cget { path option } {
return [Widget::cget $path $option]
}
proc ScrolledWindow::_set_hscroll { path vmin vmax } {
Widget::getVariable $path data
if {$data(realized) && $data(hsb,present)} {
if {$data(hsb,auto) && ![info exists data(hlock)]} {
if {$data(hsb,packed) && $vmin == 0 && $vmax == 1} {
set data(hsb,packed) 0
grid remove $path.hscroll
set data(hlock) 1
update idletasks
unset data(hlock)
} elseif {!$data(hsb,packed) && ($vmin != 0 || $vmax != 1)} {
set data(hsb,packed) 1
grid $path.hscroll -column 1 -row $data(hsb,row) \
-sticky ew -ipady $data(ipad)
set data(hlock) 1
update idletasks
unset data(hlock)
}
}
$path.hscroll set $vmin $vmax
}
}
proc ScrolledWindow::_set_vscroll { path vmin vmax } {
Widget::getVariable $path data
if {$data(realized) && $data(vsb,present)} {
if {$data(vsb,auto) && ![info exists data(vlock)]} {
if {$data(vsb,packed) && $vmin == 0 && $vmax == 1} {
set data(vsb,packed) 0
grid remove $path.vscroll
set data(vlock) 1
update idletasks
unset data(vlock)
} elseif {!$data(vsb,packed) && ($vmin != 0 || $vmax != 1) } {
set data(vsb,packed) 1
grid $path.vscroll -column $data(vsb,column) -row 1 \
-sticky ns -ipadx $data(ipad)
set data(vlock) 1
update idletasks
unset data(vlock)
}
}
$path.vscroll set $vmin $vmax
}
}
proc ScrolledWindow::_setData {path scrollbar auto sides} {
Widget::getVariable $path data
set sb [lsearch {none horizontal vertical both} $scrollbar]
set auto [lsearch {none horizontal vertical both} $auto]
set data(hsb,present) [expr {($sb & 1) != 0}]
set data(hsb,auto) [expr {($auto & 1) != 0}]
set data(hsb,row) [expr {[string match *n* $sides] ? 0 : 2}]
set data(vsb,present) [expr {($sb & 2) != 0}]
set data(vsb,auto) [expr {($auto & 2) != 0}]
set data(vsb,column) [expr {[string match *w* $sides] ? 0 : 2}]
}
proc ScrolledWindow::_realize { path } {
Widget::getVariable $path data
bind $path <Configure> {}
set data(realized) 1
}
proc ScrolledWindow::_destroy { path } {
Widget::destroy $path
}
############ end of BWidget code ##############
############ iSpin GUI specific code: #########
set Fname ""
set Sname "ispin_session"
set lno 1
set Curp Mp
set s_typ 0
set seed 123
set skipstep 0
set ubstep 10000
set l_typ 0
set stop 0
set step 0
set maxn 0
set curn 0
set lno 0
set cnt 1
set msc_full 0
set negate_ltl 0
set var_vals 1
set vo 0 ;# verification output
set vr 0 ;# verification reference
set msc_x 75
set msc_y 20
set msc_w 75
set msc_h 20
set msc_max_x $msc_x
set msc_delay 25 ;# milliseconds update delay
set msc_max_w 20
set Varnm() 0
set VarStep() 0
set Levels() 0
set LineNo() 0
set MSC_Y() 0
set LineTouched() 0
set sym_pan ""
set note_pan ""
set nvr_pan ""
set log_pan ""
set bet(0) "Physical Memory Available (in Mbytes): "
set ival(0) 1024
set expl(0) "explain"
set bet(1) "Estimated State Space Size (states x 10^3): "
set ival(1) 1000
set expl(1) "explain"
set bet(2) "Maximum Search Depth (steps): "
set ival(2) 10000
set expl(2) "explain"
set bet(3) "Nr of hash-functions in Bitstate mode: "
set ival(3) 3
set expl(3) "explain"
set bet(4) "Size for Minimized Automaton"
set ival(4) 100
set expl(4) "explain"
set bet(5) "Extra Verifier Generation Options: "
set ival(5) ""
set expl(5) "explain"
set bet(6) "Extra Compile-Time Directives: "
set ival(6) "-O2"
set expl(6) "explain"
set bet(7) "Extra Run-Time Options: "
set ival(7) ""
set expl(7) "explain"
set estop 0
set s_mode 0
set po_mode 1
set bf_mode 0
set ma_mode 0
set cc_mode 0
set p_mode 0
set c_mode 0
set u_mode 1
set a_mode 1
set x_mode 0
set e_mode 1
set q_mode 0
set f_mode 0
set bc_mode 0
set it_mode 0
set sv_mode 0
set vpanel 0
set spanel 0
set pat "" ;# search pattern
set swarm_p(0) "minimum nr of hash functions:"
set swarm_i(0) "1"
set swarm_p(1) "maximum nr of hash functions:"
set swarm_i(1) "5"
set swarm_p(2) "minimum search depth:"
set swarm_i(2) "100"
set swarm_p(3) "maximum search depth:"
set swarm_i(3) "10000"
set swarm_p(4) "number of local cpu-cores"
set swarm_i(4) "4"
set swarm_p(5) "list of remote_cpu_name:ncores"
set swarm_i(5) ""
set swarm_p(6) "maximum memory per run (suffix: M or G)"
set swarm_i(6) "512M"
set swarm_p(7) "maximum total runtime for swarm (suffix: s, m, h, d)"
set swarm_i(7) "60m"
set swarm_p(8) "hash-factor"
set swarm_i(8) "1.5"
set swarm_p(9) "state-vector size in bytes"
set swarm_i(9) "512"
set swarm_p(10) "exploration speed in states/sec"
set swarm_i(10) "250000"
set so 0 ;# swarm cfg output
set sr 0 ;# swarm run output
set o_v 0
set o_y 30
proc add_frame {fn t} {
global TBG TFG
frame $fn -bg $TBG
label $fn.lbl -text "$t" -bg $TBG -fg $TFG
entry $fn.ent -relief sunken -width 10
pack $fn -side top -fill x -expand yes
pack $fn.lbl -side left -fill x -expand no
pack $fn.ent -side right -fill x -expand no
bind $fn.ent <Return> { run_sim }
}
proc do_find {} {
global twin pat
$twin tag remove hilite 0.0 end
forAllMatches $twin $pat
}
proc model_panel {t} {
global clog twin fg CBG CFG HV0 HV1 TBG TFG MFG NFG NBG pat ScrollBarSize Fname
global xzx
frame $t.buttons -bg $CBG
button $t.buttons.open -text "Open..." -command "open_spec 1" \
-bg $NBG -fg white -font $HV0 \
-activebackground $NFG -activeforeground $NBG
button $t.buttons.ref -text "ReOpen" -command "open_spec 0" \
-bg $NBG -fg white -font $HV0 \
-activebackground $NFG -activeforeground $NBG
button $t.buttons.save -text "Save" -command "save_spec 0" \
-bg $NBG -fg white -font $HV0 \
-activebackground $NFG -activeforeground $NBG
button $t.buttons.saveas -text "Save As..." -command "save_spec 1" \
-bg $NBG -fg white -font $HV0 \
-activebackground $NFG -activeforeground $NBG
button $t.buttons.syntax -text "Syntax Check" -command "runsyntax 0" \
-bg $NBG -fg $NFG -font $HV0 \
-activebackground $NFG -activeforeground $NBG
button $t.buttons.slice -text "Redundancy Check" -command "runsyntax 1" \
-bg $NBG -fg $NFG -font $HV0 \
-activebackground $NFG -activeforeground $NBG
button $t.buttons.symb -text "Symbol Table" -command "symbol_table" \
-bg $NBG -fg $NFG -font $HV0 \
-activebackground $NFG -activeforeground $NBG
button $t.buttons.fnd1 -text "Find:" \
-command "do_find" \
-bg $NBG -fg white -font $HV0 \
-activebackground $NFG -activeforeground $NBG
entry $t.buttons.fnd2 -width 24 -textvariable pat -bg ivory \
-relief sunken -background $TBG -foreground $TFG
bind $t.buttons.fnd2 <Return> { do_find }
pack $t.buttons -side top -fill x -expand no
pack $t.buttons.open $t.buttons.ref $t.buttons.save \
$t.buttons.saveas \
$t.buttons.syntax $t.buttons.slice \
$t.buttons.symb \
-side left -fill x -expand no
pack $t.buttons.fnd1 $t.buttons.fnd2 \
-side left -fill x -expand no
set pw [PanedWindow $t.pw -side left -activator button ]
set p2 [$pw add -minsize 100]
set p1 [$pw add -minsize 20]
set sw11 [ScrolledWindow $p1.sw -size $ScrollBarSize]
set clog [text $sw11.lb -height 15 -width 100 -highlightthickness 3 -bg $CBG -fg $CFG -font $HV1]
$sw11 setwidget $clog
pack $sw11 -fill both -expand yes
###
set xx [PanedWindow $p2.wide -side top -activator button ]
set q0 [$xx add -minsize 10]
set q1 [$xx add -minsize 10]
set sw22 [ScrolledWindow $q0.wide -size $ScrollBarSize]
set twin [text $sw22.lb -undo 1 -height 30 -highlightthickness 0 -font $HV1]
$sw22 setwidget $twin
pack $sw22 -side left -fill both -expand yes
$twin insert end "model source $Fname"
$twin edit modified false
global scrollxregion scrollyregion
set cv [ScrolledWindow $q1.wide -size $ScrollBarSize]
set fg [canvas $cv.right -relief raised \
-background $NBG -scrollregion "0 0 $scrollxregion $scrollyregion" ]
set xzx $fg
$cv setwidget $fg
frame $q1.ctl -bg $NBG
button $q1.ctl.mkg -text "Automata View" -command "mk_graphs" \
-bg $NBG -fg $NFG -font $HV0 \
-activebackground $NFG -activeforeground $NBG
button $q1.ctl.plus -text "zoom in" -command "$fg scale all 0 0 1.1 1.1" -width 10 \
-bg $NBG -fg $NFG -font $HV0 \
-activebackground $NFG -activeforeground $NBG
button $q1.ctl.minus -text "zoom out" -command "$fg scale all 0 0 0.9 0.9" -width 10 \
-bg $NBG -fg $NFG -font $HV0 \
-activebackground $NFG -activeforeground $NBG
pack $q1.ctl $q1.ctl.mkg -side left -fill x -expand no
pack $q1.ctl $q1.ctl.minus -side right -fill x -expand no
pack $q1.ctl $q1.ctl.plus -side right -fill x -expand no
pack $q1 $q1.ctl -side top
pack $cv -side right -fill both -expand yes
pack $xx -fill both -expand yes
pack $pw -fill both -expand yes
bind $twin <KeyRelease> {
if {"%K" == "Return"} {
$twin insert insert "[$twin index insert] "
$twin edit modified true
} }
bind $fg <2> "$fg scan mark %x %y"
bind $fg <B2-Motion> "$fg scan dragto %x %y"
}
proc checked_exit {} {
global twin
if {[$twin edit modified]} {
set answer [tk_messageBox -icon question -type yesno \
-message "There are unsaved changes. Really Quit?" ]
switch -- $answer {
yes { }
no { return }
}
}
destroy .
exit
}
proc mk_pan { t GC CC } {
global vo RM
set errmsg ""
$vo insert end $GC\n; update
set fd -1
catch {set fd [open "|$GC" r]} errmsg
if {$fd == -1} {
$vo delete 0.0 end
$vo insert end "error: $errmsg\n"
$vo yview end
return
} else {
while {[gets $fd line] > -1} {
$vo insert end "$line\n"
$vo yview end
update
}
catch " close $fd "
}
$vo insert end $CC\n; update
catch "eval exec $CC >& pan.tmp"
set fd -1
catch {set fd [open "pan.tmp" r]} errmsg
if {$fd == -1} {
$vo delete 0.0 end
$vo insert end "$errmsg\n"
$vo yview end
} else {
while {[gets $fd line] > -1} {
$vo insert end "$line\n"
$vo yview end
update
}
catch " close $fd "
}
catch { eval exec "$RM pan.tmp" }
update
}
proc run_pan { t VC d } {
global vr vo stop KILL
if {[auto_execok "./pan"] == ""} {
return
}
$vo insert end $VC\n; update
set fd -1
set pid [eval exec $VC >& run.tmp &]
$vo insert end "Pid: $pid\n"
$vo yview end
catch {set fd [open "run.tmp" r]} errmsg
if {$fd == -1} {
$vo insert end "error: $errmsg\n"
$vo yview end
return
}
set stop 0
set pname "--"
if {$d == 1} {
$vo delete 0.0 end
$vo insert end "proc\tfrom\ttrans\tto\tsrc\tstmnt\n"
$vo insert end "name\tstate\tid\tstate\n"
}
set no_errors 0
set seen_ln 0
while {$stop == 0} {
if {[gets $fd line] == -1} {
after 10
$vo yview end
update
if {$seen_ln == 0} {
# courtesy martin vuille
after 10
catch { close $fd }
set fd [open "run.tmp" r]
}
continue
}
set seen_ln 1
if {[string first "No tty allocated" $line] >= 0} {
continue
}
if {[string first "Valid Options are:" $line] >= 0} {
while {[gets $fd line] != -1} {
$vo insert end "$line\n"
update
}
set stop 2
}
if {[string first "pan: elapsed" $line] >= 0} {
set stop 2
}
if {$d == 0} {
$vo insert end "$line\n"
$vo yview end
update
if {[string first "State-vector " $line] >= 0} {
if {[string first "errors: 0" $line] >= 0} {
set no_errors 1
} }
continue
}
if {[string first "proctype" $line] == 0} {
set pname [string range $line 9 end]
$vo insert end "\n"
$vo yview end
continue
}
if {[string first "Transition" $line] >= 0 \
|| [string first "Source-State" $line] >= 0 \
|| [string first "Note:" $line] >= 0 \
|| [string first "pan:" $line] >= 0} {
continue
}
# format:
# state 15 -(tr 18)-> state 31 [id 14 tp 5] [----L] leader:36 => out!first,number
regexp {[A-Za-z0-9_\.]+:[0-9]+} $line matched ;# file:line
set pre [string first "\[" $line]
set frst [string range $line 0 $pre]
set lst [string range $line $pre end]
set arr [string first " => " $lst]; incr arr 4
set stmnt [string range $lst $arr end]
if {[scan $line "\tstate %d -(tr %d)-> state %d \[id %d tp %d\]" \
f1 f2 f3 f4 f5] == 5} {
$vo insert end "$pname\t$f1\t\[$f2\]\t$f3\t$matched\t$stmnt\n"
} else {
$vo insert end "$line\n"
} }
if {$stop == 1} {
catch "eval exec $KILL $pid"
$vo insert end "stopped\n"
while {[gets $fd line] != -1} {
$vo insert end "$line\n"
$vo yview end
update
} }
catch " close $fd " errmsg
if {$errmsg != "" && [string first "No tty allocated" $errmsg] < 0} {
$vo insert end "$errmsg\n"
}
$vo yview end
if {$no_errors == 0} {
$vo insert end "To replay the error-trail, goto Simulate/Replay and select \"Run\"\n"
} else {
$vo insert end "No errors found -- did you verify all claims?\n"
}
bind_lines $vo $vr
update
}
proc log { n } {
set m 1
set cnt 0
while {$m<$n} {
set m [expr $m*2]
incr cnt
}
return $cnt
}
proc run_tbl { t } {
global Fname CC
if {$Fname == ""} { return }
mk_pan $t "spin -a [$t.top.right.row5.ent get] $Fname" "$CC -w -o pan pan.c"
run_pan $t "./pan -d" 1
cleanup
}
proc has_label {s dargs} {
global vr SPIN Fname
set ST "$SPIN -d $dargs $Fname"
set result 0
catch {set fd [open "|$ST" r]} errmsg
if {$fd == -1} {
$vr insert end "$errmsg\n"
$vr yview end
update
} else {
while {[gets $fd line] > -1} {
if {[string first "label $s" $line] >= 0} {
set result 1
break
} }
catch " close $fd "
}
return $result
}
proc check_sanity {gargs} {
global p_mode vo
if {[has_label "accept" $gargs] == 1} {
if {$p_mode != 2} {
$vo insert end "warning: model has accept states\n"
}
} else {
if {$p_mode == 2} {
$vo insert end "error: model has no accept states\n"
return 0
} }
if {[has_label "progress" $gargs] == 1} {
if {$p_mode != 1} {
$vo insert end "warning: model has progress states\n"
}
} else {
if {$p_mode == 1} {
$vo insert end "error: model has no progress states\n"
return 0
} }
$vo yview end
return 1
}
proc run_ver { t } {
global Fname q_mode f_mode bc_mode it_mode sv_mode
global bet ival expl estop s_mode po_mode bf_mode e_mode
global ma_mode cc_mode p_mode c_mode u_mode a_mode x_mode
global nvr_pan sym_pan SPIN CC vo peg vranges LTL_Panel
global V_Panel_1 V_Panel_3
set nc_nm ""
set match_start ""
set gargs "-a"
if {$q_mode} { set gargs "$gargs -m" }
if {$peg == 1} { set gargs "$gargs -o3" }
if {$c_mode == 2} {
catch { exec $SPIN -e $Fname > "never_claim.tmp" } errmsg
if {$errmsg != ""} {
$vo insert end $errmsg\n
$vo yview end
return
}
set nc_nm "Product"
set gargs "$gargs -N never_claim.tmp"
if {[check_sanity $gargs] == 0} {
$vo yview end
return
} }
if {$c_mode == 1} {
if {$LTL_Panel} {
if [catch { set fd [open "never_claim.tmp" w] } errmsg] {
$vo insert end $errmsg\n
$vo yview end
return
}
puts $fd [$sym_pan get 0.0 end]
puts $fd [$nvr_pan get 0.0 end]
regexp {never .*\{} [$nvr_pan get 0.0 end] match_start
if {$match_start == ""} {
$vo insert end "error: cannot find never claim\n"
$vo yview end
return
}
set match_end [string first " \{" $match_start]
if {$match_end > 0} {
incr match_end -1
}
set nc_nm [string range $match_start 6 $match_end]
# $vo insert end "\nusing claim: \'$nc_nm\'\n\n"
# $vo yview end
catch "close $fd"
set gargs "$gargs -N never_claim.tmp"
if {[check_sanity $gargs] == 0} {
$vo yview end
return
}
$vo insert end "wrote never_claim.tmp\n"
} else {
set nc_nm [$t.top.fourth.rowA.nr get]
}
}
$vo yview end
update
if {$V_Panel_3} {
set cargs "-DMEMLIM=[$t.top.right.row0.ent get] [$t.top.right.row6.ent get]"
} else {
set cargs "-DMEMLIM=$ival(0) $ival(6)"
}
if {$s_mode == 1} { set cargs "$cargs -DBITSTATE" }
if {$s_mode == 2} { set cargs "$cargs -DHC4" }
if {$V_Panel_3} {
if {$ma_mode == 1} { set cargs "$cargs -DMA=[$t.top.right.row4.ent get]" }
if {$ma_mode == 1} { set cargs "$cargs -DMA=$ival(4)" }
} else {
}
if {$bf_mode == 1} { set cargs "$cargs -DBFS" }
if {$x_mode == 0} { set cargs "$cargs -DXUSAFE" }
if {$p_mode == 0} { set cargs "$cargs -DSAFETY" }
if {$p_mode == 1} { set cargs "$cargs -DNP" }
if {$c_mode == 0} { set cargs "$cargs -DNOCLAIM" }
if {$cc_mode == 1} { set cargs "$cargs -DCOLLAPSE" }
if {$bc_mode == 1} { set cargs "$cargs -DBCS" }
if {$it_mode == 1} { set cargs "$cargs -DREACH" }
if {$po_mode == 0} { set cargs "$cargs -DNOREDUCE" }
if {$peg == 1} { set cargs "$cargs -DPEG" }
if {$vranges == 1} { set cargs "$cargs -DVAR_RANGES" }
if {$V_Panel_3} {
set vargs "-m[$t.top.right.row2.ent get] [$t.top.right.row7.ent get]"
if {$s_mode == 1} { set vargs "$vargs -k[$t.top.right.row3.ent get]" }
} else {
set vargs "-m$ival(2) $ival(7)"
if {$s_mode == 1} { set vargs "$vargs -k$ival(3)" }
}
if {$e_mode == 0} { set vargs "$vargs -E" }
if {$a_mode == 0} { set vargs "$vargs -A" }
if {$p_mode == 1} { set vargs "$vargs -l" }
if {$p_mode == 2} { set vargs "$vargs -a" }
if {$f_mode == 1} { set vargs "$vargs -f" }
if {$u_mode == 0} { set vargs "$vargs -n" }
if {$it_mode == 1} { set vargs "$vargs -i" }
if {$estop == 1} { set vargs "$vargs -c0" }
if {$V_Panel_1} {
if {$estop == 0} { set vargs "$vargs -c[$t.top.middle.row1.nr get]" }
}
if {$sv_mode == 1} { set vargs "$vargs -e" }
if {$s_mode == 1} {
if {$V_Panel_3} {
set vargs "$vargs -w[expr 10+[log [$t.top.right.row1.ent get]]]"
} else {
set vargs "$vargs -w[expr 10+[log $ival(1)]]"
} }
if {$bc_mode == 1} {
set vargs "$vargs -L[$t.top.third.rowB.ent get]"
}
if {$nc_nm != ""} { set vargs "$vargs -N $nc_nm" }
if {$V_Panel_3} {
set GC "$SPIN $gargs [$t.top.right.row5.ent get] $Fname"
} else {
set GC "$SPIN $gargs $ival(5) $Fname"
}
set CL "$CC $cargs -w -o pan pan.c"
set VC "./pan $vargs"
$vo yview end
update
mk_pan $t $GC $CL
run_pan $t $VC 0
cleanup
}
proc stop_ver { t } {
global stop
set stop 1
}
proc useful_info { sr cmd } {
catch { set fd [open "|$cmd" r] } errmsg
if {$fd == -1} {
$sr insert end "error: $errmsg"
return
}
while {[gets $fd line] > -1} {
$sr insert end "$line\n"
$sr yview end
update
}
catch "close $fd" errmsg
$sr insert end "$errmsg\n"
$sr yview end
update
}
proc swarm_gen { t } {
global so sr Fname SWARM
if {[auto_execok $SWARM] == ""} {
add_log "no swarm command is installed on this system" 0
add_log "it is available from: http://spinroot.com/swarm/" 0
tk_messageBox -icon info -message "No executable $SWARM found..."
return
}
if [catch {set fd [open "swarm_cfg.tmp" w]} errmsg] {
$so insert end "error: cannot write swarm_cfg.tmp\n"
return
}
puts $fd "## Swarm Version 3.0 -- 16 August 2010"
puts $fd "#"
puts $fd "# range"
puts $fd "k [$t.top.left.row0.e0 get] [$t.top.left.row1.e0 get]\n"
puts $fd "# limits"
puts $fd "d [$t.top.left.row3.e0 get]" ;# later also add min: [$t.top.left.row2.e0 get]
puts $fd "cpus [$t.top.left.row4.e0 get] [$t.top.left.row5.e0 get]"
puts $fd "memory [$t.top.left.row6.e0 get]"
puts $fd "time [$t.top.left.row7.e0 get]"
puts $fd "hash [$t.top.middle.row8.e1 get]"
puts $fd "vector [$t.top.middle.row9.e1 get]"
puts $fd "speed [$t.top.middle.row10.e1 get]"
puts $fd "file $Fname\n"
puts $fd "# compilation options"
puts $fd "[$t.top.right.row0 get 0.0 end]"
puts $fd "# runtime options (one line only)"
puts $fd "[$t.top.middle.row12.e1 get]\n"
puts $fd "# spin options other than -a (one line only)"
puts $fd "[$t.top.middle.row11.e1 get]\n"
catch "close $fd" errmsg
$so insert end "generated configuration file\n"
catch { set fd [open "|$SWARM swarm_cfg.tmp" r] } errmsg
if {$fd == -1} {
$so insert end "error: $errmsg"
return
}
while {[gets $fd line] > -1} {
$so insert end "$line\n"
$so yview end
update
}
catch "close $fd" errmsg
$so insert end "done:: $errmsg \n"
$so yview end
update
$so insert end "----Running----\n"
$so yview end
update
set nxn [string first "." $Fname]
if {$nxn > 0} {
incr nxn -1
set sFname [string range $Fname 0 $nxn]
} else {
set sFname $Fname
}
## untested:
if {[string first "C:" $sFname] >= 0 || [string first "/" $sFname] == 0} {
catch { set fd [open "|sh $sFname*.swarm" r] } errmsg
} else {
catch { set fd [open "|sh ./$sFname*.swarm" r] } errmsg
}
if {$fd == -1} {
$so insert end "error: $errmsg"
return
}
while {[gets $fd line] > -1} {
$so insert end "$line\n"
$so yview end
update
}
catch "close $fd" errmsg
$so insert end "run completed\n$errmsg\n"
$so yview end
update
useful_info $sr "grep -e errors: script*.out"
useful_info $sr "ls -l *.trail"
}
proc swarm_clean { } {
global Fname so RM
cleanup
catch { eval exec $RM swarm_cfg.tmp $Fname.swarm script* } err
$so insert end $err\n
$so yview end
}
proc swarm_panel { t } {
global swarm_p swarm_i CBG CFG TBG TFG NBG NFG HV0 HV1
global SWARM so sr ScrollBarSize spanel
set spanel $t
frame $t.top -bg $TBG
pack $t.top -side top -fill both -expand no
frame $t.top.left -bg $TBG
frame $t.top.middle -bg $TBG
frame $t.top.right -bg $TBG
pack $t.top.left $t.top.middle $t.top.right -side left -fill both -expand no
set p1 $t.top.left
label $p1.limits -text "Search Constraints" -relief sunken -bg $TBG -fg $TFG
pack $p1.limits -side top -fill x -expand no
for {set i 0} {$i < 8} {incr i} {
frame $p1.row$i -bg $TBG
label $p1.row$i.k0 -text "$swarm_p($i)" -bg $TBG -fg $TFG
entry $p1.row$i.e0 -relief sunken
$p1.row$i.e0 insert end "$swarm_i($i)"
pack $p1.row$i.k0 -side left -fill x -expand no
pack $p1.row$i.e0 -side right -fill x -expand no
pack $p1.row$i -side top -fill x -expand no
}
set p2 $t.top.middle
label $p2.limits -text "Estimates (Fine Tuning)" -relief sunken -bg $TBG -fg $TFG
pack $p2.limits -side top -fill x -expand no
for {set i 8} {$i < 11} {incr i} {
frame $p2.row$i -bg $TBG
label $p2.row$i.k1 -text "$swarm_p($i)" -bg $TBG -fg $TFG
entry $p2.row$i.e1 -relief sunken
$p2.row$i.e1 insert end "$swarm_i($i)"
pack $p2.row$i.k1 -side left -fill x -expand no
pack $p2.row$i.e1 -side right -fill x -expand no
pack $p2.row$i -side top -fill x -expand no
}
label $p2.other -text "Model Generation" -relief sunken -bg $TBG -fg $TFG
pack $p2.other -side top -fill x -expand no
frame $p2.row11 -bg $TBG
label $p2.row11.k1 -text "extra spin args" -bg $TBG -fg $TFG
entry $p2.row11.e1 -relief sunken
pack $p2.row11.k1 -side left -fill x -expand no
pack $p2.row11.e1 -side right -fill x -expand no
pack $p2.row11 -side top -fill x -expand no
frame $p2.row12 -bg $TBG
label $p2.row12.k1 -text "extra pan args" -bg $TBG -fg $TFG
entry $p2.row12.e1 -relief sunken
$p2.row12.e1 insert end "-c1 -x -n"
pack $p2.row12.k1 -side left -fill x -expand no
pack $p2.row12.e1 -side right -fill x -expand no
pack $p2.row12 -side top -fill x -expand no
frame $p2.buttons -bg $TBG
button $p2.buttons.run -text "Run" -command "swarm_gen $t" \
-bg $NBG -fg $NFG -font $HV0 \
-activebackground $NFG -activeforeground $NBG
button $p2.buttons.cln -text "Cleanup tmp files" -command "swarm_clean" \
-bg $NBG -fg $NFG -font $HV0 \
-activebackground $NFG -activeforeground $NBG
pack $p2.buttons.cln -side right -fill x -expand no
pack $p2.buttons.run -side right -fill x -expand no
pack $p2.buttons -side bottom -fill x -expand no
set p3 $t.top.right
label $p3.limits -text "Compilation Options (any number, one per line)" \
-relief sunken -bg $TBG -fg $TFG
text $p3.row0 -height 12 -relief sunken
$p3.row0 insert end "-DBITSTATE -DPUTPID # basic dfs\n"
$p3.row0 insert end "-DBITSTATE -DPUTPID -DREVERSE # reversed transition ordering\n"
$p3.row0 insert end "-DBITSTATE -DPUTPID -DT_REVERSE # reversed process ordering\n"
$p3.row0 insert end "-DBITSTATE -DPUTPID -DREVERSE -DT_REVERSE # both\n"
$p3.row0 insert end "-DBITSTATE -DPUTPID -DP_RAND -DT_RAND # same series with randomization\n"
$p3.row0 insert end "-DBITSTATE -DPUTPID -DP_RAND -DT_RAND -DT_REVERSE\n"
$p3.row0 insert end "-DBITSTATE -DPUTPID -DP_RAND -DT_RAND -DREVERSE\n"
$p3.row0 insert end "-DBITSTATE -DPUTPID -DP_RAND -DT_RAND -DREVERSE -DT_REVERSE\n"
pack $p3.limits $p3.row0 -side top -fill x -expand no
# frame $p3.row2
# label $p3.row2.k1 -text "runtime options" -bg $TBG -fg $TFG
# entry $p3.row2.e1 -relief sunken -bg $TBG -fg $TFG
# $p3.row2.e1 insert end "-c1 -x -n"
# pack $p3.row2.k1 $p3.row2.e1 -side top -fill x -expand no
# pack $p3.row2 -side top -fill x -expand no
set vw [PanedWindow $t.bottom -side left -activator button ]
set p8 [$vw add -minsize 100]
set p9 [$vw add -minsize 100]
set s11 [ScrolledWindow $p8.so -size $ScrollBarSize] ;# so - swarm output
set so [text $s11.lb -height 5 -highlightthickness 3 -font $HV1]
$s11 setwidget $so
set s22 [ScrolledWindow $p9.sr -size $ScrollBarSize] ;# sr - swarm run
set sr [text $s22.lb -highlightthickness 0 -bg $CBG -fg $CFG -font $HV1]
$s22 setwidget $sr
$so insert end "swarm setup output\n"
$sr insert end "swarm run output\n"
set errmsg ""
# a bit overkill, but execs compiled with gcc
# behave differently from those compiled with cl
# complaints about missing tty, for instance
# spin on cygwin is compiled with cl, swarm with gcc
if {[auto_execok $SWARM] == ""} {
$sr insert end "no 'swarm' command is found\n"
$sr insert end "available from: http://spinroot.com/swarm/\n"
} else {
catch { set fd [open "|$SWARM -V" r] } errmsg
if {$fd == -1} {
$sr insert end "$errmsg\n"
} else {
while {[gets $fd line] > -1} {
$sr insert end "$line\n"
}
catch " close $fd "
} }
pack $s11 -fill both -expand yes
pack $s22 -fill both -expand yes
pack $vw -fill both -expand yes
}
proc explain0 {} {
global vo
$vo insert end "\n"
$vo insert end "\tPhysical Memory Available:\n"
$vo insert end "\tSet this number to amount of physical (not virtual) memory\n"
$vo insert end "\tin your system, in MegaBytes, and leave it there for all runs.\n"
$vo insert end "\n"
$vo insert end "\tWhen the limit is reached, the verification is stopped to\n"
$vo insert end "\tavoid trashing.\n"
$vo insert end "\n"
$vo insert end "\tIf an exhaustive verification cannot be completed due to\n"
$vo insert end "\tlack of memory, select a different storage mode.\n\n"
$vo yview end
}
proc explain1 {} {
global vo
$vo insert end "\tEstimated State Space Size:\n"
$vo insert end "\tThis parameter is used to calculate the size of the\n"
$vo insert end "\thash-table. It results in a selection of a numeric argument\n"
$vo insert end "\tfor the -w flag of the verifier. Setting it too high may\n"
$vo insert end "\tcause an out-of-memory error with zero states reached\n"
$vo insert end "\t(meaning that the verification could not be started).\n"
$vo insert end "\tSetting it too low can cause inefficiencies due to\n"
$vo insert end "\thash collisions.\n"
$vo insert end "\t\n"
$vo insert end "\tWhen using bitstate, start with the default\n"
$vo insert end "\tsetting. After a run completes successfully,\n"
$vo insert end "\tdouble the estimate, and see if the number of reached\n"
$vo insert end "\tstated changes much. Continue to do this until\n"
$vo insert end "\tit stops changing, or until you reach the memory bound.\n"
$vo insert end "\t\n"
$vo insert end "\tiSpin uses the closest power of two to determine the parameter\n"
$vo insert end "\tgiven to the -w flag that is used for the run.\n\n"
$vo yview end
}
proc explain2 {} {
global vo
$vo insert end "\tMaximum Search Depth:\n"
$vo insert end "\tThis number determines the size of the depth-first\n"
$vo insert end "\tsearch stack that is used during the verification.\n"
$vo insert end "\tA larger number increases the memory requirements, and\n"
$vo insert end "\ta lower number decreases it. When there seems not to be\n"
$vo insert end "\tsufficient memory for the search depth needed, reduce\n"
$vo insert end "\treduce the estimated state space size to free some\n"
$vo insert end "\tmore memory for the stack, or change the storage mode.\n"
$vo insert end "\t\n"
$vo insert end "\tIf you hit the maximum search depth during a verification\n"
$vo insert end "\t(noted as 'Search not completed' or 'Search Truncated'\n"
$vo insert end "\tin the verification output) without finding an error,\n"
$vo insert end "\tincrease the search depth parameter and repeat the run.\n\n"
$vo yview end
}
proc explain3 {} {
global vo
$vo insert end "\tNumber of hash functions:\n"
$vo insert end "\tThis number determines how many bits are set per\n"
$vo insert end "\tstate when in Bitstate verification mode. The default is 3,\n"
$vo insert end "\tbut you can use any number greater to or equal to 1.\n"
$vo insert end "\tAt the end of a Bitstate verification run, the verifier\n"
$vo insert end "\tcan issue a recommendation for a different setting of\n"
$vo insert end "\tthis parameter (specified with the -k flag), if this can\n"
$vo insert end "\timprove coverage.\n\n"
$vo yview end
}
proc explain4 {} {
global vo
$vo insert end "\tSize for Minimized Automata:\n"
$vo insert end "\tWhen using the minimized automata storage mode, you should\n"
$vo insert end "\tset this parameter to be equal to the statevector size at first.\n"
$vo insert end "\tAt the end of the run, the verifier will then report if a smaller\n"
$vo insert end "\tnumber can also be used. The smaller the number the faster the run.\n\n"
$vo yview end
}
proc explain5 {} {
global vo
$vo insert end "\tExtra Verifier Generator Options:\n"
$vo insert end "\tPossible options include:\n"
$vo insert end "\t-o1 to disable dataflow optimizations\n"
$vo insert end "\t-o2 to disable dead-variable elimination\n"
$vo insert end "\t-o3 to disable statement merging (which improves source-line references)\n\n"
$vo yview end
}
proc explain6 {} {
global vo
$vo insert end "\tExtra Compile-time Directives:\n"
$vo insert end "\tFor possible options see:\n"
$vo insert end "\thttp://spinroot.com/spin/Man/Pan.html#B\n\n"
$vo yview end
}
proc explain7 {} {
global vo
$vo insert end "\tExtra Run-time Options:\n"
$vo insert end "\tPossible options include:\n"
$vo insert end "\t-hN use a different hash-function (N: 1..32, default 1)\n"
$vo insert end "\t-J reverse evaluation order on nested unless structures\n"
$vo insert end "\t-q require channels to be empty in valid endstates\n"
$vo insert end "\t-QN try to stop the run after N minutes\n"
$vo insert end "\t-tSuf use Suf as a suffix on trail files instead of .trail\n"
$vo insert end "\t-T create trail files in read-only mode\n"
$vo insert end "\t-x do not overwrite an existing trail file\n\n"
$vo yview end
}
proc ver_help {} {
global vo
$vo insert end "\tHelp with Verification Complexity:\n"
$vo insert end "\t---------------------------------------\n"
$vo insert end "\tWhen a verification cannot be completed because it\n"
$vo insert end "\truns out of memory or you run out of time, there are\n"
$vo insert end "\tsome useful strategies that can be tried to restore tractability.\n"
$vo insert end "\n"
$vo insert end "\t0. Run the Redundancy Check (in the Edit/View tab) to see if you can\n"
$vo insert end "\tsimplify the model and still prove the same properties.\n"
$vo insert end "\n"
$vo insert end "\t1. Try to make the model more general.\n"
$vo insert end "\tRemember that you are constructing a verification model and not\n"
$vo insert end "\tan implementation. The model checker is good at proving properties\n"
$vo insert end "\tof *interactions* in a distributed system (the implicit assumptions\n"
$vo insert end "\tthat processes make about each other) -- it is generally not strong\n"
$vo insert end "\tin proving things about *computations*, data dependencies etc.\n"
$vo insert end "\n"
$vo insert end "\t2. Remove everything that is not directly related to the property\n"
$vo insert end "\tyou are trying to prove: redundant computations, redundant data. \n"
$vo insert end "\t*Avoid counters*; avoid incrementing variables that are used for\n"
$vo insert end "\tonly book-keeping purposes.\n"
$vo insert end "\tThe Syntax Check option (Edit/View tab) warns about the gravest offenses.\n"
$vo insert end "\n"
$vo insert end "\t3. Asynchronous channels can be a significant source of complexity in\n"
$vo insert end "\tverification. Use *synchronous channels* where possible. Reduce the\n"
$vo insert end "\tnumber of slots in asynchronous channels to a minimum (use 2, or 3\n"
$vo insert end "\tslots to get started).\n"
$vo insert end "\n"
$vo insert end "\t4. Look for processes that merely transfer messages. Consider if\n"
$vo insert end "\tyou can remove processes that only copy incoming messages from\n"
$vo insert end "\tone channel into another, by letting the sender generate the\n"
$vo insert end "\tfinal message right away. If the intermediate process makes\n"
$vo insert end "\tchoices (e.g., to delete or duplicate, etc.), let the sender\n"
$vo insert end "\tmake that choice, rather than an intermediate process.\n"
$vo insert end "\n"
$vo insert end "\t5. Combine local computations into atomic, or d_step, sequences.\n"
$vo insert end "\n"
$vo insert end "\t6. Avoid leaving scratch data around in variables. You can often reduce\n"
$vo insert end "\tthe number of states by, for instance, resetting local variables\n"
$vo insert end "\tthat are used inside atomic sequences to zero at the end of those\n"
$vo insert end "\tsequences; so that the scratch values aren't visible outside the\n"
$vo insert end "\tsequence. Consider using the predefined variable \"_\" as a write-only\n"
$vo insert end "\tscratch variable where possible.\n"
$vo insert end "\n"
$vo insert end "\t7. Try to combine the behavior of two processes into one.\n"
$vo insert end "\tGeneralize behavior. Focus on coordination aspects\n"
$vo insert end "\t(i.e., the interfaces between processes, rather than the local\n"
$vo insert end "\tcomputations inside processes).\n"
$vo insert end "\n"
$vo insert end "\t8. Try to exploit the partial order reduction strategies.\n"
$vo insert end "\tUse the xr and xs assertions where possible (see the online manpages\n"
$vo insert end "\tat spinroot.com; avoid sharing channels between multiple receivers or\n"
$vo insert end "\tmultiple senders.\n"
$vo insert end "\tAvoid merging independent data-streams into a single shared channel.\n"
$vo yview end
}
proc del_v_panel {n} {
global vpanel
if {$n == 1} {
catch { destroy $vpanel.top.middle }
}
if {$n == 2} {
catch { destroy $vpanel.top.third }
}
if {$n == 3} {
catch { destroy $vpanel.top.right }
}
}
proc toggle_a {n} {
global V_Panel_1 V_Panel_3 vpanel LIB NBG HV0 NFG
if {$n == 1} {
if {$V_Panel_1} {
set V_Panel_1 0
set p6 $vpanel.top.middle
catch {
destroy $p6.er
destroy $p6.lb
destroy $p6.row0
destroy $p6.row1
destroy $p6.row2
destroy $p6.row4
destroy $p6.row5
destroy $p6.row7
destroy $p6.row8
destroy $p6.rowA
destroy $p6.row66
}
frame $p6.row66 -bg $LIB
button $p6.row66.a1 -text "Show\nError\nTrapping\nOptions" \
-command "toggle_a 1" \
-fg white -bg black -activeforeground $NBG \
-activebackground $NFG -font $HV0
pack $p6.row66.a1 -side left -fill x -expand yes
pack $p6.row66 -side top -fill x -expand yes
} else {
set V_Panel_1 1
$vpanel.top.middle.row66.a1 configure -text "Remove"
advanced_1
} }
if {$n == 3} {
if {$V_Panel_3} {
set V_Panel_3 0
set p6 $vpanel.top.right
catch {
destroy $p6.t
for {set i 0} {$i <= 7} {incr i} {
destroy $p6.row$i
}
destroy $p6.row66
}
frame $p6.row66 -bg $LIB
button $p6.row66.a3 -text "Show\nAdvanced\nParameter\nSettings" \
-command "toggle_a 3" \
-fg white -bg black -activeforeground $NBG \
-activebackground $NFG -font $HV0
pack $p6.row66.a3 -side left -fill x -expand yes
pack $p6.row66 -side top -fill x -expand yes
} else {
set V_Panel_3 1
$vpanel.top.right.row66.a3 configure -text "Remove"
advanced_3
} }
}
set peg 0
set vranges 0
set sv_mode 0
set estop 0
set q_mode 0
proc advanced_1 {} {
global LIB TFG NFG NBG HV0 vpanel V_Panel_1
global peg sv_mode estop vranges q_mode
set t $vpanel
set p6 $t.top.middle
label $p6.er -text "Advanced: Error Trapping" -relief raised -bg $LIB
frame $p6.row0 -bg $LIB
radiobutton $p6.row0.ds -variable estop -value 1 -text "don't stop at errors" -bg $LIB -fg $TFG
pack $p6.row0.ds -side left -fill x -expand no
frame $p6.row1 -bg $LIB
radiobutton $p6.row1.st -variable estop -value 0 -text "stop at error nr:" -bg $LIB -fg $TFG
entry $p6.row1.nr
$p6.row1.nr insert end "1"
pack $p6.row1.st -side left -fill x -expand no
pack $p6.row1.nr -side right -fill x -expand yes
frame $p6.row2 -bg $LIB
checkbutton $p6.row2.se -variable sv_mode -text "save all error-trails" -bg $LIB -fg $TFG
pack $p6.row2.se -side left -fill x -expand no
frame $p6.row4 -bg $LIB
checkbutton $p6.row4.ac -variable peg -text "add complexity profiling" -bg $LIB -fg $TFG
pack $p6.row4.ac -side left -fill x -expand no
frame $p6.row5 -bg $LIB
checkbutton $p6.row5.vr -variable vranges -text "compute variable ranges" -bg $LIB -fg $TFG
pack $p6.row5.vr -side left -fill x -expand no
pack $p6.er $p6.row0 $p6.row1 $p6.row2 $p6.row4 $p6.row5 \
-side top -fill x -expand yes
label $p6.lb -text "A Full Channel" -relief raised -bg $LIB -fg $TFG
frame $p6.row7 -bg $LIB
radiobutton $p6.row7.b -variable q_mode -value 0 -text "blocks new msgs" -bg $LIB -fg $TFG
pack $p6.row7.b -side left -fill x -expand no
frame $p6.row8 -bg $LIB
radiobutton $p6.row8.l -variable q_mode -value 1 -text "loses new msgs" -bg $LIB -fg $TFG
pack $p6.row8.l -side left -fill x -expand no
frame $p6.rowA -bg $LIB
button $p6.rowA.tb -text "State Tables" \
-command " run_tbl $t " \
-fg white -bg grey -activeforeground $NBG -activebackground $NFG -font $HV0
button $p6.rowA.clr -text "Clear" -command " do_clear " \
-fg white -bg grey -activeforeground $NBG -activebackground $NFG -font $HV0
button $p6.rowA.hlp -text "Help" -command " ver_help " \
-fg white -bg grey -activeforeground $NBG -activebackground $NFG -font $HV0
pack $p6.rowA.tb $p6.rowA.clr $p6.rowA.hlp -side left -fill x -expand yes
pack $p6.lb $p6.row7 $p6.row8 $p6.rowA -side top -fill x -expand no
}
proc advanced_2 {} {
global TFG NFG NBG HV0 vpanel TBG
global po_mode bf_mode bc_mode it_mode u_mode
set LIB $TBG ;# overrides global
set t $vpanel
set p5 $t.top.third
label $p5.sm -text "Search Mode" -relief raised -bg $LIB -fg $TFG
frame $p5.row5 -bg $LIB
label $p5.row5.sp -width 1 -bg $LIB -fg $TFG
checkbutton $p5.row5.po -variable po_mode -text "+ partial order reduction" -bg $LIB -fg $TFG
pack $p5.row5.sp $p5.row5.po -side left -fill x -expand no
frame $p5.row6 -bg $LIB
radiobutton $p5.row6.dfs -variable bf_mode -value 0 -text "depth-first search" -bg $LIB -fg $TFG
pack $p5.row6.dfs -side left -fill x -expand no
frame $p5.row60 -bg $LIB
label $p5.row60.sp -width 1 -bg $LIB -fg $TFG
checkbutton $p5.row60.fs -variable bc_mode -text "+ bounded context switching" -bg $LIB -fg $TFG
pack $p5.row60.sp $p5.row60.fs -side left -fill x -expand no
frame $p5.rowB -bg $LIB
label $p5.rowB.sp -width 6 -bg $LIB -fg $TFG
label $p5.rowB.nm -text "with bound:" -bg $LIB -fg $TFG
entry $p5.rowB.ent -relief sunken -width 8
$p5.rowB.ent insert end "0"
pack $p5.rowB.sp $p5.rowB.nm -side left -fill x -expand no
pack $p5.rowB.ent -side left -fill x -expand yes
frame $p5.row61 -bg $LIB
label $p5.row61.sp -width 1 -bg $LIB -fg $TFG
checkbutton $p5.row61.fs -variable it_mode -text "+ iterative search for short trail" -bg $LIB -fg $TFG
pack $p5.row61.sp $p5.row61.fs -side left -fill x -expand no
frame $p5.row62 -bg $LIB
label $p5.row62.sp -width 1 -bg $LIB -fg $TFG
checkbutton $p5.row62.po -variable po_mode -text "+ partial order reduction" -bg $LIB -fg $TFG
pack $p5.row62.sp $p5.row62.po -side left -fill x -expand no
frame $p5.row7 -bg $LIB
radiobutton $p5.row7.bfs -variable bf_mode -value 1 -text "breadth-first search" -bg $LIB -fg $TFG
pack $p5.row7.bfs -side left -fill x -expand no
frame $p5.row8 -bg $LIB
checkbutton $p5.row8.ur -variable u_mode -text "report unreachable code" -bg $LIB -fg $TFG
pack $p5.row8.ur -side left -fill x -expand no
frame $p5.row9 -bg $LIB
entry $p5.row9.en -relief sunken -width 12
button $p5.row9.lb -text "Save Result in:" \
-command " save_in $p5.row9.en" \
-bg grey -fg white \
-activeforeground $NBG -activebackground $NFG -font $HV0
$p5.row9.en insert end "pan.out"
pack $p5.row9.lb $p5.row9.en -side left -fill y -expand yes
pack $p5.sm $p5.row6 $p5.row62 $p5.row60 $p5.rowB $p5.row61 $p5.row7 $p5.row5 $p5.row8 $p5.row9 \
-side top -fill x -expand no
}
proc advanced_3 {} {
global bet ival expl LIB TFG NFG NBG HV0 vpanel V_Panel_3
set t $vpanel
set p7 $t.top.right
label $p7.t -text "Advanced: Parameters" -relief raised -bg $LIB -fg $TFG
pack $p7.t -side top -fill x -expand no
for {set i 0} {$i <= 7} {incr i} {
frame $p7.row$i -bg $LIB
label $p7.row$i.lbl -text $bet($i) -bg $LIB -fg $TFG
entry $p7.row$i.ent -width 20
$p7.row$i.ent insert end $ival($i)
button $p7.row$i.exp -text $expl($i) -command " explain$i " -bg $LIB -fg $TFG
pack $p7.row$i.lbl -side left -fill x -expand no
pack $p7.row$i.exp -side right -fill x -expand no
pack $p7.row$i.ent -side right -fill x -expand no
pack $p7.row$i -side top -fill x -expand no
}
}
proc verify_panel {t} {
global bet ival expl estop s_mode po_mode bf_mode e_mode HV0 HV1 CBG CFG TBG TFG NBG NFG it_mode
global ma_mode cc_mode p_mode c_mode u_mode a_mode x_mode q_mode f_mode bc_mode
global sv_mode vo vr Fname ScrollBarSize peg vranges vpanel
global LTL_Panel V_Panel_1 V_Panel_3 LIB
set vpanel $t
set LIB lightgray ;# background for less important options -- was TBG
frame $t.top -bg $LIB
pack $t.top -side top -fill both -expand no
frame $t.top.left -bg $TBG
frame $t.top.fourth -bg $TBG
frame $t.top.middle -bg $LIB
frame $t.top.third -bg $LIB
frame $t.top.right -bg $LIB
pack $t.top.left $t.top.fourth -side left -fill both -expand yes
pack $t.top.third -side left -fill both -expand yes
pack $t.top.middle -side left -fill x -expand yes
pack $t.top.right -side left -fill x -expand yes
set p1 $t.top.left
label $p1.saf -text "Safety" -relief raised -bg $TBG -fg $TFG
label $p1.liv -text "Liveness" -relief raised -bg $TBG -fg $TFG
frame $p1.row0 -bg $TBG
radiobutton $p1.row0.sf -variable p_mode -value 0 -text "safety" -bg $TBG -fg $TFG
pack $p1.row0.sf -side left -fill x -expand no
frame $p1.row1 -bg $TBG
label $p1.row1.sp -width 1 -bg $TBG -fg $TFG
checkbutton $p1.row1.av -variable a_mode -text "+ assertion violations" -bg $TBG -fg $TFG
pack $p1.row1.sp $p1.row1.av -side left -fill x -expand no
frame $p1.row9 -bg $TBG
label $p1.row9.sp -width 1 -bg $TBG -fg $TFG
checkbutton $p1.row9.xr -variable x_mode -text "+ xr/xs assertions" -bg $TBG -fg $TFG
pack $p1.row9.sp $p1.row9.xr -side left -fill x -expand no
frame $p1.row2 -bg $TBG
label $p1.row2.sp -width 1 -bg $TBG -fg $TFG
checkbutton $p1.row2.ie -variable e_mode -text "+ invalid endstates (deadlock)" -bg $TBG -fg $TFG
pack $p1.row2.sp $p1.row2.ie -side left -fill x -expand no
pack $p1.saf $p1.row0 $p1.row2 $p1.row1 $p1.row9 -side top -fill x -expand no
frame $p1.row3 -bg $TBG
radiobutton $p1.row3.np -variable p_mode -value 1 -text "non-progress cycles" -bg $TBG -fg $TFG
pack $p1.row3.np -side left -fill x -expand no
frame $p1.row4 -bg $TBG
radiobutton $p1.row4.ac -variable p_mode -value 2 -text "acceptance cycles" -bg $TBG -fg $TFG
pack $p1.row4.ac -side left -fill x -expand no
frame $p1.row5 -bg $TBG
# label $p1.row5.sp -width 1 -bg $TBG -fg $TFG
checkbutton $p1.row5.wf -variable f_mode -text "enforce weak fairness constraint" -bg $TBG -fg $TFG
pack $p1.row5.wf -side left -fill x -expand no
pack $p1.liv $p1.row3 $p1.row4 $p1.row5 -side top -fill x -expand no
set p10 $t.top.fourth
label $p10.alg -text "Storage Mode" -relief raised -bg $TBG -fg $TFG
frame $p10.row0 -bg $TBG
radiobutton $p10.row0.ex -variable s_mode -value 0 -text "exhaustive" -bg $TBG -fg $TFG
pack $p10.row0.ex -side left -fill x -expand no
# frame $p10.row1 -bg $TBG
# radiobutton $p10.row1.bs -variable s_mode -value 1 -text "bitstate" -bg $TBG -fg $TFG
# pack $p10.row1.bs -side left -fill x -expand no
frame $p10.row2 -bg $TBG
radiobutton $p10.row2.hc -variable s_mode -value 2 -text "hash-compact" -bg $TBG -fg $TFG
radiobutton $p10.row2.bs -variable s_mode -value 1 -text "bitstate/supertrace" -bg $TBG -fg $TFG
pack $p10.row2.hc $p10.row2.bs -side left -fill x -expand no
frame $p10.row3 -bg $TBG
label $p10.row3.sp -width 1 -bg $TBG -fg $TFG
checkbutton $p10.row3.ma -variable ma_mode -text "+ minimized automata (slow)" -bg $TBG -fg $TFG
pack $p10.row3.sp $p10.row3.ma -side left -fill x -expand no
frame $p10.row4 -bg $TBG
label $p10.row4.sp -width 1 -bg $TBG -fg $TFG
checkbutton $p10.row4.cl -variable cc_mode -text "+ collapse compression" -bg $TBG -fg $TFG
pack $p10.row4.sp $p10.row4.cl -side left -fill x -expand no
frame $p10.row6 -bg $TBG
button $p10.row6.go -text "Run" \
-command " run_ver $t " \
-fg $NFG -bg $NBG -activeforeground $NBG -activebackground $NFG -font $HV0
button $p10.row6.no -text "Stop" \
-command " stop_ver $t " \
-fg $NFG -bg $NBG -activeforeground $NBG -activebackground $NFG -font $HV0
pack $p10.row6.no $p10.row6.go -side right -fill x -expand yes
pack $p10.alg $p10.row0 $p10.row3 $p10.row4 $p10.row2 \
-side top -fill x -expand no
label $p10.nc -text "Never Claims" -relief raised -bg $TBG -fg $TFG
frame $p10.row9 -bg $TBG
if {$LTL_Panel} {
radiobutton $p10.row9.nc -variable c_mode -value 1 -text "use claim from LTL panel:" -bg $TBG -fg $TFG
pack $p10.row9.nc -side left -fill x -expand no
} else {
radiobutton $p10.row9.nc -variable c_mode -value 1 -text "use claim" -bg $TBG -fg $TFG
pack $p10.row9.nc -side left -fill x -expand no
frame $p10.rowA -bg $TBG
label $p10.rowA.lb -text " claim name (opt):" -bg $TBG -fg $TFG
entry $p10.rowA.nr
pack $p10.rowA.lb -side left -fill x -expand no
pack $p10.rowA.nr -side left -fill x -expand yes
}
# frame $p10.row10 -bg $TBG
# radiobutton $p10.row10.nc -variable c_mode -value 2 \
# -text "use (only) product of claims in spec" -bg $TBG -fg $TFG
# pack $p10.row10.nc -side left -fill x -expand no
frame $p10.row11 -bg $TBG
radiobutton $p10.row11.nc -variable c_mode -value 0 \
-text "do not use a never claim or ltl property" -bg $TBG -fg $TFG
pack $p10.row11.nc -side left -fill x -expand no
pack $p10.nc $p10.row11 $p10.row9 \
-side top -fill x -expand no
if {$LTL_Panel == 0} {
pack $p10.rowA -side top -fill x -expand no
}
set p6 $t.top.middle
frame $p6.row66 -bg $LIB
button $p6.row66.a1 -text "Show\nError\nTrapping\nOptions" \
-command "toggle_a 1" \
-fg white -bg black -activeforeground $NBG \
-activebackground $NFG -font $HV0
pack $p6.row66.a1 -side left -fill x -expand yes
pack $p6.row66 -side top -fill x -expand yes
set p6 $t.top.right
frame $p6.row66 -bg $LIB
button $p6.row66.a3 -text "Show\nAdvanced\nParameter\nSettings" \
-command "toggle_a 3" \
-fg white -bg black -activeforeground $NBG \
-activebackground $NFG -font $HV0
pack $p6.row66.a3 -side left -fill x -expand yes
pack $p6.row66 -side top -fill x -expand yes
pack $p10.row6 -side bottom -fill x -expand no
advanced_2
if {$V_Panel_1} {
advanced_1
}
if {$V_Panel_3} {
advanced_3
}
###
set vw [PanedWindow $t.bottom -side top -activator button ]
set p9 [$vw add -minsize 100]
set p8 [$vw add -minsize 100]
set s11 [ScrolledWindow $p8.vo -size $ScrollBarSize] ;# vo - verification output
set vo [text $s11.lb -height 6 -width 100 -highlightthickness 3 -bg $CBG -fg $CFG -font $HV1]
$s11 setwidget $vo
set s22 [ScrolledWindow $p9.vr -size $ScrollBarSize] ;# vr - verification reference
set vr [text $s22.lb -height 35 -highlightthickness 0 -font $HV1]
$s22 setwidget $vr
pack $s11 -fill both -expand yes
pack $s22 -fill both -expand yes
pack $vw -fill both -expand yes
$vo insert end "verification result:\n"
$vr insert end "model source:\n"
}
proc save_in {v} {
global vo
set f [$v get]
if {$f == ""} {
return
}
add_log "save verification output in $f" 0
if [ catch {set fd [open $f w]} errmsg ] {
add_log $errmsg 0
return
}
puts $fd [$vo get 0.0 end]
catch { close $fd }
}
proc do_clear {} {
global vo
$vo delete 0.0 end
}
proc output_filters {x} {
global TBG TFG
set fl $x.filters
frame $fl -bg $TBG
pack $fl -padx 1 -pady 1 -side left -fill both -expand no
label $fl.lbl -text "Output Filtering (reg. exps.)" -relief raised -bg $TBG -fg $TFG
pack $fl.lbl -side top -fill x -expand no
add_frame $fl.pids "process ids:"
add_frame $fl.qids "queue ids:"
add_frame $fl.vars "var names:"
add_frame $fl.track "tracked variable:"
add_frame $fl.scale "track scaling:"
}
proc find_trail {e} {
set ftypes {
{{Spin Trail File Format} {.trail} }
{{All Files} *}
}
switch -- [set file [tk_getOpenFile -filetypes $ftypes]] "" return
catch { $e delete 0.0 end }
catch { $e insert end $file }
}
proc setup_controls {x} {
global TBG TFG NBG NFG
frame $x.run -bg $TBG
pack $x.run -padx 1 -pady 1 -side left -fill both -expand no
frame $x.run.ctl -bg $TBG
button $x.run.ctl.run -width 12 -text "(Re)Run" \
-command { run_sim } \
-bg $NBG -fg $NFG -activebackground $NFG -activeforeground $NBG
button $x.run.ctl.step -width 12 -text "Step Forward" \
-bg $NBG -fg grey -activebackground $NFG -activeforeground $NBG
button $x.run.ctl.stop -width 12 -text "Stop" \
-command { set stop 1 } \
-bg $NBG -fg $NFG -activebackground $NFG -activeforeground $NBG
button $x.run.ctl.back -width 12 -text "Step Backward" \
-bg $NBG -fg grey -activebackground $NFG -activeforeground $NBG
button $x.run.ctl.reset -width 12 -text "Rewind" \
-bg $NBG -fg grey -activebackground $NFG -activeforeground $NBG
pack $x.run.ctl -side left -fill both -expand no
pack $x.run.ctl.run \
$x.run.ctl.stop \
$x.run.ctl.reset \
$x.run.ctl.step \
$x.run.ctl.back \
-side top -fill y -expand yes
}
proc inspect_ltl {et ns} {
set x [$et get]
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 [$ns 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 {
$ns insert end "$pattern\t?\n"
}
set line [$ns get 0.0 end]
} } }
}
set ltl_cnt 0
proc ltl_log {s} {
global ltl_cnt log_pan
incr ltl_cnt
$log_pan insert end "$ltl_cnt $s\n"
$log_pan yview end
update
}
proc gen_claim {et nc ns} {
global negate_ltl
inspect_ltl $et $ns
set formula [$et get]
if {$negate_ltl == "1"} {
set formula "!($formula)"
}
$nc delete 0.0 end
catch {
set fd [open "|spin -f \"($formula)\"" r]
while {[eof $fd] == 0 && [gets $fd line] > -1} {
$nc insert end $line\n
}
catch "close $fd"
}
}
proc clear_ltl {t} {
global sym_pan nvr_pan note_pan
$t.left.frm.tmp delete 0 end
$t.left.frm.ent delete 0 end
$sym_pan delete 0.0 end
$nvr_pan delete 0.0 end
$note_pan delete 0.0 end
ltl_log "clear"
}
proc help_ltl {} {
ltl_log "\tLTL Help"
ltl_log "\tYou can load an LTL template with a previously saved LTL"
ltl_log "\tformula from a file via the Browse button on the upper"
ltl_log "\tright of the LTL Property Manager panel."
ltl_log ""
ltl_log "\tDefine a new LTL formula using lowercase names for the"
ltl_log "\tpropositional symbols, for instance:"
ltl_log "\t [] (p U q)"
ltl_log "\tThe formula expresses either a positive (desired) or a"
ltl_log "\tnegative (undesired) property of the model. A positive"
ltl_log "\tproperty is negated automatically by the translator to"
ltl_log "\tconvert it in a never claim (which expresses the"
ltl_log "\tcorresponding negative property (the undesired behavior"
ltl_log "\tthat is claimed 'never' to occur)."
ltl_log ""
ltl_log "\tYou can also avoid the use of propositional symbols by"
ltl_log "\tusing embedded expressions in curly braces, e.g., instead"
ltl_log "\tof defining"
ltl_log "\t #define p (nr_leaders > 0)"
ltl_log "\tand using p as a propositional symbol in the LTL formula"
ltl_log "\t <>\[\] p"
ltl_log "\tyou can also use an embedded expression as follows:"
ltl_log "\t <>\[\] {nr_leaders > 0}"
ltl_log ""
ltl_log "\tWhen you type a <Return> or hit the <click to generate> button"
ltl_log "\tat the bottom of the screen, the formula is converted into"
ltl_log "\ta never-claim, which can be imported into a verification on the"
ltl_log "\tVerification Panel (or saved in a template file for later)."
ltl_log ""
ltl_log "\tIf you're using propositional symbols (p, q, etc.) a definition"
ltl_log "\tfor each symbol used must be given in the top window (macros)"
ltl_log "\tThese definitions become part of the LTL template."
ltl_log "\tEnclose the symbol definitions in round braces, for instance:"
ltl_log ""
ltl_log "\t#define p (a > b)"
ltl_log "\t#define q (len(q) < 5)"
ltl_log ""
ltl_log "\tValid temporal logic operators are:"
ltl_log "\t \[\] Always (no space between \[ and \])"
ltl_log "\t <> Eventually (no space between < and >)"
ltl_log "\t U (Strong) Until"
ltl_log "\t V The Dual of Until: (p V q) == !(!p U !q)"
ltl_log "\t"
ltl_log "\t All operators are left-associative."
ltl_log "\t"
ltl_log "\tBoolean Operators:"
ltl_log "\t && Logical And (alternative form: /\\, no spaces)"
ltl_log "\t ! Logical Negation"
ltl_log "\t || Logical Or (alternative form: \\/, no spaces)"
ltl_log "\t -> Logical Implication"
ltl_log "\t <-> Logical Equivalence"
ltl_log ""
ltl_log "\tBoolean Predicates:"
ltl_log "\t true, false"
ltl_log "\t any name that starts with a lowercase letter, or"
ltl_log "\t any state expression enclosed in curly braces {...}"
ltl_log "\t"
ltl_log "\tExamples:"
ltl_log "\t \[\] p"
ltl_log "\t !( <> !q )"
ltl_log "\t p U q"
ltl_log "\t p U (\[\] (q U r))"
ltl_log "\t { a + b == 15 } U { qempty(qin) }"
ltl_log "\t"
ltl_log "\tGeneric types of LTL properties:"
ltl_log "\t Invariance: \[\] p"
ltl_log "\t Response: (p -> \<\> q)"
ltl_log "\t Precedence: (p -> (q U r))"
ltl_log "\t Objective: (p -> \<\> (q || r))"
ltl_log "\t"
ltl_log "\t Each of the above 4 generic types of properties"
ltl_log "\t can (and will generally have to) be prefixed by"
ltl_log "\t temporal operators such as"
ltl_log "\t \[\], \<\>, \[\]\<\>, \<\>\[\]"
ltl_log "\t The last (objective) property can be read to mean"
ltl_log "\t that 'p' is a trigger, or 'enabling' condition that"
ltl_log "\t determines when the requirement becomes applicable"
ltl_log "\t (e.g. the sending of a new data message); then 'q'"
ltl_log "\t can be the fullfillment of the requirement (e.g."
ltl_log "\t the arrival of the matching acknowledgement), and"
ltl_log "\t 'r' could be a discharging condition that voids the"
ltl_log "\t applicability of the check (an abort condition)."
}
proc put_t_name {t file} {
if {[string first "[pwd]/" $file] == 0} {
set prf [string length "[pwd]/"]
set file [string range $file $prf end]
}
$t.left.frm.tmp delete 0 end
$t.left.frm.tmp insert insert "$file"
}
proc dump_contents {s fd w} {
puts $fd "===start $s==="
puts $fd [$w get 0.0 end]
puts $fd "===end $s==="
}
proc hunt_for {s fd} {
while {[gets $fd line] > -1} {
if {[string first "$s" $line] >= 0} {
return "$line"
}
}
add_log "restore: $s not found" 0
return ""
}
proc get_contents {s fd w} {
set found 0
if {[hunt_for "===start $s===" $fd] == ""} {
catch { close $fd }
return 0
}
$w delete 0.0 end
set found 0
while {[gets $fd line] > -1} {
if {[string first "===end $s===" $line] == 0} {
set found 1
break
} else {
$w insert end $line\n
} }
if {$found == 0} {
add_log "restore: end tag $s not found" 0
catch { close $fd }
return 0
}
return 1
}
proc get_field {s fd e} {
set want [hunt_for $s $fd]
if {$want == ""} {
add_log "restore: no field $s" 0
return 0
}
set x [string last "\t" $want]
incr x
$e delete 0 end
$e insert end [string range $want $x end]
}
proc get_var {s fd} {
set want [hunt_for $s $fd]
if {$want == ""} {
add_log "restore: no var $s" 0
return 0
}
set x [string last "\t" $want]
incr x
return [string range $want $x end]
}
proc restore_session {} {
global Fname Sname twin vwin qwin swin clog x
set ftypes {
{{iSpin Session Format} {.isf} }
{{All Files} *}
}
switch -- [set f [tk_getOpenFile -filetypes $ftypes]] "" return
if [catch {set fd [open "$f" r]} errmsg] {
add_log $errmsg 1
return
}
if {[gets $fd line] <= -1} {
add_log "restore_session: empty file" 1
return
}
# Edit/View
set nx [string first "\t" $line]
if {[string first "Fname" $line] != 0 || $nx != 5} {
add_log "$f is not an ispin session file" 1
add_log "first line is: $line at: [string first "Fname" $line] x: $nx" 0
return
}
incr nx
set Fname [string range $line $nx end]
wm title . "$Fname"
if {[get_contents "Model Spec" $fd $twin] == 0} { return }
if {[get_contents "Model Log" $fd $clog] == 0} { return }
# Simulate
global l_typ msc_full var_vals
get_field "Seed" $fd $x.sms.rnd.fld2 ;# random seed value
get_field "Trail" $fd $x.sms.int.fld4 ;# error trail name
get_field "SkipStep" $fd $x.sms.skp.ent ;# steps skipped
get_field "MaxStep" $fd $x.sms.ub.ent ;# max steps
set var_vals [get_var "VarVals" $fd] ;# variable values
set l_typ [get_var "FullQ" $fd] ;# block/loses choice
set msc_full [get_var "MSC_Full" $fd] ;# MSC+stmnt boolean
get_field "MaxText" $fd $x.afq.max.me ;# MSC max text width
get_field "Delay" $fd $x.afq.delay.me ;# MSC update delay
get_field "Pids" $fd $x.filters.pids.ent ;# process ids
get_field "Qids" $fd $x.filters.qids.ent ;# queue ids
get_field "Vars" $fd $x.filters.vars.ent ;# var names
get_field "Track" $fd $x.filters.track.ent ;# tracked var
get_field "Scale" $fd $x.filters.scale.ent ;# track scaling
if {[get_contents "Data" $fd $vwin] == 0} { return }
if {[get_contents "Sim" $fd $swin] == 0} { return }
if {[get_contents "Queues" $fd $qwin] == 0} { return }
# LTL
global nvr_pan note_pan sym_pan ltl_main
global negate_ltl
global LTL_Panel
set LTL_Panel [get_var "LTL_Panel" $fd]
if {$LTL_Panel} {
get_field "Formula" $fd $ltl_main.left.frm.ent
get_field "Template" $fd $ltl_main.left.frm.tmp
set negate_ltl [get_var "All" $fd] ;# all/no executions
if {[get_contents "Symbols" $fd $sym_pan] == 0} { return }
if {[get_contents "Notes" $fd $note_pan] == 0} { return }
if {[get_contents "Claim" $fd $nvr_pan] == 0} { return }
}
# Verification
global p_mode a_mode e_mode x_mode f_mode s_mode q_mode
global cc_mode ma_mode c_mode estop bf_mode po_mode
global bc_mode it_mode u_mode sv_mode peg vranges
global vpanel vo
set a_mode [get_var "a_mode" $fd]
set bc_mode [get_var "bc_mode" $fd]
get_field "bc_bound" $fd $vpanel.top.third.rowB.ent
set bf_mode [get_var "bf_mode" $fd]
set c_mode [get_var "c_mode" $fd]
set cc_mode [get_var "cc_mode" $fd]
set e_mode [get_var "e_mode" $fd]
set estop [get_var "estop" $fd]
set f_mode [get_var "f_mode" $fd]
set it_mode [get_var "it_mode" $fd]
set ma_mode [get_var "ma_mode" $fd]
set p_mode [get_var "p_mode" $fd]
set peg [get_var "peg" $fd]
set po_mode [get_var "po_mode" $fd]
set q_mode [get_var "q_mode" $fd]
set s_mode [get_var "s_mode" $fd]
set sv_mode [get_var "sv_mode" $fd]
set u_mode [get_var "u_mode" $fd]
set vranges [get_var "vranges" $fd]
set x_mode [get_var "x_mode" $fd]
global vpanel vo V_Panel_3
if {$V_Panel_3} {
get_field "vrow0" $fd $vpanel.top.right.row0.ent ;# phys mem
get_field "vrow1" $fd $vpanel.top.right.row1.ent ;# state space size
get_field "vrow2" $fd $vpanel.top.right.row2.ent ;# max depth
get_field "vrow3" $fd $vpanel.top.right.row3.ent ;# nr hashfcts
get_field "vrow4" $fd $vpanel.top.right.row4.ent ;# MA size
get_field "vrow5" $fd $vpanel.top.right.row5.ent ;# extra spin options
get_field "vrow6" $fd $vpanel.top.right.row6.ent ;# extra cc options
get_field "vrow7" $fd $vpanel.top.right.row7.ent ;# extra pan options
}
if {[get_contents "VerOut" $fd $vo] == 0} { return }
# Swarm
global spanel so sr
get_field "srow0" $fd $spanel.top.left.row0.e0 ;# min hashfcts
get_field "srow1" $fd $spanel.top.left.row1.e0 ;# max hashfcts
get_field "srow2" $fd $spanel.top.left.row2.e0 ;# min search depth
get_field "srow3" $fd $spanel.top.left.row3.e0 ;# max search depth
get_field "srow4" $fd $spanel.top.left.row4.e0 ;# nr cpus local
get_field "srow5" $fd $spanel.top.left.row5.e0 ;# nr cpus remote
get_field "srow6" $fd $spanel.top.left.row6.e0 ;# max mem per run
get_field "srow7" $fd $spanel.top.left.row7.e0 ;# max runtime
get_field "srow8" $fd $spanel.top.middle.row8.e1 ;# hash-factor
get_field "srow9" $fd $spanel.top.middle.row9.e1 ;# statevector size in bytes
get_field "srow10" $fd $spanel.top.middle.row10.e1 ;# exploration speed
get_field "srow11" $fd $spanel.top.middle.row11.e1 ;# extra spin args
get_field "srow12" $fd $spanel.top.middle.row12.e1 ;# extra pan args
if {[get_contents "CCopts" $fd $spanel.top.right.row0] == 0} { return }
if {[get_contents "SwSetup" $fd $so] == 0} { return }
if {[get_contents "SwRun" $fd $sr] == 0} { return }
catch { close $fd }
add_log "restored session from file $f" 0
}
proc save_session {n} {
global Fname Sname twin vwin qwin swin clog x
global l_typ msc_full LTL_Panel
set f "$Sname.isf" ;# ispin session file
if {$n == 1} { set f [tk_getSaveFile -defaultextension .isf] }
if {$f == ""} { return }
if {[string first "." $f] < 0} {
set f "$f.isf"
}
if ![file_ok $f] { return }
if [catch {set fd [open $f w]} errmsg] {
add_log $errmsg
return
}
fconfigure $fd -translation lf ;# no cr at end of line
set Sname $f
# Global
# PM save colors/fonts/fontsizes, if modified from default
# Edit/View
# PM save width/height logwindow in Edit panel
# but $twin configure -height etc. doesnt seem to capture current size
# set x [$twin configure -height]
# set n [llength $x]; incr n -1
# puts $fd "Height [lindex $x $n]" ;# data not current
# filename
puts $fd "Fname $Fname"
dump_contents "Model Spec" $fd $twin
dump_contents "Model Log" $fd $clog
# Simulate
# PM width/height of text and msc/data/sim/queues panels
global var_vals
puts $fd "Seed [$x.sms.rnd.fld2 get]" ;# random seed value
puts $fd "Trail [$x.sms.int.fld4 get]" ;# error trail name
puts $fd "SkipStep [$x.sms.skp.ent get]" ;# steps skipped
puts $fd "MaxStep [$x.sms.ub.ent get]" ;# max steps
puts $fd "VarVals $var_vals" ;# variable values
puts $fd "FullQ $l_typ" ;# block/loses choice
puts $fd "MSC_Full $msc_full" ;# MSC+stmnt boolean
puts $fd "MaxText [$x.afq.max.me get]" ;# MSC max text width
puts $fd "Delay [$x.afq.delay.me get]" ;# MSC update delay
puts $fd "Pids [$x.filters.pids.ent get]" ;# process ids
puts $fd "Qids [$x.filters.qids.ent get]" ;# queue ids
puts $fd "Vars [$x.filters.vars.ent get]" ;# var names
puts $fd "Track [$x.filters.track.ent get]" ;# tracked var
puts $fd "Scale [$x.filters.scale.ent get]" ;# track scaling
dump_contents "Data" $fd $vwin
dump_contents "Sim" $fd $swin
dump_contents "Queues" $fd $qwin
# LTL
global nvr_pan note_pan sym_pan ltl_main
global negate_ltl
puts $fd "LTL_Panel $LTL_Panel"
if {$LTL_Panel} {
# PM width/height of symbol/notes/claim/log panels
puts $fd "Formula [$ltl_main.left.frm.ent get]"
puts $fd "Template [$ltl_main.left.frm.tmp get]"
puts $fd "All $negate_ltl" ;# all/no executions
dump_contents "Symbols" $fd $sym_pan
dump_contents "Notes" $fd $note_pan
dump_contents "Claim" $fd $nvr_pan
}
# Verification
# PM width/height of ref and output panels
global p_mode a_mode e_mode x_mode f_mode s_mode q_mode
global cc_mode ma_mode c_mode estop bf_mode po_mode
global bc_mode it_mode u_mode sv_mode peg vranges
global vpanel vo V_Panel_3
puts $fd "a_mode $a_mode"
puts $fd "bc_mode $bc_mode"
puts $fd "bc_bound [$vpanel.top.third.rowB.ent get]"
puts $fd "bf_mode $bf_mode"
puts $fd "c_mode $c_mode"
puts $fd "cc_mode $cc_mode"
puts $fd "e_mode $e_mode"
puts $fd "estop $estop"
puts $fd "f_mode $f_mode"
puts $fd "it_mode $it_mode"
puts $fd "ma_mode $ma_mode"
puts $fd "p_mode $p_mode"
puts $fd "peg $peg"
puts $fd "po_mode $po_mode"
puts $fd "q_mode $q_mode"
puts $fd "s_mode $s_mode"
puts $fd "sv_mode $sv_mode"
puts $fd "u_mode $u_mode"
puts $fd "vranges $vranges"
puts $fd "x_mode $x_mode"
if {$V_Panel_3} {
puts $fd "vrow0 [$vpanel.top.right.row0.ent get]" ;# phys mem
puts $fd "vrow1 [$vpanel.top.right.row1.ent get]" ;# state space size
puts $fd "vrow2 [$vpanel.top.right.row2.ent get]" ;# max depth
puts $fd "vrow3 [$vpanel.top.right.row3.ent get]" ;# nr hashfcts
puts $fd "vrow4 [$vpanel.top.right.row4.ent get]" ;# MA size
puts $fd "vrow5 [$vpanel.top.right.row5.ent get]" ;# extra spin options
puts $fd "vrow6 [$vpanel.top.right.row6.ent get]" ;# extra cc options
puts $fd "vrow7 [$vpanel.top.right.row7.ent get]" ;# extra pan options
}
dump_contents "VerOut" $fd $vo
# Swarm
global spanel so sr
# PM height setup and output panels
puts $fd "srow0 [$spanel.top.left.row0.e0 get]" ;# min hashfcts
puts $fd "srow1 [$spanel.top.left.row1.e0 get]" ;# max hashfcts
puts $fd "srow2 [$spanel.top.left.row2.e0 get]" ;# min search depth
puts $fd "srow3 [$spanel.top.left.row3.e0 get]" ;# max search depth
puts $fd "srow4 [$spanel.top.left.row4.e0 get]" ;# nr cpus local
puts $fd "srow5 [$spanel.top.left.row5.e0 get]" ;# nr cpus remote
puts $fd "srow6 [$spanel.top.left.row6.e0 get]" ;# max mem per run
puts $fd "srow7 [$spanel.top.left.row7.e0 get]" ;# max runtime
puts $fd "srow8 [$spanel.top.middle.row8.e1 get]" ;# hash-factor
puts $fd "srow9 [$spanel.top.middle.row9.e1 get]" ;# statevector size in bytes
puts $fd "srow10 [$spanel.top.middle.row10.e1 get]" ;# exploration speed
puts $fd "srow11 [$spanel.top.middle.row11.e1 get]" ;# extra spin args
puts $fd "srow12 [$spanel.top.middle.row12.e1 get]" ;# extra pan args
dump_contents "CCopts" $fd $spanel.top.right.row0 ;# compilation options
dump_contents "SwSetup" $fd $so ;# contents setup output panel?
dump_contents "SwRun" $fd $sr ;# contents swarm output panel?
catch "close $fd"
add_log "session save in $Sname" 1
}
proc save_spec {n} {
global Fname twin
set f $Fname
if {$n == 1} { set f [tk_getSaveFile] }
if {$f != ""} { writeoutfile $f }
}
proc save_ltl {t} {
global sym_pan note_pan nvr_pan
if {[$t.left.frm.ent get] == ""} {
ltl_log "error: save, no formula specified"
return
}
gen_claim $t.left.frm.ent $nvr_pan $sym_pan ;# needed for negations
switch -- [set file [eval tk_getSaveFile -initialdir { [pwd] } ]] "" {
ltl_log "error: file select failed"
return
}
if ![file_ok $file] {
ltl_log "error: save, '$file' is not writable"
return
}
if [catch {set fd [open $file w]} errmsg] { return }
puts $fd [string trimright [ $sym_pan get 0.0 end] "\n"]
puts $fd [string trimright " /*\n"]
puts $fd [string trimright " * Formula As Typed: [$t.left.frm.ent get]\n"]
puts $fd [string trimright " */\n"]
puts $fd [string trimright [ $nvr_pan get 0.0 end] "\n"]
puts $fd [string trimright "#ifdef NOTES\n"]
puts $fd [string trimright [ $note_pan get 0.0 end] "\n"]
puts $fd [string trimright "#endif\n"]
close $fd
put_t_name $t $file
ltl_log "saved in '[$t.left.frm.tmp get]'"
}
proc load_from {t file} {
global negate_ltl sym_pan nvr_pan note_pan
if [catch {set fd [open $file r]} errmsg] {
ltl_log "error: cannot open '$file'"
return
}
clear_ltl $t
put_t_name $t $file
set inside_claim 0
set inside_notes 0
while {[gets $fd line] > -1} {
if {$inside_claim} {
$nvr_pan insert end $line\n
if {[string first "\}" $line] == 0} {
set inside_claim 0
}
continue
}
if {$inside_notes} {
if {[string first "#endif" $line] == 0} {
set inside_notes 0
continue
}
$note_pan insert end $line\n
continue
}
if {[string first "#define" $line] >= 0} {
$sym_pan insert end $line\n
continue
}
if {[string first "* Formula As Typed: " $line] > 0} {
set sof [string first ":" $line]
incr sof 2
$t.left.frm.ent insert end [string range $line $sof end]
continue
}
if {[string first "never" $line] == 0} {
set inside_claim 1
if {[string first "/* !(" $line] > 0} {
set negate_ltl 1
}
$nvr_pan insert end $line\n
continue
}
if {[string first "#ifdef NOTES" $line] >= 0} {
set inside_notes 1
}
if {[string first "#ifdef RESULT" $line] >= 0} {
set inside_notes 1
$note_pan insert end "==Verification Result===\n"
}
}
catch " close $fd "
ltl_log "load '$file'"
}
proc load_ltl {t} {
set ftypes {
{{Spin LTL template format} {.ltl} }
{{All Files} *}
}
switch -- [set file [tk_getOpenFile -filetypes $ftypes]] "" return
load_from $t $file
}
proc reopen_ltl {t} {
load_from $t [$t.left.frm.tmp get]
}
proc ltl_panel {t} {
global NBG NFG TBG TFG CBG CFG LTLbg HV0 HV1 negate_ltl ltl_main
global sym_pan note_pan nvr_pan log_pan ScrollBarSize Fname
set ltl_main $t
$t configure -background $LTLbg
frame $t.left
pack $t.left -side top -fill both -expand yes
frame $t.left.frm -bg $TBG
label $t.left.frm.lbl -text "LTL Formula:" -bg $TBG -fg $TFG -font $HV1
entry $t.left.frm.ent -width 60 -relief sunken
label $t.left.frm.tnm -text "Template File:" -bg $TBG -fg $TFG
entry $t.left.frm.tmp -width 30 -relief sunken -bg white -fg $TFG
button $t.left.frm.browse -text "browse" -command "load_ltl $t" \
-relief raised -bg $TBG -fg $TFG
$t.left.frm.tmp insert insert "(use save/load)"
set et $t.left.frm.ent
frame $t.left.op -bg $TBG
pack $t.left.op -side top -fill x -expand no
set alw {\[\] }
set eve {\<\> }
pack [label $t.left.op.s0 -text "Valid Operators: " -bg $TBG -fg $TFG -relief flat] -side left
pack [button $t.left.op.always -bg $CBG -fg $CFG -font $HV0 -text " always: \[\] " \
-command "$et insert insert \"$alw \""] -side left
pack [button $t.left.op.event -bg $CBG -fg $CFG -font $HV0 -text " eventually: \<\> " \
-command "$et insert insert \"$eve \""] -side left
pack [button $t.left.op.until -bg $CBG -fg $CFG -font $HV0 -text " strong-until: U " \
-command "$et insert insert \" U \""] -side left
pack [button $t.left.op.impl -bg $CBG -fg $CFG -font $HV0 -text " implication: -> " \
-command "$et insert insert \" -> \""] -side left
pack [button $t.left.op.and -bg $CBG -fg $CFG -font $HV0 -text " and: && " \
-command "$et insert insert \" && \""] -side left
pack [button $t.left.op.or -bg $CBG -fg $CFG -font $HV0 -text " or: || " \
-command "$et insert insert \" || \""] -side left
pack [button $t.left.op.not -bg $CBG -fg $CFG -font $HV0 -text "negation: ! " \
-command "$et insert insert \" ! \""] -side left
button $t.left.op.open -text "ReLoad" -command "reopen_ltl $t" \
-activebackground $NFG -activeforeground $NBG \
-relief raised -bg $NBG -fg $NFG -font $HV0
button $t.left.op.save -text "Save as" -command "save_ltl $t" \
-activebackground $NFG -activeforeground $NBG \
-relief raised -bg $NBG -fg $NFG -font $HV0
button $t.left.op.clear -text "Clear" -command "clear_ltl $t" \
-activebackground $NFG -activeforeground $NBG \
-relief raised -bg $NBG -fg $NFG -font $HV0
button $t.left.op.help -text "Help" -command "help_ltl" \
-activebackground $NFG -activeforeground $NBG \
-relief raised -bg $NBG -fg $NFG -font $HV0
pack $t.left.op.help $t.left.op.clear $t.left.op.save $t.left.op.open \
-side right -fill x -expand no
pack $t.left.frm.lbl $t.left.frm.ent \
-side left -fill x -expand no
pack $t.left.frm.browse $t.left.frm.tmp $t.left.frm.tnm \
-side right -fill x -expand no
pack $t.left.frm -fill x -expand no
frame $t.left.hlds -bg $TBG
label $t.left.hlds.nm -text "Property holds for:" -bg $TBG -fg $TFG
radiobutton $t.left.hlds.yes -text "all executions (expresses desired behavior)" \
-variable negate_ltl -value 0 -bg $TBG -fg $TFG
radiobutton $t.left.hlds.non -text "no executions (expresses error behavior)" \
-variable negate_ltl -value 1 -bg $TBG -fg $TFG
pack $t.left.hlds -side top -fill x -expand no
pack $t.left.hlds.nm $t.left.hlds.yes $t.left.hlds.non \
-side left -fill x -expand no
label $t.left.spacer1 -height 1 -bg $LTLbg
pack $t.left.spacer1 -side top -fill x -expand no
###
set horiz_pw [PanedWindow $t.left.top -side top -activator button ]
set lft [$horiz_pw add] ;# left hand side
set rgt [$horiz_pw add] ;# right hand side
pack $horiz_pw -fill both -expand yes
set ltl_pw [PanedWindow $lft.x -side left -activator button ]
set mp [$ltl_pw add] ;# macros
set np [$ltl_pw add] ;# notes
set cp [$ltl_pw add] ;# claim
set not_pw [PanedWindow $rgt.x -side left -activator button ]
set lp [$not_pw add] ;# log
pack $ltl_pw $not_pw -fill both -expand yes
### Macros
set mp_t [label $mp.t -text "Symbol macro-definitions (all symbols used in formula):" \
-bg $TBG -fg $TFG -font $HV0]
set sw1 [ScrolledWindow $mp.sw1 -size $ScrollBarSize]
set sym_pan [text $sw1.lb -height 4 -font $HV1]
$sw1 setwidget $sym_pan
### Notes
set np_t [label $np.n -text "Notes (informal explanation of property):" \
-bg $TBG -fg $TFG -font $HV0]
set sw3 [ScrolledWindow $np.sw3 -size $ScrollBarSize]
set note_pan [text $sw3.lb -height 4 -font $HV1]
$sw3 setwidget $note_pan
### Claim
set cp_t [button $cp.n -text "Never Claim (click to generate):" \
-bg $TBG -fg $TFG -font $HV0]
set sw5 [ScrolledWindow $cp.sw5 -size $ScrollBarSize]
set nvr_pan [text $sw5.lb -height 4 -font $HV1]
$sw5 setwidget $nvr_pan
$cp.n configure -command "gen_claim $et $nvr_pan $sym_pan"
### Log
set sw7 [ScrolledWindow $lp.sw7 -size $ScrollBarSize]
set log_pan [text $sw7.lb -width 60 -relief sunken -bg $CBG -fg $CFG -font $HV1]
$sw7 setwidget $log_pan
pack $mp_t -fill x -expand no
pack $sw1 -fill both -expand yes
pack $np_t -fill x -expand no
pack $sw3 -fill both -expand yes
pack $cp_t -fill x -expand no
pack $sw5 -fill both -expand yes
pack $sw7 -fill both -expand yes
bind $et <Return> " gen_claim $et $nvr_pan $sym_pan"
ltl_log "ltl log"
}
set scrollxregion 10000
set scrollyregion 40000
proc simulate_panel {t} {
global x CBG CFG HV0 HV1 ScrollBarSize scrollxregion scrollyregion
global s_typ seed skipstep ubstep l_typ var_vals
global TBG TFG NBG NFG XBB Fname msc_max_w msc_delay
global rwin swin cwin vwin qwin msc msc_full
set pws [PanedWindow $t.pw -side left -activator button ]
set p2 [$pws add -minsize 10]
set p1 [$pws add -minsize 10]
set sf1 [ScrolledWindow $p1.sw -size $ScrollBarSize]
set tbot [text $sf1.lb -highlightthickness 0 -bg $CBG -fg $CFG -font $HV1]
$sf1 setwidget $tbot
set ttop [frame $p2.sw ] ;# we create the ref scrolled text window below
set sf2 $ttop
pack $sf1 $sf2 $pws -fill both -expand yes
#### Simulation Mode
set topf [frame $ttop.topf]
pack $topf -pady 2 -side top -fill both -expand yes
frame $topf.left -bg $TBG ;# left side of top frame; there's no right side yet
pack $topf.left -side top -fill both -expand no
set x $topf.left
frame $x.sms -bg $TBG
label $x.sms.fld0 -text "Mode" -relief raised -bg $TBG -fg $TFG
pack $x.sms -padx 1 -pady 1 -side left -fill both -expand no
pack $x.sms.fld0 -side top -fill x -expand no
#### Reference Model for Tracking
set mws [PanedWindow $topf.middle -side top -activator button ]
set q0 [$mws add -minsize 10]
set q1 [$mws add -minsize 10]
# bottom part of top frame: model text for tracking
set ref [ScrolledWindow $q0.middle -size $ScrollBarSize]
set rwin [text $ref.lb -highlightthickness 0 -font $HV1]
$ref setwidget $rwin
pack $ref -side left -fill both -expand yes
$rwin insert end "reference to model source $Fname"
set cref [ScrolledWindow $q1.middle -size $ScrollBarSize]
set msc [canvas $cref.right -relief raised \
-background $XBB -scrollregion "0 0 $scrollxregion $scrollyregion" ]
$cref setwidget $msc
pack $mws -side top -fill both -expand yes
pack $cref -side right -fill both -expand yes
$msc create text 20 10 -text "MSC $msc_full" -fill white
bind $rwin <KeyRelease> {
if {"%K" == "Return"} {
$rwin insert insert "[$rwin index insert] "
$rwin edit modified true
} }
bind $msc <2> "$msc scan mark %x %y"
bind $msc <B2-Motion> "$msc scan dragto %x %y"
#### Random
frame $x.sms.rnd -bg $TBG
radiobutton $x.sms.rnd.fld1 -text "Random, with seed: " \
-variable s_typ -value 0 -bg $TBG -fg $TFG
entry $x.sms.rnd.fld2 -relief sunken -width 12
pack $x.sms.rnd -side top -fill x -expand no
pack $x.sms.rnd.fld1 -side left -fill x -expand no
pack $x.sms.rnd.fld2 -side right -fill x -expand no
$x.sms.rnd.fld2 insert end $seed
### Interactive
frame $x.sms.usr -bg $TBG
radiobutton $x.sms.usr.fld -text "Interactive (for resolution of all nondeterminism)" \
-variable s_typ -value 2 -bg $TBG -fg $TFG
pack $x.sms.usr -side top -fill x -expand no
pack $x.sms.usr.fld -side left -fill x -expand no
#### Guided
frame $x.sms.int -bg $TBG
radiobutton $x.sms.int.fld3 -text "Guided, with trail:" \
-variable s_typ -value 1 -bg $TBG -fg $TFG
entry $x.sms.int.fld4 -relief sunken
button $x.sms.int.fld5 -relief raised -text "browse" \
-command { find_trail $x.sms.int.fld4 } -bg $TBG -fg $TFG
pack $x.sms.int -side top -fill x -expand no
pack $x.sms.int.fld3 -side left -fill x -expand no
pack $x.sms.int.fld4 -side left -fill x -expand no
pack $x.sms.int.fld5 -side left -fill x -expand no
#### Initial Steps
frame $x.sms.skp -bg $TBG
label $x.sms.skp.lbl -text " initial steps skipped:" -bg $TBG -fg $TFG
entry $x.sms.skp.ent -relief sunken -width 12
$x.sms.skp.ent insert end $skipstep
frame $x.sms.ub -bg $TBG
label $x.sms.ub.lbl -text " maximum number of steps:" -bg $TBG -fg $TFG
entry $x.sms.ub.ent -relief sunken -width 12
$x.sms.ub.ent insert end $ubstep
frame $x.sms.vv -bg $TBG
checkbutton $x.sms.vv.xx -variable var_vals \
-text "Track Data Values (this can be slow)" -bg $TBG -fg $TFG
pack $x.sms.skp -side top -fill x -expand no
pack $x.sms.skp.lbl -side left -fill x -expand no
pack $x.sms.skp.ent -side right -fill x -expand no
pack $x.sms.ub -side top -fill x -expand no
pack $x.sms.ub.lbl -side left -fill x -expand no
pack $x.sms.ub.ent -side right -fill x -expand no
pack $x.sms.vv -side top -fill x -expand no
pack $x.sms.vv.xx -side left -fill x -expand no
#### A Full Queue
frame $x.afq -bg $TBG
label $x.afq.fld0 -text "A Full Channel" -relief raised -bg $TBG -fg $TFG
pack $x.afq -padx 1 -pady 1 -side left -fill both -expand no
pack $x.afq.fld0 -side top -fill x -expand no
#### Blocks/Loses
frame $x.afq.int -bg $TBG
frame $x.afq.int.la -bg $TBG
radiobutton $x.afq.int.la.fld3 -text "blocks new messages" -variable l_typ -value 0 -bg $TBG -fg $TFG
radiobutton $x.afq.int.la.fld4 -text "loses new messages" -variable l_typ -value 1 -bg $TBG -fg $TFG
pack $x.afq.int -side top -fill x -expand no
pack $x.afq.int.la -side left -fill x -expand yes
pack $x.afq.int.la.fld3 -side top -fill x -expand no -anchor w
pack $x.afq.int.la.fld4 -side top -fill x -expand no -anchor w
#### MSC
frame $x.afq.ish -bg $TBG
checkbutton $x.afq.ish.is -text "MSC+stmnt" -variable msc_full -bg $TBG -fg $TFG
pack $x.afq.ish.is -side left -fill x -expand no
pack $x.afq.ish -side top -fill x -expand no
frame $x.afq.max -bg $TBG
label $x.afq.max.mx -text "MSC max text width" -bg $TBG -fg $TFG
entry $x.afq.max.me -relief sunken -width 6
pack $x.afq.max.mx $x.afq.max.me -side left -fill x -expand yes
pack $x.afq.max -side top -fill x -expand no
$x.afq.max.me insert end $msc_max_w
frame $x.afq.delay -bg $TBG
label $x.afq.delay.mx -text "MSC update delay" -bg $TBG -fg $TFG
entry $x.afq.delay.me -relief sunken -width 6
pack $x.afq.delay.mx $x.afq.delay.me -side left -fill x -expand yes
pack $x.afq.delay -side top -fill x -expand no
$x.afq.delay.me insert end $msc_delay
#### Output Filters
output_filters $x
#### Controls
setup_controls $x
#### Command executed
frame $x.bgf -bg $TBG
pack $x.bgf -side right -fill both -expand yes
set lwin [label $x.bgf.lbl -text "Background command executed:" -bg $TBG -fg $TFG]
pack $lwin -side top -fill x -expand no
set cwin [text $x.bgf.cmd -height 6 -bg lightgray -fg $TFG -font $HV1]
pack $cwin -side top -fill both -expand yes
button $x.bgf.ps -text "Save in: msc.ps" -font $HV0 \
-fg black -bg ivory -activeforeground $NBG -activebackground $NFG \
-command "$msc postscript -file msc.ps -colormode color"
pack $x.bgf.ps -side right -expand no
### Simulation output
set bwp [PanedWindow $tbot.pw -side top -activator button ]
set p2 [$bwp add -minsize 10]
set p1 [$bwp add -minsize 10]
set p0 [$bwp add -minsize 10]
set lwp [ScrolledWindow $p1.sw -size $ScrollBarSize]
set swin [text $lwp.lb -highlightthickness 0 -bg $CBG -fg $CFG -font $HV1]
$lwp setwidget $swin
pack $lwp $bwp -fill both -expand yes
$swin insert end "Simulation output"
### Data Values
set si3 [ScrolledWindow $p2.sw2 -size $ScrollBarSize]
set vwin [text $si3.lb -width 20 -highlightthickness 0 -bg $CBG -fg $CFG]
$si3 setwidget $vwin
pack $si3 -side right -fill both -expand yes
$vwin insert end "Data Values"
set si4 [ScrolledWindow $p0.sw0 -size $ScrollBarSize]
set qwin [text $si4.qv -width 20 -highlightthickness 0 -bg $CBG -fg $CFG]
$si4 setwidget $qwin
pack $si4 -side top -fill both -expand yes
$qwin insert end "Queues"
}
proc curp { x } {
global Curp rwin vr
if {$Curp == "Sp"} {
update_master $rwin
}
if {$Curp == "Vp"} {
update_master $vr
}
set Curp $x
}
proc create_panels {} {
global Curp NBG NFG MFG MBG version xversion HV0 Fname tcl_platform
global LTL_Panel
frame .menu -bg $MFG
label .menu.title -text "$version :: $xversion" -bg $MFG -fg $MBG ;# reversed menu colors
pack append .menu .menu.title {left frame c expand}
pack append . .menu {top frame w fillx}
set pane .f
set nb [NoteBook $pane -bg $NBG -fg $NFG -font $HV0 \
-activebackground $NFG -activeforeground $NBG -side top]
pack $pane -fill both -expand yes
model_panel [$nb insert end Mp -text " Edit/View " -raisecmd "curp Mp" ]
simulate_panel [$nb insert end Sp -text " Simulate / Replay " -raisecmd "curp Sp; runsim" ]
if {$LTL_Panel} {
ltl_panel [$nb insert end Lp -text " LTL Properties " -raisecmd "curp Lp; runltl" ]
}
verify_panel [$nb insert end Vp -text " Verification " -raisecmd "curp Vp; runveri" ]
swarm_panel [$nb insert end Sw -text " Swarm Run " -raisecmd "curp Sw; runswarm" ]
$nb insert end Hp -text " <Help> " -raisecmd "helper; $pane raise $Curp"
$nb insert end Ss -text " Save Session " -raisecmd "save_session 1; $pane raise $Curp"
$nb insert end Rs -text " Restore Session " -raisecmd "restore_session; $pane raise $Curp"
$nb insert end Qt -text " <Quit> " -raisecmd "cleanup; checked_exit; $pane raise $Curp"
$pane raise Mp ;# default view
}
proc runltl {} { add_log "ltl property" 1 }
proc runswarm {} { add_log "swarm run" 1 }
proc runsim {} {
global rwin s_typ Fname
update_ref $rwin
add_log "simulate/replay" 1
if {[catch { set fd [open "$Fname.trail" r]} errmsg]} {
;# no trail file
} else {
catch { close $fd }
set s_typ 1
}
}
proc runveri {} {
global vr p_mode
update_ref $vr
add_log "verification" 1
if {[has_label "accept" ""]} {
set p_mode 2 ;# liveness
} else {
if {[has_label "progress" ""]} {
set p_mode 1 ;# liveness
} else {
set p_mode 0 ;# safety
} }
}
proc bind_lines {into rf} {
global SFG CFG Fname pane
set cnt 0
scan [$into index end] %d numLines
for {set i 1} {$i <= $numLines} { incr i} {
set line [$into get $i.0 $i.end]
set matched ""
regexp {[A-Za-z0-9_\.]+:[0-9]+} $line matched
if {$matched == ""} { continue }
set fn [string first $matched $line]
set char $fn
set fn $i.$fn
incr char [string length $matched]
set splitx [split $matched ":"]
set fnm [lindex $splitx 0]
set lnr [lindex $splitx 1]
set indend $i
append indend "." $char
$into tag add hilite$cnt $fn $indend
$into tag bind hilite$cnt <ButtonPress-1> "
if {\[string compare \"$fnm\" \$Fname] == 0 || \[readinfile \"$fnm\" \]} {
$rf yview -pickplace $lnr.0
catch { $rf tag delete hilite }
$rf tag add hilite $lnr.0 $lnr.end
$rf tag configure hilite -foreground $SFG
}
"
$into tag bind hilite$cnt <Enter> "
$into tag configure hilite$cnt -foreground $SFG
"
$into tag bind hilite$cnt <Leave> "
$into tag configure hilite$cnt -foreground $CFG
"
incr cnt
}
}
proc queue_update {n} { ;# in separate panel from vars
global QStep Qnm Levels qwin
if { [info exists Levels($n)] == 0 } {
set Levels($n) "-"
}
$qwin delete 0.0 end
$qwin insert end "\[queues, step $Levels($n)\]\n\n"
foreach el [lsort [array names Qnm]] {
catch {
set qc $QStep([list $n $el])
# set ff [string last ":" $qc]
# incr ff
# set cargo [string range $qc $ff end]
set ff [string first "(" $qc]
set cargo [string range $qc $ff end]
$qwin insert end "q $el :: $cargo\n"
} }
}
proc step_forw {} {
global curn maxn
if {$curn >= $maxn} { return }
incr curn
var_update $curn
queue_update $curn
}
proc step_back {} {
global curn maxn
if {$curn <= 1} { return }
incr curn -1
var_update $curn
queue_update $curn
}
proc rewind {} {
global curn x msc
set curn 1
var_update $curn
queue_update $curn
catch {
$x.run.ctl.step configure -fg gold -command step_forw
$x.run.ctl.back configure -fg gold -command step_back
}
$msc yview moveto 0.0
}
set ostep 0
proc var_update {n} {
global VarStep Varnm swin vwin Levels curn maxn LineNo
global MSC_Y msc msc_w msc_h msc_max_x ostep SFG CFG NFG
set curn $n
if { [info exists Levels($n)] == 0 || $Levels($n) == "-" } {
return
# set Levels($n) "0"
}
$vwin delete 0.0 end
$vwin insert end "\[variable values, step $Levels($n)\]\n\n"
foreach el [lsort [array names Varnm]] {
catch { $vwin insert end " $el = $VarStep([list $n $el])\n" }
}
set showln [expr $LineNo($n) - 1]
if {$showln <= 0} {
return
# set showln 0
}
$swin yview -pickplace $showln
# find closest entry in MSC_Y not larger than lookfor
set lookfor $Levels($n)
set putithere 0
foreach el [array names MSC_Y] {
if {$el < $lookfor} {
if {$el > $putithere} {
set putithere $el
} } }
$msc delete wherearewe
if {[info exists MSC_Y($putithere)] == 0} {
set MSC_Y($putithere) 0 ;# really $msc_min_y - $msc_h
}
set ty [expr $MSC_Y($putithere) + $msc_h]
$msc create line \
30 $ty \
[expr $msc_max_x + $msc_w] $ty \
-width 1 -dash {8 2} -fill red -tags wherearewe
# highlight line in text view:
catch { $swin tag configure bound$ostep -foreground $CFG }
$swin tag configure bound$n -foreground $NFG
set ostep $n
}
proc file_view {fnm zzz} {
global Fname SFG rwin
if {$fnm != ""} {
if {[string compare "$fnm" $Fname] == 0 || [readinfile "$fnm" ]} {
$rwin yview -pickplace $zzz.0
catch { $rwin tag delete hilite }
$rwin tag add hilite $zzz.0 $zzz.end
$rwin tag configure hilite -foreground $SFG
$rwin yview -pickplace [expr $zzz - 5]
} }
}
proc put_msc {how sno prno stmnt ss pnm fnm zzz} {
global msc msc_x msc_y msc_w msc_h msc_max_x scrollyregion
global x ProcessLine MSC_Y msc_max_w msc_delay HV0 CBG NFG
global XBG XFG XTX XAR XPR
if {$msc_max_x < $msc_x} {
set msc_max_x $msc_x
}
set msc_max_w [$x.afq.max.me get]
set mw [font measure $HV0 "w"]
set mw [expr $mw * $msc_max_w]
set msc_x [expr ($mw / 2) + $prno * ($msc_w + 10)]
set dx [expr $msc_x + $msc_w / 2 ]
if {[info exists ProcessLine($prno)]} {
$msc create line \
$dx $ProcessLine($prno) \
$dx $msc_y -tags session \
-width 1 -fill $XPR
} else {
$msc create text \
$dx [expr $msc_y - $msc_h / 2] \
-text "$pnm:$prno" -fill $XTX -tags session
}
set ProcessLine($prno) [expr $msc_y + $msc_h]
set MSC_Y($sno) $msc_y
if {$how} {
$msc create rectangle \
$msc_x $msc_y \
[expr $msc_x + $msc_w] [expr $msc_y + $msc_h] \
-outline $XBG -fill $XFG -tags session
set tcol $XTX
} else {
set tcol black
}
set stmnt [string trimleft $stmnt "\["]
set stmnt [string trimright $stmnt "\]"]
if {[string length $stmnt] > $msc_max_w} {
set stmnt [string range $stmnt 0 $msc_max_w]
set stmnt "$stmnt..."
}
set nv [$msc create text \
[expr $msc_x + $msc_w / 2] [expr $msc_y + $msc_h / 2] \
-text "$stmnt" -font $HV0 -fill $tcol -tags session]
$msc bind $nv <ButtonPress-1> "
var_update $ss
queue_update $ss
file_view {$fnm} $zzz
"
$msc create text \
15 [expr $msc_y + $msc_h / 2] \
-text "$sno" -fill $XTX -tags sno ;# sno: step number
catch " $msc yview moveto [expr 1.0 * ($msc_y - 10*$msc_h) / $scrollyregion] "
update
set msc_delay [$x.afq.delay.me get]
if {$msc_delay > 0} {
after $msc_delay
}
}
proc handle_ipc {qno istype} {
global Qfill Qempty Mbox_x Mbox_y XAR
global msc msc_x msc_y msc_w msc_h
## connect send to receive
## just deals with the easy case
## so far, ie not !! or ??
if {[info exists Qfill($qno)] == 0} {
set Qfill($qno) 1
set Qempty($qno) 1
}
if {$istype == 1} { ;# send
set Mbox_x([list $Qfill($qno) $qno]) $msc_x
set Mbox_y([list $Qfill($qno) $qno]) [expr $msc_y + $msc_h / 2]
incr Qfill($qno)
} else { ;# recv
set ox $Mbox_x([list $Qempty($qno) $qno])
set oy $Mbox_y([list $Qempty($qno) $qno])
set tx $msc_x
set ty [expr $msc_y + $msc_h / 2]
if {$oy != 0 && $oy != 0} {
if {$ox < $tx} {
incr ox $msc_w
} else {
incr tx $msc_w
}
## -dash { 4 2 } -width 3
$msc create line $ox $oy $tx $ty -width 1 \
-fill $XAR -arrow last -arrowshape {3 5 3} -tags session
}
incr Qempty($qno)
}
}
proc clearup {} {
global Varnm Qnm ProcessLine cwin vwin
global Qfill Qempty Mbox_x Mbox_y
$cwin delete 0.0 end
$vwin delete 0.0 end
catch {
foreach el [array names ProcessLine] {
unset ProcessLine($el)
} }
catch {
foreach el [array names Varnm] {
unset Varnm($el)
}
foreach el [array names Qnm] {
unset Qnm($el)
} }
catch {
foreach el [array names Qfill] {
unset Qfill($el)
}
foreach el [array names Qempty] {
unset Qempty($el)
} }
catch {
foreach el [array names Mbox_x] {
unset Mbox_x($el)
}
foreach el [array names Mbox_y] {
unset Mbox_y($el)
} }
}
proc lines_touched {} {
global LineTouched Fname rwin NBG
foreach el [array names LineTouched] {
set f [lindex $el 0]
if {$f == $Fname} {
set n [lindex $el 1]
$rwin tag add touched $n.0 $n.end
} }
$rwin tag configure touched -foreground $NBG
}
proc line_bindings {lnr prno sno line} {
global Levels LineNo step swin SFG CFG msc_full
global Fname rwin step msc_h msc_y LineTouched
set LineNo($step) $lnr
catch { $swin tag remove bound$step 0.0 end }
set ft [string first ":" $line] ;# first colon
set nft [expr $ft - 1]
set Levels($step) [string range $line 0 $nft]
set fnm ""
set zzz 0
set matched ""
regexp {[A-Za-z0-9_\.]+:[0-9]+} $line matched
if {$matched != ""} {
set splitx [split $matched ":"]
set fnm [lindex $splitx 0]
set zzz [lindex $splitx 1]
set LineTouched([list $fnm $zzz]) 1
}
$swin tag add bound$step $lnr.0 $lnr.$ft
if {$matched == ""} {
$swin tag bind bound$step <ButtonPress-1> "
var_update $step
queue_update $step
"
} else {
$swin tag bind bound$step <ButtonPress-1> "
var_update $step
queue_update $step
if {\[string compare \"$fnm\" \$Fname] == 0 || \[readinfile \"$fnm\" \]} {
$rwin yview -pickplace $zzz.0
catch { $rwin tag delete hilite }
$rwin tag add hilite $zzz.0 $zzz.end
$rwin tag configure hilite -foreground $SFG
$rwin yview -pickplace [expr $zzz - 5]
}
"
}
$swin tag bind bound$step <Enter> "
$swin tag configure bound$step -foreground $SFG
"
$swin tag bind bound$step <Leave> "
$swin tag configure bound$step -foreground $CFG
"
if {$msc_full} {
set sos [string first "\[" $line]
if {$sos > 0} {
set stmnt [string range $line $sos end]
if {[string first "!" $stmnt] < 0 \
&& [string first "?" $stmnt] < 0} {
set a [string first "(" $line]
set b [string first ")" $line]
if {$a > 0 && $b > 0} {
incr a
incr b -1
set c [string range $line $a $b]
} else {
set c "--"
}
put_msc 0 $sno $prno $stmnt $step $c $fnm $zzz
incr msc_y $msc_h
} } }
}
proc var_track {nm vl ts} {
global msc msc_h msc_y o_y o_v
if {$msc_y > $o_y} {
for {set i $o_y} {$i < $msc_y} {incr i $msc_h} {
$msc create line \
30 $i \
[expr 30 + $o_v * $ts] $i \
-width [expr $msc_h - 5] -fill orange -tags vartrack
} }
set o_y $msc_y
set o_v $vl
$msc create line \
30 $msc_y \
[expr 30 + $vl * $ts] $msc_y \
-width [expr $msc_h - 5] -fill orange -tags vartrack
}
set Choice(0) ""
set PlaceMenu "+150+150"
set howmany 0
proc pickoption {nm} {
global Choice PlaceMenu howmany NBG NFG cwin swin rwin
set howmany 0
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"
set cnt 0
focus .prompt
foreach i [lsort [array names Choice]] {
if {$Choice($i) != 0} {
incr cnt
pack append .prompt \
[button .prompt.b$cnt -text "$i: $Choice($i)" \
-anchor w \
-bg $NBG -fg $NFG \
-command "set howmany $i" ] \
{top expand fillx}
set matched ""
regexp {[A-Za-z0-9_\.]+:[0-9]+} $Choice($i) matched
if {$matched == ""} { continue }
set splitx [split $matched ":"]
set fnm [lindex $splitx 0]
set lnr [lindex $splitx 1]
bind .prompt.b$cnt <Enter> "$rwin yview -pickplace $lnr.0"
} }
pack append .prompt \
[button .prompt.q -text "quit" \
-anchor w -bg $NBG -fg $NFG -command {set howmany "q\n"} ] \
{top expand fillx}
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
$cwin insert end "$howmany "
$swin insert end "Selected: $howmany\n"
return $howmany
}
proc run_sim {} {
global stop x swin rwin vwin cwin stop l_typ s_typ Fname SPIN maxn
global VarStep Varnm step QStep Qnm SFG CFG Levels LineNo var_vals
global msc msc_x msc_y msc_w msc_h msc_max_x msc_full MSC_Y Choice
set stop 0
update
set seed [$x.sms.rnd.fld2 get]
set skipped [$x.sms.skp.ent get]
set upper [$x.sms.ub.ent get]
set pfilter [$x.filters.pids.ent get]
set vfilter [$x.filters.vars.ent get]
set qfilter [$x.filters.qids.ent get]
set tfilter [$x.filters.track.ent get]
set tscale [$x.filters.scale.ent get]
if {$tscale == ""} { set tscale 1 }
set args "-p -s -r -X -v -n$seed"
if {$var_vals} { set args "$args -l -g" }
if {$skipped > 0} { set args "$args -j$skipped" }
if {$l_typ != 0} { set args "$args -m" }
if {$s_typ == 2} { set args "$args -i" }
if {$s_typ == 1} {
set tname [$x.sms.int.fld4 get]
if {$tname == ""} {
$cwin insert end "error: no trailfile specified\n"
return
}
if [catch {set fo [open "$tname" r]} errmsg] {
$cwin insert end "$errmsg\n"
return
}
catch { close $fo }
set args "$args -k $tname"
# set upper 0
}
if {$upper > 0} { set args "$args -u$upper" }
clearup
set args "$args $Fname"
$cwin insert end "spin $args\n"
set fd [open "|$SPIN $args" r+]
catch "flush $fd"
$swin delete 0.0 end
set step 0
set lnr 1
$msc delete session
$msc delete wherearewe
$msc delete sno
$msc delete vartrack
set msc_x 75
set msc_y 20
set msc_max_x $msc_x
set Banner ""
if {$s_typ == 2} {
catch { foreach el [array names Choice] { unset Choice($el) } }
}
while {$stop == 0 && [eof $fd] == 0 && [gets $fd line] > -1} {
if {$line == ""} {
continue
}
if {[string first "type return to proceed" $line] > 0} {
catch { puts $fd ""; flush $fd }
update
continue
}
## interactive mode only:
if {$s_typ == 2} {
if {[string first "Select stmnt" $line] >= 0 \
|| [string first "Select a statement" $line] >= 0} {
set Banner $line
continue
}
if {[string first "choice " $line] >= 0} {
if {[string first " unexecutable" $line] < 0 \
&& [string first " outside range" $line] < 0} {
scan $line " choice %d:" which
set NN [string first ":" $line]
incr NN 2
set what [string range $line $NN end]
set Choice($which) $what
## $swin insert end "=$which=$what== $line\n"
}
continue
}
if {[string first "Make Selection" $line] >= 0} {
set nr [pickoption $Banner]
catch { puts $fd "$nr"; flush $fd }
if {$nr == "q\n"} { set stop 1 }
continue
} }
set i [string first "<merge" $line]
if {$i > 0} {
incr i -1
set line [string range $line 0 $i]
set line [string trimright $line]
}
set ipc [string first "\[values: " $line]
if {$ipc > 0} { ;# send or receive action
incr ipc 9
set epc [string last "\]" $line]
if {$epc > $ipc} {
incr epc -1
set stmnt [string range $line $ipc $epc]
# eg 5!first,7
set snd [string first "!" $stmnt]
if {$snd > 0} {
incr snd -1
set qno [string range $stmnt 0 $snd]
set istype 1 ;# send
} else {
set rcv [string first "?" $stmnt]
incr rcv -1
set qno [string range $stmnt 0 $rcv]
set istype 2 ;# recv
}
if {$qfilter == "" || [regexp $qfilter $qno] > 0} {
if {[scan $line "%d: proc %d (%s)" sno prno pnm] == 3} {
regexp {[A-Za-z0-9_\.]+:[0-9]+} $line matched
if {$matched != ""} {
set splitx [split $matched ":"]
set fnm [lindex $splitx 0]
set zzz [lindex $splitx 1]
}
if {$pfilter == "" || [regexp $pfilter $prno] > 0} {
set pnm [string trimright $pnm ")"]
put_msc 1 $sno $prno $stmnt [expr $step + 1] $pnm $fnm $zzz
catch { handle_ipc $qno $istype }
incr msc_y $msc_h
} } }
}
continue
}
if {[scan $line "%d: proc %d " sno prno] == 2} { ;# process line: transition info
set nstep [expr $step + 1]
foreach el [array names Varnm] {
if [info exists VarStep([list $step $el])] {
set xx $VarStep([list $step $el])
set VarStep([list $nstep $el]) $xx
} }
foreach el [array names Qnm] {
if [info exists QStep([list $step $el])] {
set xx $QStep([list $step $el])
set QStep([list $nstep $el]) $xx
} }
if [info exists LineNo($step)] {
set LineNo($nstep) $LineNo($step)
} else {
set LineNo($nstep) 0
}
incr step
if {$step > $maxn} { set maxn $step }
if {$pfilter == "" || [regexp $pfilter $prno] > 0} {
if {[string first "\[.(goto)\]" $line] > 0 \
|| [string first "goto :" $line] > 0} {
continue
}
$swin insert end "$line\n"
line_bindings $lnr $prno $sno $line
lines_touched ;# update
incr lnr
}
} else { ;# variables, queues, and other info
if {[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 " "]
if {$vfilter == "" || [regexp $vfilter $varnm] > 0} {
set Varnm($varnm) 1
set VarStep([list $step $varnm]) $varvl
var_update $step
if {$tfilter != "" && [regexp $tfilter $varnm] > 0} {
var_track $varnm $varvl $tscale
}
}
} else { ;# not a variable update
;# check for queue contents
set qstart [string first " queue " $line]
if {$qstart > 0} {
incr qstart 7
set ltail [string range $line $qstart end]
set qend [string first " " $ltail]
set qno [string range $ltail 0 $qend]
if {$qfilter == "" || [regexp $qfilter $qno] > 0} {
set Qnm($qno) 1
set QStep([list $step $qno]) $ltail
queue_update $step
}
} else {
# could be never claim move
set nvr [string first ":never:" $line]
if {$nvr > 0} {
incr nvr 8
set envr $nvr
while {[string is integer [string range $line $envr [expr $envr + 1]]]} {
incr envr
}
set clmnt [string range $line $nvr $envr]
set line " (never) [string range $line $nvr end]"
}
$swin insert end "$line\n"; incr lnr
} } }
}
if {$stop == 1} {
while {[eof $fd] == 0 && [gets $fd line] > -1} {
if {[string first "type return to proceed" $line] > 0} {
puts $fd "q"
flush $fd
break
} }
}
catch "close $fd"
catch {
$x.run.ctl.reset configure -fg gold -command rewind
}
bind_lines $swin $rwin
}
proc add_log {s c} {
global clog twin cnt
if {$c} {
$clog insert end "$cnt $s\n"
incr cnt
} else {
$clog insert end "$s\n"
}
bind_lines $clog $twin
$clog yview -pickplace end
}
proc runsyntax {a} {
global twin swin pane
if {[$twin edit modified]} {
set answer [tk_messageBox -icon question -type yesno \
-message "There are unsaved changes. Save first?" ]
switch -- $answer {
yes { save_spec 0; open_spec 0 }
no { }
}
}
if {$a} {
add_log "redundancies" 1
} else {
add_log "syntax check" 1
}
syntax_check $a $swin
}
proc cleanup {} {
global Fname RM
catch { eval exec $RM never_claim.tmp }
catch { eval exec $RM $Fname.nvr spinbat.bat dot.tmp dot.out dot.sel pan.tmp }
catch { eval exec $RM pan.t pan.m pan.h pan.c pan.b pan.p pan.pre }
catch { eval exec $RM run.tmp pan.exe pan }
}
proc syntax_check {a into} {
global clog Fname SPIN Unix
if {$Fname == ""} {
add_log "no model" 0
return
}
set SPINBAT $SPIN ;# default
if {$Unix == 0} { ;# on Windows systems only
if [catch {set fd [open "spinbat.bat" w 0777]} errmsg] {
;# same as default
} else {
set SPINBAT "./spinbat.bat" ;# avoids windows popping up
puts $fd "@spin %1 %2\n"
catch "close $fd"
} }
set cnt 0
if {$a} { set args "-A" } else { set args "-a" }
catch {eval exec $SPINBAT $args $Fname} err
$into delete 0.0 end
if {$err == ""} {
add_log "spin: nothing to report" 0
} else {
add_log "$err" 0
}
update
cleanup
}
proc forAllMatches {w pattern} {
global lno SFG
$w tag remove hilite 0.0 end
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"
$w tag add hilite $i.0 $i.end
$w tag configure hilite -foreground $SFG
} }
# 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"
$w 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"
$w yview -pickplace [expr $i-5]
set lno $i
return
} }
add_log "no match found of \"$pattern\"" 0
}
proc file_ok {f} {
if {[file exists $f]} {
if {![file isfile $f] || ![file writable $f]} {
add_log "error: file $f is not writable" 0
return 0
} }
return 1
}
proc update_master {w} { ;# called for rwin and vr
global twin ;# to make w match twin
$twin delete 0.0 end
scan [$w index end] %d numLines
incr numLines -1
for {set i 1} {$i < $numLines} {incr i} {
set line [$w get $i.0 $i.end]
$twin insert end "$line\n"
}
set line [$w get $i.0 $i.end]
if {$line != ""} {
$twin insert end "$line\n"
}
}
proc update_ref {w} { ;# called for rwin and vr
global twin ;# to make w match twin
$w delete 0.0 end
scan [$twin index end] %d numLines
incr numLines -1
for {set i 1} {$i < $numLines} {incr i} {
set line [$twin get $i.0 $i.end]
$w insert end "$line\n"
}
set line [$w get $i.0 $i.end]
if {$line != ""} {
$twin insert end "$line\n"
}
}
proc writeoutfile {to} {
global Fname twin
if ![file_ok $to] { return 0 }
if [catch {set fd [open $to w]} errmsg] {
add_log $errmsg 0
return 0
}
fconfigure $fd -translation lf ;# no cr at end of line, just lf
scan [$twin index end] %d numLines
for {set i 1} {$i < $numLines} {incr i} {
set line [$twin get $i.0 $i.end]
if {[scan $line "%d " lnr] == 1} {
set sol [string first "\t" $line]
incr sol
puts $fd [string range $line $sol end]
} else {
if {[string length $line] > 0} {
puts $fd $line
} } }
close $fd
set Fname $to
wm title . $Fname
add_log "<saved $Fname>" 1
return 1
}
proc readinfile {from} {
global Fname CBG CFG LTL_Panel
global vr twin rwin ltl_main
if [catch {set fd [open $from r]} errmsg] {
add_log "$errmsg" 0
return 0
}
# $rwin configure -state normal
# $twin configure -state normal
# $vr configure -state normal
$rwin delete 0.0 end
$twin delete 0.0 end
$vr delete 0.0 end
set ln 1
while {[gets $fd line] > -1} {
$rwin insert end "$ln $line\n"
$twin insert end "$ln $line\n"
$vr insert end "$ln $line\n"
incr ln
}
# $rwin configure -state disabled
# $twin configure -state disabled
# $vr configure -state disabled
$twin edit modified false
catch { close $fd }
add_log "$from:1" 1
set prf "[pwd]/"
if {[string first $prf $from] == 0} {
set from [string range $from [string length $prf] end]
}
set Fname $from
wm title . "$Fname"
if {$LTL_Panel} {
$ltl_main.left.frm.tmp delete 0 end
if [catch {set fo [open "$Fname.ltl" r]} errmsg] {
# ltl_log "no ltl-file $Fname.ltl"
} else {
catch { close $fo }
$ltl_main.left.frm.tmp insert insert "$Fname.ltl"
reopen_ltl $ltl_main
} }
return 1
}
proc open_spec {h} {
global Fname x
if {$h == 1} {
set ftypes {
{{Promela File Format} {.pml} }
{{All Files} *}
}
switch -- [set file [tk_getOpenFile -filetypes $ftypes]] "" return
} else {
if {$Fname == ""} { return }
set file $Fname
}
if [readinfile $file] {
set_path $Fname
}
if {$Fname != ""} {
$x.sms.int.fld4 delete 0 end
$x.sms.int.fld4 insert end $Fname.trail
}
}
proc set_path {f} {
global Fname
set fullpath [split $f /]
set nlen [llength $fullpath]
set Fname [lindex $fullpath [expr $nlen - 1]]
wm title . "$Fname"
set fullpath [lrange $fullpath 0 [expr $nlen - 2]] ;# strip filename
set wd [join $fullpath /] ;# put path back together
catch {cd $wd}
}
proc symbol_table {} {
global clog SPIN Fname
if {$Fname == ""} {
add_log "no model" 0
return
}
set ST "$SPIN -d $Fname"
catch {set fd [open "|$ST" r]} errmsg
if {$fd == -1} {
$clog insert end "$errmsg\n"
$clog yview end
update
return
}
$clog insert end "Symbol Table Information for $Fname:\n"
while {[gets $fd line] > -1} {
$clog insert end "$line\n"
$clog yview end
update
}
catch { close $fd }
}
proc helper {} {
global HV0 NBG NFG LTL_Panel
catch {destroy .hlp}
toplevel .hlp -bg black
wm title .hlp "Help with iSpin"
wm iconname .hlp "Help"
wm geometry .hlp 800x450+60+150
set hlp [NoteBook .hlp.x -bg black -fg $NFG -font $HV0 \
-activebackground $NFG -activeforeground $NBG -side top]
pack .hlp.x -fill both -expand yes
g_hlp [$hlp insert end Gh -text " General " ]
n_hlp [$hlp insert end Nh -text " What is New in 6.0 " ]
m_hlp [$hlp insert end Mh -text " Edit/View? " ]
s_hlp [$hlp insert end Sh -text " Simulation/Replay? " ]
if {$LTL_Panel} {
l_hlp [$hlp insert end Lh -text " LTL Properties? " ]
}
v_hlp [$hlp insert end Vh -text " Verification? " ]
sw_hlp [$hlp insert end Swh -text " Swarm? " ]
session_hlp [$hlp insert end Sessionh -text " Save/Restore Session? " ]
q_hlp [$hlp insert end Qh -text " Quit? " ]
$hlp raise Gh
}
proc boilerplate {t} {
global version xversion CBG CFG HV1 ScrollBarSize
set x [ScrolledWindow $t.sw -size $ScrollBarSize]
set y [text $x.lb -height 15 -width 100 -highlightthickness 3 -bg $CBG -fg $CFG -font $HV1]
$x setwidget $y
pack $x -fill both -expand yes
return $y
}
proc n_hlp {t} {
set y [boilerplate $t]
$y insert end "Spin Version 6.0 has a number of new features.
- Improved scope rules:
so far, there were only two levels of scope for variable
declarations: global or proctype local.
6.0 supports the more traditional block scope as well:
a variable declared inside an inline definition or inside
a block has scope that is limited to that inline or block.
You can revert to the old scope rules by using spin -O
- Multiple never claims:
In 6.0 you can name never claims, by adding a name in
between the keyword 'never' and the opening curly brace of
the never claim body.
This allows you to specify multiple never claims in a single
Spin model. The model checker will still only use one never
claim to perform the verification, but you can choose on the
command line of pan which claim you want to use: pan -N name
- Synchronous product of claims:
If multiple never claims are defined, you can use spin to
generate a single claim which encodes the synchronous product
of all never claims defined, using the new option -e:
spin -e spec.pml
- Inline ltl properties:
Instead of specifying an explicit never claim, you can now
specify LTL properties directly inline. Any number of named
properties can be provided, and you can again choose which
one should be checked, using the -N command line argument to pan.
Example LTL property: ltl p1 \{ []<>p \}
Inline LTL properties state positive properties to prove, i.e.,
they are not negated. (When spin generates the corresponding
never claim, it will perform the negation automatically, so that
it can find counter-examples to the positive property.)
- Dot support:
A new option for the executable pan supports the generation of
the state tables in the format accepted by the dot tool from
graphviz: pan -D (the ascii format is still available as pan -d).
- Standardized output:
All filename / linenumber references are now in a single standard
format, given as filename:linenumber, which allows postprocessing
tools, like iSpin, to easily hotlink such references to the source.
"
}
proc version_check {y} {
global CURL
set TMP _version_check_.tmp
set URL http://spinroot.com/spin/Src/index.html
if {[auto_execok $CURL] == ""} {
return
}
catch { eval exec $RM $TMP }
catch { eval exec $CURL -s -S $URL -o $TMP } err
if {$err != ""} {
catch { eval exec $RM $TMP }
return
}
set fd -1
catch { set fd [open $TMP r] }
if {$fd != -1} {
while {[gets $fd line] > -1} {
set want [string first "Current Version" $line]
if {$want >= 0} {
set ln [expr $want + [string length "Current Version "]]
set el [string first ":" $line]
$y insert end "The latest Spin Version is: "
$y insert end "[string range $line $ln [expr $el - 1]] "
$y insert end "(visit http://spinroot.com/spin/Bin)\n"
break
} }
catch { close $fd }
}
catch { eval exec $RM $TMP }
}
proc g_hlp {t} {
global version xversion
set y [boilerplate $t]
$y insert end " $version\n $xversion\n\n"
version_check $y
$y insert end "
Spin is an on-the-fly LTL model checking system for proving properties
of asynchronous software systems, and iSpin is a Graphical User Interface
for Spin written in Tcl/Tk.
Click on one of the above tabs for a more detailed explanation of each
options supported through this interface.
For the latest version of Spin, see:
http://spinroot.com/spin/Bin (precompiled binaries)
or
http://spinroot.com/spin/Src (sources)
For help with Promela, the specification language used by Spin, see:
http://spinroot.com/spin/Man/index.html (overview)
http://spinroot.com/spin/Man/promela.html (manual pages)
For help not covered here and for bug-reports: spin_list \@ spinroot.com
iSpin works only with Spin Version 6.0.0 or later.
Spin is (c) 1989-2003 Bell Laboratories, Lucent Technologies, Murray Hill, NJ, USA,
Extensions 2003-2010 (c) JPL/Caltech. All rights reserved.
Spin and iSpin are for educational and research purposes only. No guarantee
whatsoever is expressed or implied by the distribution of this code.
Last updated: 4 December 2010.
"
}
proc m_hlp {t} {
set y [boilerplate $t]
$y insert end "
This panel allows you to Open or Save a Promela verification models
The default file extension for Promela models is .pml.
Syntax Check, Redundancy Check, and Symbol Table can be used to produce
the corresponding output in the black log window at the bottom of the panel.
Each command issued by iSpin is actually performed by standard Spin
running in the background, so without Spin (or with the wrong version of
Spin pre 6.0) not much of interest can happen.
Find allows you to locate a search string in the Promela model text.
The Automata View button (in the right side mid panel)
populates the blue canvas with the names of proctypes and never claims.
It does so by first generating and compiling the model checking code, so
if there are syntax errors that prevent compilation, you will see those first.
Click on a name to generate the control-flow graph of the corresponding
state machine. Currently, the text in the graphs does not scale when you zoom
in or out, so this is still of some limited use.
You can scroll the display by holding button 2 (middle button) down
and moving the mouse.
"
}
proc s_hlp {t} {
set y [boilerplate $t]
$y insert end "
The Simulation panel has all options that are relevant for random or guided
simulations of the model. A guided similation uses an error-trail produced
in a Verification or Swarm run to guide the execution.
Run button starts a simulation run
Stop stops it
Rewind rewinds a completed run to the start
Step Forward moves one step forward through an earlier run
Step Back moves one step backwards through an earlier run
The background command executed by Spin to generate the output is shown in the box at the top right.
Clicking on a line of text in the Simulation output panel moves to that line
and updates variable values and queue contents values to that point in the execution.
You can also click on the boxes in an MSC display to achieve the same effect.
The entry box for process ids allows you to define a regular expression of pids
that will be used to restrict the output to only processes with matching pids,
for instance you can use 1|3 to display output for only processes 1 and 3
or use \[^1-3\] to suppress output for processes 1, 2, and 3
The entry box for queue ids similarly allows the definition of a regular expression
filter for operations on channels.
The entry box for var names allows you to restrict the output in the Data Values
panel to only variable names matching the regular expression given
The entry box for tracked variable is an experimental option to display a bar in
the MSC panel indicating the size of the variable specified -- the size of the
bar can be scaled with the value given in the track scaling box (e.g., 10 or 0.01).
"
}
proc l_hlp {t} {
set y [boilerplate $t]
$y insert end "
Define an LTL formula in the top box, using the black buttons as
short-hands if needed. Define any necessary symbols as macros in
the Symbols panel, add notes to explain what it is you are trying
to express in the Notes panel and then click the Never Claim bar
(or type return in the Formula entry box) to generate the never claim.
You can save a filled in Properties panel as a template with the Save as button,
and you can (re)load the contents of this panel from an earlier template by
giving a file name in the Template file entry box (top right) and clicking ReLoad.
You can load an LTL template with a previously saved LTL
formula from a file via the Browse button on the upper
right of the LTL Property Manager panel.
See also the Help button on the far right on this panel -- with more detailed guidance.
"
}
proc v_hlp {t} {
set y [boilerplate $t]
$y insert end "
Many options are available here; the purpose of most will be clear from the labels.
A good practice is to go through the options from left to right:
first choosing the type of verification to be done
then what types of error trails you want to see
next the specific type of search to be done (leave it at the default
setting if you can't decide)
next choose a storage mode (again, keep the default if you don't
have a good reason to change it). the options other than exhaustive
are there just to help you reduce memory.
The panel at the far right allows you to provide more detailed parameters.
each of these parameters comes with a short explanation -- press the
'explain' button next to the parameter to check this.
Run generates and compiles the model checker and will execute it (if no errors
prevent the compilation). You can interrupt a long running verification run with the
Stop button.
Use the Help button (on the far right, in the middle) gives more detailed information
on methods to reduce verification complexity.
"
}
proc sw_hlp {t} {
set y [boilerplate $t]
$y insert end "
This panel allows you to configure a Swarm verification run, which can be quite effective
for large models. You specify the maximum runtime and the number of CPU cores
to use (do not exceed the number of cores on your system). To use this option,
you must have the swarm preprocessor installed on your system.
You can download swarm from: http://spinroot.com/swarm
"
}
proc session_hlp {t} {
set y [boilerplate $t]
$y insert end "
Save Session:
Saves the state and contents of *all* panels and selections made,
as well as all textual outputs displayed.
The data is recorded in a session snapshot file with file extension .isf
Restore Session:
Restores the iSpin displays and selections to the a previously saved state."
}
proc q_hlp {t} {
set y [boilerplate $t]
$y insert end "
Performs an orderly exit from iSpin, cleaning up temporary files, etc.
If you forgot to save a modified model, you'll get a warning.
You can of course also just kill the window itself -- but then none of these
niceties will happen.
"
}
proc find_field {fld ln} {
set a [string first "$fld" $ln]
incr a [string length "$fld"]
set b [string first "\"" [string range $ln $a end]]
if {$b <= 0} {
set b [string first "," [string range $ln $a end]]
}
if {$b <= 0} {
set b [string first "\]" [string range $ln $a end]]
}
set b [expr $a + $b - 1]
set mf [string range $ln $a $b]
if {$mf == ""} { set mf 1 }
return [expr 50 * $mf]
}
proc display_graph {pn} {
global fg RM DOT
add_log "select $pn" 1
set found 0
set fd [open dot.tmp r]
set fo [open dot.out w]
while {[gets $fd line] > -1} {
if {[string first "digraph" $line] >= 0} {
if {[string first "$pn" $line] >= 0} {
set found 1
} else {
set found 0
} }
if {$found} {
puts $fo "$line"
} }
catch { close $fd }
catch { close $fo }
# do not overwrite dot.tmp
puts stderr "dbg:\n[exec cat dot.out]"; # MH
catch { eval exec \"$DOT\" -Ttk < dot.out > dot.sel } err
if {$err != ""} {
add_log "$err" 0
tk_messageBox -icon info -message "pan: $err"
return
}
catch { $fg delete graph }
set c $fg
set fd [open dot.sel r]
while {[gets $fd line] > -1} {
if {[string first "#" $line] < 0} {
if {[string first "create polygon" $line] > 0} {
set line [string map {black red} $line]
set line [string map {white black} $line]
}
if {[string first "create oval" $line] > 0} {
set line [string map {black ivory} $line] ;# outline black -> ivory
set line [string map {white black} $line] ;# fill white -> black
}
if {[string first "create line" $line] > 0} {
set line [string map {black ivory} $line]
}
if {[string first "create text" $line] > 0} {
set line [string map {black gold} $line]
}
eval $line -tags graph
# MH: tu jest blad, nie ma .c, jak sie powinien nazywac wgt canvas ???
} }
catch { close $fd }
catch { eval $RM dot.sel dot.out } ;# cannot delete dot.tmp yet
}
proc mk_graphs {} {
global fg Fname SPIN CC DOT HV1 RM
if {$Fname == ""} { return }
if {[auto_execok $DOT] == ""} {
tk_messageBox -icon info -message "ispin: cannot find $DOT"
return
}
add_log "$SPIN -o3 -a $Fname" 1
catch { eval exec $SPIN -o3 -a $Fname } err
if {$err != ""} {
if {[string first "Error:" $err] > 0} {
tk_messageBox -icon info -message "spin: $err"
return
}
add_log "$err" 0
}
add_log "$CC -o pan pan.c" 1
catch { eval exec $CC -w -o pan pan.c } err
if {$err != ""} {
add_log "$err" 0
tk_messageBox -icon info -message "cc: $err"
return
}
# use output from ./pan -D to build menu
add_log "./pan -D > dot.tmp" 1
catch { eval exec ./pan -D > dot.tmp } err
if {$err != ""} {
add_log "$err" 0
tk_messageBox -icon info -message "pan: $err"
return
}
set dx 50
set dy 20
catch { $fg delete hotlinks }
catch { $fg delete graph }
set hl [$fg create text $dx $dy -text "Select:" \
-font $HV1 -fill white -tags hotlinks]
incr dy 15
set fd [open dot.tmp r]
while {[gets $fd line] > -1} {
if {[string first "digraph" $line] >= 0} {
set x [string first "\{" $line]
set pn [string trim [string range $line 8 [expr $x - 1]]]
set hl [$fg create text $dx $dy \
-text $pn -font $HV1 -fill lightblue -tags hotlinks]
incr dy 15
$fg bind $hl <Any-Enter> "
$fg itemconfigure $hl -fill gold
"
$fg bind $hl <Any-Leave> "
$fg itemconfigure $hl -fill lightblue
"
$fg bind $hl <ButtonPress-1> "
display_graph $pn
"
} }
catch { close $fd }
}
#### Startup
create_panels
add_log "$version" 0
add_log "$xversion" 0
add_log "TclTk Version [info tclversion]/$tk_version" 0
if {$argc == 1} {
set Fname "$argv"
open_spec 0
}
update