# ***************************************************************************
# * FC2 PACKAGE SOURCE FILE
# * 
# * xeve-win.tcl -- Tcl Procedures File for window management
# ***************************************************************************

# ***************************************************************************
# * Windows Creation/Destruction Procedures
# ***************************************************************************
# procedure to show window .
proc ShowMainPanel {args} {
    global blifName
    global env

    # Window manager configurations
    wm positionfrom . user
    wm sizefrom . user
    wm geometry . 400x320
    wm grid . 25 20 7 13
    wm maxsize . [expr [winfo screenwidth .]/7] \
        [expr [winfo screenheight .]/13]
    wm minsize . 25 20
    wm title . {XEVE: Esterel Verification Environment}

    # Application Menu
    # ----------------
    # build widget .menu
    frame .menu -borderwidth {2} -relief raised

    checkbutton .menu.beginners -text {Beginner's Mode} \
        -variable {blifName(Beginner)} \
        -command {OnLineInfo ""}

    # build widget .menu.files
    menubutton .menu.files -menu {.menu.files.m} -text {Files} -underline {0}

    # build widget .menu.files.m
    menu .menu.files.m -tearoff 0
    .menu.files.m add command -command {LoadBlifFromBrowser 1} \
            -label {Open FSM (blif  format)} -underline {10}
    .menu.files.m add command -command {LoadBddfFromBrowser} \
            -label {Open FSM (bddf format)} -underline {10}
    .menu.files.m add separator
    .menu.files.m add command -command {SaveFsmInBddf} \
        -label {Save FSM (bddf format)} -underline {0}

    .menu.files.m add separator
    .menu.files.m add command -command {Quit} -label {Quit} -underline {0}

    # build widget .menu.signals
    # menubutton .menu.signals -menu {.menu.signals.m} \
        # -text {Signals} -underline {0}

    # build widget .menu.signals.m
    # menu .menu.signals.m -tearoff 0

    # .menu.signals.m add checkbutton \
        # -variable blifName(Signals:ActionOutputs) \
        # -label {See Action Outputs} -underline {4} \
        # -command {SeeOrHideActionOutputs}

    # .menu.signals.m add checkbutton \
        # -variable blifName(Signals:TestInputs) \
        # -label {See Test Inputs} -underline {9} \
        # -command {SeeOrHideTestInputs}

    # .menu.signals.m add checkbutton \
        # -variable blifName(Signals:TestOutputs) \
        # -label {See Test Outputs} -underline {9} \
        # -command {SeeOrHideTestOutputs}

    # build widget .menu.verification
    menubutton .menu.verification -menu {.menu.verification.m} \
            -text {Verification} -underline {0}

    # build widget .menu.verification.m
    menu .menu.verification.m -tearoff 0
    .menu.verification.m add radiobutton -command {SetVerificationSelection} \
            -variable blifName(verification) -value checkoutput \
            -label {Check outputs} -underline {0}
    .menu.verification.m add radiobutton -command {SetVerificationSelection} \
            -variable blifName(verification) -value reduce -label {Reduce} \
            -underline {0}
    .menu.verification.m add command -command {Verify} -label {Apply} \
            -underline {0}
    .menu.verification.m add separator
    .menu.verification.m add command -label {Compute Reachable States} \
            -command {ReachableStates} \
            -underline {0}

    if {[info exists blifName(UnderDevelopment)] && 
        $blifName(UnderDevelopment) == 1} {
        .menu.verification.m add separator
        .menu.verification.m add command -command {ShowAdvancedWindow} \
            -label {Advanced Verification} -underline {0}
    }

#     .menu.verification.m add separator
#     .menu.verification.m add checkbutton -label {Data-Path Signals} \
#       -variable blifName(DataPathSignals) \
#       -underline {0} \
#       -command {SeeOrHideDataPathSignals}

    # build widget .menu.options
    menubutton .menu.options -menu {.menu.options.m} -text {Options} \
            -underline {0}

    # build widget .menu.help.m
    menu .menu.options.m -tearoff 0
    .menu.options.m add checkbutton -label {FSM stats window} \
            -underline {0} -variable blifName(FsmStats) \
            -command ShowFsmStats
    .menu.options.m add checkbutton -label {Trace reachable states} \
            -underline {0} -variable blifName(ReachableTrace) \
            -command ShowConsole
    .menu.options.m add checkbutton -variable {cb_tools(balloon_help)} \
            -label {Balloon Help} -underline {0}

    if {[info exists blifName(UnderDevelopment)] && 
        $blifName(UnderDevelopment) == 1} {
        .menu.options.m add separator
        .menu.options.m add checkbutton -variable blifName(XeveShell) \
            -label {Shell} -underline {1} -command ShowXeveShell
    }

    # build widget .menu.help
    menubutton .menu.help -menu {.menu.help.m} -text {?} -underline {0}

    # build widget .menu.help.m
    menu .menu.help.m -tearoff 0
    .menu.help.m add command -command {HelpWindow} -label {Xeve Help} \
            -underline {0}
    .menu.help.m add separator
    .menu.help.m add command -command {AboutXeve} -label {About Xeve} \
            -underline {0}

    # pack widget .menu
    pack .menu.files -side left
    # pack .menu.signals -side left
    pack .menu.verification -side left
    pack .menu.options -side left
    pack .menu.help -side left
    pack .menu.beginners -side right -fill y

    # File Selection Area
    # -------------------
    label .label1 -text "File Selection" -anchor sw

    # build widget .frame
    frame .frame -borderwidth {2} -relief groove

    frame .frame.dir
    label .frame.dir.labeldir -text {Working Directory:}
    label .frame.dir.pwd -textvariable blifName(CurrentDirectory) \
            -text $blifName(CurrentDirectory) -anchor w

    pack .frame.dir.labeldir -side left -ipady 0.5m
    pack .frame.dir.pwd -side right -expand 1 -fill x -ipady 2m 

    frame .frame.files

    label .frame.files.relation -text {Relation File}
    label .frame.files.fsm -text {FSM File}

    # build widget .frame.files.frame1
    frame .frame.files.frame1

    # build widget .frame.files.frame1.scrollbar1
    scrollbar .frame.files.frame1.scrollbar1 -highlightthickness 0 \
            -command {.frame.files.frame1.entry2 xview} -orient {horizontal} \
            -width 11 -relief {sunken}

    # build widget .frame.files.frame1.entry2
    entry .frame.files.frame1.entry2 -background {#ffffff} -relief {sunken} \
            -xscrollcommand {.frame.files.frame1.scrollbar1 set}

    catch { .frame.files.frame1.entry2 configure \
            -font lucidasans-bolditalic-12 }

    # bindings for entry .frame.files.frame1.entry2
    bind .frame.files.frame1.entry2 <Key-Return> {LoadBlifFromSelection}

    # pack widget .frame.files.frame1
    pack .frame.files.frame1.entry2 -side top -expand 1 -fill both
    pack .frame.files.frame1.scrollbar1 -side top -fill x

    # build widget .frame.files.frame2
    frame .frame.files.frame2

    # build widget .frame.files.frame2.scrollbar1
    scrollbar .frame.files.frame2.scrollbar1 \
            -command {.frame.files.frame2.entry2 xview} \
            -orient {horizontal} -width 11 -highlightthickness 0 \
            -relief {sunken}

    # build widget .frame.files.frame2.entry2
    entry .frame.files.frame2.entry2 -background {#ffffff} -relief {sunken} \
            -xscrollcommand {.frame.files.frame2.scrollbar1 set}

    catch { .frame.files.frame2.entry2 configure \
            -font lucidasans-bolditalic-12 }
    
    # bindings for entry .frame.files.frame2.entry2
    bind .frame.files.frame2.entry2 <Key-Return> {LoadBlifFromSelection}
    
    # pack widget .frame.files.frame2
    pack .frame.files.frame2.entry2 -side top -expand 1 -fill both
    pack .frame.files.frame2.scrollbar1 -side top -fill x

    # pack widget .frame.files
    pack .frame.files.fsm -side left -ipady 0.5m
    pack .frame.files.frame1 -side left -expand 1 -fill x -padx 1m
    pack .frame.files.relation -side left -ipady 0.5m
    pack .frame.files.frame2 -side left -expand 1 -fill x -padx 1m

    # pack widget .frame
    pack .frame.dir -expand 1 -fill both
    pack .frame.files -expand 1 -fill both

    # Verification Selection Area
    # ---------------------------
    label .verifSelectLabel -text "Verification Selection" -anchor sw

    # build widget .frame
    frame .verif -borderwidth {2} -relief groove

    frame .verif.select
    radiobutton .verif.select.reduce -text "REDUCE" \
            -variable blifName(verification) \
            -value reduce -command "SetVerificationSelection" \
            -relief flat

    radiobutton .verif.select.checkoutput -text "CHECK OUTPUTS" \
            -variable blifName(verification) \
            -value checkoutput -command "SetVerificationSelection" \
            -relief flat

    pack .verif.select.checkoutput -ipadx 1m -expand 1 -anchor w
    pack .verif.select.reduce -ipadx 1m -expand 1 -anchor w

    button .verif.apply -text "Apply" -command Verify


    pack .verif.select -side left -expand 1
    pack .verif.apply -side left -ipadx 1m -ipady 1m -expand 1

    # Signal Selection Area
    # ---------------------
    label .signalSelectLabel -text "Signal Selection" -anchor sw

    # build widget .frame3
    frame .frame3 -borderwidth {2} ; # -relief groove

    # build widget .frame3.frame4
    frame .frame3.frame4 -borderwidth {2} -relief groove

    # build widget .frame3.frame4.frame
    frame .frame3.frame4.frame

    # build widget .frame3.frame4.frame.scrollbar2
    scrollbar .frame3.frame4.frame.scrollbar2 -highlightthickness 0 \
            -command {.frame3.frame4.frame.text0 yview} -relief {sunken}

    # build widget .frame3.frame4.frame.text0
    text .frame3.frame4.frame.text0 -borderwidth {2} -cursor {top_left_arrow} \
                -background #ffffff -foreground {#000000} -height {15} \
                -relief {groove} -width {25} -wrap {none} -state disabled \
                -yscrollcommand {.frame3.frame4.frame.scrollbar2 set} \
                -exportselection 0 -selectborderwidth 0 \
                -selectbackground {#ffffff} -selectforeground {#000000} \
                -highlightthickness 0

    catch {
        .frame3.frame4.frame.text0 configure \
            -font -adobe-helvetica-bold-r-normal--12-120-75-75-p-70-iso8859-1
    }

    # pack widget .frame3.frame4.frame
    pack .frame3.frame4.frame.scrollbar2 -side right -fill y
    pack .frame3.frame4.frame.text0 -side bottom -expand 1 -fill both

    # build widget .frame3.frame4.frame8
    frame .frame3.frame4.frame8 -borderwidth {2} -relief {flat}

    # build widget .frame3.frame4.frame8.label13
    label .frame3.frame4.frame8.label13 -text {INPUTS}

    # pack widget .frame3.frame4.frame8
    pack .frame3.frame4.frame8.label13 -side left -expand 1 -fill x

    # build widget .frame3.frame4.frame1
    frame .frame3.frame4.frame1 -borderwidth {2}

    # build and pack widget .frame3.frame4.frame1.select
    set image [image create bitmap -file "$env(XEVE_LIB)/select.xbm"]
    button .frame3.frame4.frame1.select \
                    -image $image \
                    -relief flat \
                    -command { SignalSelectMode input}

    # build and pack widget .frame3.frame4.frame1.brush
    set image [image create bitmap -file "$env(XEVE_LIB)/palette32.xbm"]
    button .frame3.frame4.frame1.brush \
        -image $image \
        -relief flat \
        -command {SignalPaintMode input}

    pack .frame3.frame4.frame1.select -side left
    pack .frame3.frame4.frame1.brush -side left

    pack [MakeSignalPalette .frame3.frame4.frame1 \
            input $blifName(verification)] -side right \
                    -expand 1 -anchor e \
                    -padx 5m

    # pack widget .frame3.frame4
    pack .frame3.frame4.frame8 -side top -fill x
    pack .frame3.frame4.frame -side top -expand 1 -fill both
    pack .frame3.frame4.frame1 -side top -fill x

    # build widget .frame3.frame5
    frame .frame3.frame5 -borderwidth {2} -relief groove

    # build widget .frame3.frame5.frame
    frame .frame3.frame5.frame

    # build widget .frame3.frame5.frame.scrollbar2
    scrollbar .frame3.frame5.frame.scrollbar2 -highlightthickness 0 \
            -command {.frame3.frame5.frame.text0 yview} -relief {sunken}

    # build widget .frame3.frame5.frame.text0
    text .frame3.frame5.frame.text0 -borderwidth {2} -background #ffffff \
            -foreground {#000000} -cursor {top_left_arrow} \
                             -height {15} -relief {groove} \
            -width {25} -wrap {none} -state disabled \
            -yscrollcommand {.frame3.frame5.frame.scrollbar2 set} \
            -exportselection 0 -selectborderwidth 0 \
            -selectbackground {#ffffff} -selectforeground {#000000} \
            -highlightthickness 0

    catch {
        .frame3.frame5.frame.text0 configure \
            -font -adobe-helvetica-bold-r-normal--12-120-75-75-p-70-iso8859-1
    }

    # pack widget .frame3.frame5.frame
    pack .frame3.frame5.frame.scrollbar2 -side right -fill y
    pack .frame3.frame5.frame.text0 -side bottom -expand 1 -fill both

    # build widget .frame3.frame5.frame8
    frame .frame3.frame5.frame8 -borderwidth {2} -relief {flat}

    # build widget .frame3.frame5.frame8.label15
    label .frame3.frame5.frame8.label15 -text {OUTPUTS}

    # pack widget .frame3.frame5.frame8
    pack .frame3.frame5.frame8.label15 -side left -expand 1 -fill x

    # build widget .frame3.frame5.frame1
    frame .frame3.frame5.frame1 -borderwidth {2}

    # build and pack widget .frame3.frame5.frame1.select
    set image [image create bitmap -file "$env(XEVE_LIB)/select.xbm"]
    button .frame3.frame5.frame1.select \
                -image $image \
                -relief flat \
                -command { SignalSelectMode output}

    # build and pack widget .frame3.frame5.frame1.brush
    set image [image create bitmap -file "$env(XEVE_LIB)/palette32.xbm"]
    button .frame3.frame5.frame1.brush -image $image \
        -relief flat \
        -command {SignalPaintMode output}

    pack .frame3.frame5.frame1.select -side left
    pack .frame3.frame5.frame1.brush -side left

    pack [MakeSignalPalette .frame3.frame5.frame1 \
            output $blifName(verification)] -side right \
                -expand 1 -anchor e \
                -padx 5m

    # pack widget .frame3.frame5
    pack .frame3.frame5.frame8 -side top -fill x
    pack .frame3.frame5.frame -side top -expand 1 -fill both
    pack .frame3.frame5.frame1 -side top -fill x

    # pack widget .frame3
    pack .frame3.frame4 -side left -expand 1 -fill both
    pack .frame3.frame5 -side left -expand 1 -fill both

    # pack widget .
    pack .frame3 -side bottom -expand 1 -padx 2m -pady 2m -ipady 2m -fill both
    pack .signalSelectLabel  -side bottom -fill x -padx 2m -ipady 1m
    pack .menu -side top -fill x
    pack .label1 -side top -fill x -padx 2m -ipady 1m
    pack .frame -side top -fill both -padx 2m -ipadx 1m -ipady 2m
    pack .verifSelectLabel  -side top -fill x -padx 2m -ipady 1m
    pack .verif -side top -fill both -padx 2m -ipadx 1m -ipady 2m -pady 1m

    .frame.files.frame1.entry2 insert end {}
    .frame3.frame4.frame.text0 insert end {}
    .frame3.frame5.frame.text0 insert end {}
}

# Procedure to show window ShowAdvancedWindow
proc ShowAdvancedWindow { } {
    global symbolicName
    global resultName

    set w .advanced
    if {[ShowResultPanel $w]} {
        if {[info exists resultName(ReachableStates)] == 1} {
            $w$symbolicName(ReachableStates) configure \
                    -text $resultName(ReachableStates)
        }
        return
    }

    toplevel $w
    wm withdraw $w
    wm group $w .
    update

    wm title $w "Advanced Verification"
    wm geometry $w 510x455
    wm minsize $w 510 455
    wm maxsize $w 600 700

    BuildKernelPanel $w

    $w$symbolicName(Dismiss) configure -state normal
    $w$symbolicName(AbortButton) configure -state disabled

    label $w.label0 -text "Behavior Status" -anchor sw

    frame $w.frame0 -borderwidth 2 -relief groove
    frame $w.frame0.frame0 -borderwidth 2 -relief flat
    frame $w.frame0.frame1 -borderwidth 2 -relief flat

    label $w.frame0.frame0.label0 -text "Program execution"

    set symbolicName(AdvancedOptionModality) $w.frame0.frame0.mod
    set symbolicName(AdvancedOptionProperty) $w.frame0.frame0.pro

    set symbolicName(AdvancedOptionModalityMenu) \
            [tk_optionMenu $w.frame0.frame0.mod optionModality \
            "Can" "Must"]

    set symbolicName(AdvancedOptionPropertyMenu) \
            [tk_optionMenu $w.frame0.frame0.pro optionProperty \
            "Terminate" "Idle Forever"]

    for {set i 0} {$i < 4} {incr i} {
        set mod [$symbolicName(AdvancedOptionModalityMenu) entrycget $i -label]
        $symbolicName(AdvancedOptionModalityMenu) entryconfigure $i \
                -command "ShowAdvancedCheckResult Modality \"$mod\""
    }
    for {set i 0} {$i < 2} {incr i} {
        set pro [$symbolicName(AdvancedOptionPropertyMenu) entrycget $i -label]
        $symbolicName(AdvancedOptionPropertyMenu) entryconfigure $i \
                -command "ShowAdvancedCheckResult Property \"$pro\""
    }
        
    set symbolicName(AdvancedCheckButton) \
            [button $w.frame0.frame0.button0 -text "Check" \
            -command {AdvancedCheck}]

    pack $w.frame0.frame0.label0 -side left
    pack $w.frame0.frame0.mod -side left
    pack $w.frame0.frame0.pro -side left
    pack $w.frame0.frame0.button0 -side right

    label $w.frame0.frame1.label0 -text "Result:"
    set symbolicName(AdvancedCheckResult) \
            [label $w.frame0.frame1.label1 -text " " -background #ffffff \
            -relief sunken -width 10]
    button $w.frame0.frame1.button0 -text "Save Path" -state disabled
    pack $w.frame0.frame1.label0 -side left
    pack $w.frame0.frame1.label1 -side left
    pack $w.frame0.frame1.button0 -side right

    pack $w.frame0.frame0 -side top -fill x -anchor n
    pack $w.frame0.frame1 -side bottom -fill x -anchor s

    pack $w.label0 -side top -fill x -padx 3m -ipady 3m
    pack $w.frame0 -side top -fill x -padx 3m -ipady 5m

    # SetAdvancedCheckButton
    if {[info exists resultName(ReachableStates)] == 1} {
        $w$symbolicName(ReachableStates) configure \
                -text $resultName(ReachableStates)
    }

    wm deiconify $w
    update
}

proc ShowScale {message} {
    global blifName

    set w .topscale

    catch {destroy $w}

    if {$message == ""} {
        set message "Current operation"
    }

    set blifName(currentScaleValue) "0\%"
    set blifName(scaleFrom) 0
    set blifName(scaleTo) 100

    toplevel $w -class Information
    wm withdraw $w
    wm protocol $w WM_DELETE_WINDOW { }

    wm title $w "Information"

    frame $w.frame -relief flat -width 100m
    frame $w.frame.dummy -relief flat -width 100m 

    label $w.frame.text -relief flat -text $message

    frame $w.frame.scale -relief sunken -width 200m \
        -borderwidth 2 -height 5m
    frame $w.frame.value -relief flat
    frame $w.frame.interval -relief flat

    label $w.frame.value.label -textvariable blifName(currentScaleValue)

    label $w.frame.interval.left -relief flat -text $blifName(scaleFrom)
    label $w.frame.interval.right -relief flat -text $blifName(scaleTo)

    frame $w.frame.scale.slider -relief flat \
        -width $blifName(scaleFrom)m -bg #0000ff -height 5m

    pack $w.frame.scale.slider -side left

    pack $w.frame.interval.left -side left
    pack $w.frame.interval.right -side right

    pack $w.frame.value.label

    pack $w.frame.dummy -fill x -expand 1
    pack $w.frame.text -fill x
    pack $w.frame.value -fill x
    pack $w.frame.scale -fill x 
    pack $w.frame.interval -fill x -expand 1

    pack $w.frame -expand 1

    wm withdraw $w
    update idletasks
    set x [expr {[winfo screenwidth $w]/2 - [winfo reqwidth $w]/2 \
            - [winfo vrootx [winfo parent $w]]}]
    set y [expr {[winfo screenheight $w]/2 - [winfo reqheight $w]/2 \
            - [winfo vrooty [winfo parent $w]]}]
    wm geom $w +$x+$y
    wm resizable $w 0 0
    wm deiconify $w

    update
}

proc DestroyScale {} {
    global symbolicName

    catch "destroy $symbolicName(Scale)"
}

proc SetScaleSlider {scaleValue} {
    global symbolicName
    global blifName

    if {[winfo exists $symbolicName(Scale)] != 0} {
        set blifName(currentScaleValue) "${scaleValue}\%"
        $symbolicName(Scale:Slider) configure -width "${scaleValue}m"

        update
    }
}

proc ShowTextualScale {message} {
    global blifName

    set w .topscale
    catch {destroy $w}

    if {$message == ""} {
        set message "Current operation"
    }

    set blifName(currentScaleValue) "1 refinement step"

    toplevel $w -class Information
    wm withdraw $w
    wm protocol $w WM_DELETE_WINDOW { }

    wm title $w "Information"

    frame $w.dummy -width 100m -relief flat
    label $w.text -relief flat -text $message

    label $w.label -textvariable blifName(currentScaleValue) \
        -fg #0000ff

    pack $w.dummy -fill x -expand 1
    pack $w.text -expand 1 -fill x -anchor e
    pack $w.label -expand 1 -fill x -anchor e

    wm withdraw $w
    update idletasks
    set x [expr {[winfo screenwidth $w]/2 - [winfo reqwidth $w]/2 \
            - [winfo vrootx [winfo parent $w]]}]
    set y [expr {[winfo screenheight $w]/2 - [winfo reqheight $w]/2 \
            - [winfo vrooty [winfo parent $w]]}]
    wm geom $w +$x+$y
    wm resizable $w 0 0
    wm deiconify $w
    update
}

proc SetTextualScaleSlider {text} {
    global symbolicName
    global blifName

    if {[winfo exists $symbolicName(Scale)] != 0} {
        set blifName(currentScaleValue) "$text"
        update
    }
}

proc ShowXeveShell {} {
    global blifName

    if {$blifName(XeveShell) == 0} {
        catch {destroy .xeveshell}
        return
    }

    toplevel .xeveshell
    wm withdraw .xeveshell
    wm title .xeveshell "Xeve Shell"
    wm group .xeveshell .

    frame .xeveshell.shell -borderwidth 2

    label .xeveshell.shell.label -text "Command"

    frame .xeveshell.shell.cmd -borderwidth 2

    scrollbar .xeveshell.shell.cmd.scrollbar -highlightthickness 0 \
        -command {.xeveshell.shell.cmd.entry xview} -orient {horizontal} \
        -width 11 -relief {sunken}

    entry .xeveshell.shell.cmd.entry -background {#ffffff} -relief {sunken} \
        -xscrollcommand {.xeveshell.shell.cmd.scrollbar set}

    bind .xeveshell.shell.cmd.entry <Return> {
        SendCommand [%W get]
    }

    pack .xeveshell.shell.cmd.entry -expand yes -fill x
    pack .xeveshell.shell.cmd.scrollbar -expand yes -fill x

    pack .xeveshell.shell.label -side left -anchor n
    pack .xeveshell.shell.cmd -side right -expand yes -fill x -anchor n

    frame .xeveshell.buttons -borderwidth 2
    button .xeveshell.buttons.eval -text "Eval" -command {
        SendCommand [.xeveshell.shell.cmd.entry get]
    }
    button .xeveshell.buttons.clear -text "Clear" -command {
        .xeveshell.shell.cmd.entry delete 0 end
    }
    button .xeveshell.buttons.dismiss -text "Dismiss" -command {DestroyXeveShell}

    pack .xeveshell.buttons.eval -side left -expand yes
    pack .xeveshell.buttons.clear -side left -expand yes
    pack .xeveshell.buttons.dismiss -side left -expand yes

    pack .xeveshell.buttons -side bottom -expand yes -fill x
    pack .xeveshell.shell -side top -expand yes -fill both

    wm deiconify .xeveshell

    update
}

proc DestroyXeveShell {} {
    global blifName

    set blifName(XeveShell) 0
    catch {destroy .xeveshell}
}

proc ShowConsole {} {
    global blifName

    if {[winfo exists .console]} {
        if {![winfo ismapped .console]} {
            wm deiconify .console
            raise .console .
            update
            return
        }
        wm withdraw .console
        update
        return
    }
    toplevel .console
    wm withdraw .console
    wm title .console "FSM Reachable State Trace"
    wm group .console .

    label .console.label -text "FSM Reachable State Trace"

    frame .console.cmd -borderwidth 2

    button .console.cmd.close -text Close -command {CloseConsole}
    button .console.cmd.clear -text Clear \
            -command ClearConsole

    pack .console.cmd.close -side left -expand 1 -ipadx 1m -ipady 2m
    pack .console.cmd.clear -side left -expand 1 -ipadx 1m -ipady 2m

    text .console.text -state disabled -highlightthickness 0 -wrap char

    scrollbar .console.vscroll -command ".console.text yview" -orient vertical
    .console.text configure -yscrollcommand ".console.vscroll set"

    pack .console.label -side top -fill x
    pack .console.cmd -side bottom -fill x
    pack .console.vscroll -side right -fill y
    pack .console.text -side left -expand 1 -fill both

    update idletasks
}

proc ShowFsmStats {} {
    global blifName

    if {$blifName(FsmStats) == 0} {
        catch {destroy .stats}
        return
    }
    if {[winfo exist .stats]} {
        wm deiconify .stats
        raise .stats .
        if {[winfo exists $blifName(CurrentResultPanel)]} {
            raise $blifName(CurrentResultPanel) .
        }
        RefreshFsmStats
        update
        return
    }
    toplevel .stats -class Statistics
    wm withdraw .stats
    wm title .stats "FSM Statistics"
    wm group .stats .

    wm geometry .stats 250x190

    label .stats.label -text "FSM Statistics" -anchor w
    button .stats.close -text Close -command CloseFsmStats

    pack .stats.close -side bottom -ipadx 1m -ipady 1m
    pack .stats.label -side top -fill x -padx 2m -pady 1m

    frame .stats.frame -borderwidth 2 -relief groove -width 200

    foreach stat "inputs outputs latches literals states" {
        frame .stats.frame.$stat
        label .stats.frame.$stat.label -text "$stat = "
        label .stats.frame.$stat.value
        pack .stats.frame.$stat.label -side left
        pack .stats.frame.$stat.value -side left

        pack .stats.frame.$stat -expand 1 -fill x
    }

    pack .stats.frame -expand 1 -fill both -padx 2m

    RefreshFsmStats

    wm deiconify .stats
    raise .stats .
    if {[winfo exists $blifName(CurrentResultPanel)]} {
        raise $blifName(CurrentResultPanel) .
    }
    update idletasks
}

# procedure: ShowDataPathSignalWindow

proc ShowDataPathSignalWindow {} {
    global symbolicName
    global blifName

    # -----------------------------------------------------------------------
    # Test if window exists
    # -----------------------------------------------------------------------
    if { [winfo exists $symbolicName(DataPathSinals)] == 1 } {
        # window already exists. Just raises it.
        wm raise $symbolicName(DataPathSinals)
        update
        return
    }

    set w $symbolicName(DataPathSinals)

    # -----------------------------------------------------------------------
    # Create the data-path signals window as a new toplevel window
    # -----------------------------------------------------------------------
    toplevel $w
    wm withdraw $w
    wm group $w .
    wm title $w "Data-Path Signals"
    update

    # -----------------------------------------------------------------------
    # First frame for signals related to tests
    # -----------------------------------------------------------------------

    # A title label 
    label $w.teststitle -text "Test Control Signals"

    # A frame
    frame $w.tests -borderwidth 2 -relief groove

    # A title label for inputs
    label $w.tests.inputs -text "Test Inputs"

    # A scrollbar for the list of test input signals
    scrollbar $w.tests.inputscroll -highlightthickness 0 \
        -command "$w.tests.inputlist yview" -relief {sunken}

    # A text widget for test inputs areas
    text $w.tests.inputlist -borderwidth {2} \
        -cursor {top_left_arrow} \
        -background #ffffff -foreground {#000000} -height {15} \
        -relief {groove} -width {25} -wrap {none} -state disabled \
        -yscrollcommand "$w.tests.inputscroll set" \
        -exportselection 0 -selectborderwidth 0 \
        -selectbackground {#ffffff} \
        -selectforeground {#000000} \
        -highlightthickness 0 \
                                   
    # A title label for outputs
    label $w.tests.outputs -text "Test Outputs"

    # A scrollbar for the list of test output signals
    scrollbar $w.tests.outputscroll -highlightthickness 0 \
        -command "$w.tests.outputlist yview" -relief {sunken}

    # A text widget for test outputs areas
    text $w.tests.outputlist -borderwidth {2} \
        -cursor {top_left_arrow} \
        -background #ffffff -foreground {#000000} -height {15} \
        -relief {groove} -width {25} -wrap {none} -state disabled \
        -yscrollcommand "$w.tests.outputscroll set" \
        -exportselection 0 -selectborderwidth 0 \
        -selectbackground {#ffffff} -selectforeground {#000000} \
        -highlightthickness 0

    # Palettes of colors
    set testInputPalette [ MakeSignalPalette $w.tests input $blifName(verification) ]
    set testOutputPalette [ MakeSignalPalette $w.tests output $blifName(verification) ]

    # -----------------------------------------------------------------------
    # First frame for signals related to actions
    # -----------------------------------------------------------------------

    # A title label 
    label $w.actionstitle -text "Action Control Signals"

    # A frame
    frame $w.actions -borderwidth 2 -relief groove

    # A title label for inputs
    label $w.actions.outputs -text "Action Outputs"

    # A scrollbar for the list of test input signals
    scrollbar $w.actions.outputscroll -highlightthickness 0 \
        -command "$w.actions.outputlist yview" -relief {sunken}

    # A text widget for test outputs areas
    text $w.actions.outputlist -borderwidth {2} \
        -cursor {top_left_arrow} \
        -background #ffffff -foreground {#000000} -height {15} \
        -relief {groove} -width {25} -wrap {none} -state disabled \
        -yscrollcommand "$w.actions.outputscroll set" \
        -exportselection 0 -selectborderwidth 0 \
        -selectbackground {#ffffff} -selectforeground {#000000} \
        -highlightthickness 0

    # Palettes of colors
    set actionOutputPalette [ MakeSignalPalette $w.actions output \
                                  $blifName(verification) ]
                                   
    # -----------------------------------------------------------------------
    # Source Related Information
    # -----------------------------------------------------------------------
    # An frame for source information
    frame $w.source -borderwidth 2

    # A label for source information
    label $w.source.label -text "Source :"

    # An entry for source information
    entry $w.source.entry -relief sunken -background {#ffffff}

    # -----------------------------------------------------------------------
    # Griding
    # -----------------------------------------------------------------------

    grid configure $w.teststitle -row 0 -column 0 -sticky nw -padx 2m
    grid configure $w.tests -row 1 -column 0 -sticky nsew -padx 2m -pady 2m

    grid configure $w.tests.inputs       -row 0 -column 0
    grid configure $w.tests.inputlist    -row 1 -column 0 -sticky nsew
    grid configure $w.tests.inputscroll  -row 1 -column 1 -sticky ns

    grid configure $w.tests.outputs      -row 0 -column 2
    grid configure $w.tests.outputlist   -row 1 -column 2 -sticky nsew
    grid configure $w.tests.outputscroll -row 1 -column 3 -sticky ns

    grid configure $testInputPalette   -row 2 -column 0 -sticky e
    grid configure $testOutputPalette  -row 2 -column 2 -sticky e

    grid configure $w.actionstitle -row 0 -column 1 -sticky nw -padx 2m
    grid configure $w.actions -row 1 -column 1 -sticky nsew -padx 2m -pady 2m

    grid configure $w.actions.outputs      -row 0 -column 0
    grid configure $w.actions.outputlist   -row 1 -column 0 -sticky nsew
    grid configure $w.actions.outputscroll -row 1 -column 1 -sticky ns

    grid configure $w.source -row 2 -columnspan 2 -sticky ew -padx 2m -pady 2m
    grid configure $w.source.label -row 0 -column 0 -sticky w
    grid configure $w.source.entry -row 0 -column 1 -sticky ew

    grid configure $actionOutputPalette  -row 2 -column 0 -sticky e

    grid columnconfigure $w 0 -weight 1
    grid columnconfigure $w 1 -weight 1
    grid rowconfigure    $w 1 -weight 1

    grid columnconfigure $w.tests 0 -weight 1
    grid columnconfigure $w.tests 2 -weight 1
    grid rowconfigure    $w.tests 1 -weight 1

    grid columnconfigure $w.actions 0 -weight 1
    grid rowconfigure    $w.actions 1 -weight 1

    grid columnconfigure $w.source 1 -weight 1
    grid rowconfigure    $w.source 0 -weight 1

    # Display window on the screen
    wm deiconify $w
    update
}

# ***************************************************************************
# * Widgets Manipulation Procedures
# ***************************************************************************
proc InitializePalette { paletteName } {

    upvar #0 $paletteName palette

    for {set i 0} {$i < $palette(colors)} {incr i} {
        set palette([lindex $palette($i) 0]) $i
    }
    set palette(current) [lindex $palette($palette(default)) 0]
    set palette(previous) $palette(current)
}

proc SetPaletteHelpAndState { type paletteName } {
    global blifName

    upvar #0 $paletteName palette

    set w $palette(name)

    set defaultBg [$w cget -background]

    for {set i 0} {$i < $palette(colors)} {incr i} {
        set state [lindex $palette($i) 2]
        if {$state == "disabled" } {
            continue
        }
        set color [lindex $palette($i) 0]
        set help  [lindex $palette($i) 1]
        set text  [lindex $palette($i) 3]

        set image "$blifName(verification):$type:$color"
        $w.$color.$color configure -image $blifName($image) -state $state \
                -command "SetHighlight $type $paletteName $color"

        cb_balloonHelp $w.$color.$color $help

    }
    update
}


proc SetHighlight {type paletteName color } {
    global symbolicName
    global blifName
    global env

    upvar #0 $paletteName palette
    set w $palette(name)

    if {$blifName(${type}List:Mode) == "selection"} {
        PaintSelectedSignalsInColor $type $color
    } {
#       $symbolicName(${type}List) configure \
#           -cursor "hand2 #ffffff $color"
    }

    if {$color == $palette(current)} {
        return
    }

    set defaultBg [$w cget -background]

    set palette(previous) $palette(current)
    $w.$palette(current) configure -relief flat -background $defaultBg
    $w.$palette(current).$palette(current) configure -relief flat
    $w.$color configure -relief groove -background #000000
    $w.$color.$color configure -relief flat
    set palette(current) $color
    update
}

proc MakeSignalPalette {w type op} {
    global blifName
    global ${type}Palette

    set ${type}Palette(colors) [llength $blifName($op,$type)]
    set ${type}Palette(default) 0

    set ${type}Palette(name) $w.${type}Palette

    foreach colorHelp $blifName($op,$type) {
        set index [lindex $colorHelp 0]
        set color [lindex $colorHelp 1]
        set help  [lindex $colorHelp 2]
        set state [lindex $colorHelp 3]
        set text  [lindex $colorHelp 4]

        set ${type}Palette($index) "$color [list $help] $state $text"
    }
    return [MakePaletteFrame $type ${type}Palette]
}

proc MakePaletteFrame { type paletteName } {
    global blifName

    upvar #0 $paletteName palette

    InitializePalette $paletteName

    set w $palette(name)

    catch "destroy $w"

    frame $w -borderwidth 2 -relief groove

    set defaultBg [$w cget -background]

    for {set i 0} {$i < $palette(colors)} {incr i} {
        set state [lindex $palette($i) 2]
        if {$state == "disabled"} {
            continue
        }
        set color [lindex $palette($i) 0]
        set help  [lindex $palette($i) 1]
        set text  [lindex $palette($i) 3]

        set image "$blifName(verification):$type:$color"

        frame $w.$color -borderwidth 3 -relief flat

        button $w.$color.$color -relief flat -state $state
        $w.$color.$color configure \
                -image $blifName($image) \
                -command "SetHighlight $type $paletteName $color"

        cb_balloonHelp $w.$color.$color $help

        pack $w.$color.$color
        pack $w.$color -side right
    }

    set color [lindex $palette($palette(default)) 0]

    $w.$color.$color configure -relief flat
    $w.$color configure -relief groove -background #000000; #yellow

    return $w
    update
}

proc ChangePaletteHelp { } {
    global blifName
    global inputPalette
    global outputPalette

    set type input
    set op $blifName(verification)

    foreach type "input output" {
        set ${type}Palette(colors) [llength $blifName($op,$type)]
        set ${type}Palette(default) 0
        set default 0
        foreach colorHelp $blifName($op,$type) {
            set state [lindex $colorHelp 3]
            set index [lindex $colorHelp 0]
            set color [lindex $colorHelp 1]
            set help  [lindex $colorHelp 2]
            set text  [lindex $colorHelp 4]

            if {$index == $default} {
                set defaultColor $color
            }

            set ${type}Palette($index) "$color [list $help] $state $text"
        }
        set defaultColor [eval lindex $${type}Palette($default) 0]
        # SetPaletteHelpAndState $type ${type}Palette
        pack [MakePaletteFrame $type ${type}Palette] -side right \
            -expand 1 -anchor e \
            -padx 5m

        
        # SetHighlight ${type}Palette $defaultColor

    }
    update
}

proc PutsToConsole {text} {
    global symbolicName

    $symbolicName(Console:Text) configure -state normal
    $symbolicName(Console:Text) insert end "$text"
    $symbolicName(Console:Text) configure -state disabled
    $symbolicName(Console:Text) see end
    update idletasks
}

proc ClearConsole {} {
    global symbolicName

    $symbolicName(Console:Text) configure -state normal
    $symbolicName(Console:Text) delete 1.0 end
    $symbolicName(Console:Text) configure -state disabled
    update idletasks
}

proc CloseConsole {} {
    global blifName

    set blifName(ReachableTrace) 0
    catch {wm withdraw .console}
}

proc RefreshFsmStats {} {
    global blifName

    foreach stat "inputs outputs latches literals states" {
        if {[info exists blifName(fsm:stat:$stat)]} {
            ShowStat $stat $blifName(fsm:stat:$stat)
        } else {
            ShowStat $stat ""
        }
    }
}

proc CloseFsmStats {} {
    global blifName

    set blifName(FsmStats) 0
    catch {destroy .stats}
}

proc SetStats {stat value} {
    global blifName

    set blifName(fsm:stat:$stat) $value
    ShowStat $stat $value
}

proc ShowStat {stat value} {

    if {[winfo exists .stats]} {
        .stats.frame.$stat.value configure -text $value
        update
    }

}

proc ClearFsmStats {} {
    global symbolicName
    global blifName

    foreach stat "inputs outputs latches literals states" {
        catch {unset blifName(fsm:stat:$stat)}
    }
    update
}
    
# Procedure: SeeOrHideDataPathSignals
proc SeeOrHideDataPathSignals {} {
    global blifName

    if { $blifName(DataPathSignals) == 0 } {
        catch {destroy $symbolicName(DataPathSignals)}
    }

    if { [ info exist blifName(DataPathFile) ] == 0 } {
        # LoadDataPathFile
    }

    ShowDataPathSignalWindow
}

# Procedure: ClearAndResetAll
proc ClearAndResetAll {} {
    global symbolicName
    global blifName

    ClearFileSelection
    ClearInputOutputList

    catch {destroy .checkoutput}
    catch {destroy .reduce}
    catch {destroy .reachable_states}
    catch {destroy .advanced}

    foreach sig $blifName(CheckOutputList) {
        unset blifName($sig,file) blifName($sig,index) \
                blifName($sig,checked) blifName($sig,status)
    }
    set blifName(CheckOutputList) {}
}

# Procedure: ClearAndResetSignalLists
proc ClearAndResetSignalLists {} {
    global blifName

    unset blifName(inputList)
    unset blifName(outputList)
    set blifName(inputList) {}
    set blifName(outputList) {}
}

# Procedure: ResetReducePanel
proc ResetReducePanel {} {
     global symbolicName

    set w .reduce
    if {[winfo exists $w]} {
        $w$symbolicName(MinimizedStates) configure -text ""
        update
    }
}

# Procedure: DisableButtons
proc DisableButtons {} {
    global symbolicName

    DisableSignalSelection

    $symbolicName(VerifyButton) configure -state disabled

    $symbolicName(CheckOutputButton) configure -state disabled
    $symbolicName(ReduceButton) configure -state disabled
    $symbolicName(CommandMenu) configure -state disabled

    bind $symbolicName(BlifFileEntry) <Key-Return> { break }
    bind $symbolicName(RelationFileEntry) <Key-Return> { break }

    $symbolicName(FilesMenu) entryconfigure 0 -state disabled
    $symbolicName(FilesMenu) entryconfigure 1 -state disabled
    $symbolicName(FilesMenu) entryconfigure 3 -state disabled

    $symbolicName(OptionMenu) entryconfigure 0 -state disabled
    # $symbolicName(OptionMenu) entryconfigure 1 -state disabled

    update
}

# Procedure: EnableButtons
proc EnableButtons {} {
    global symbolicName

    EnableSignalSelection

    $symbolicName(VerifyButton) configure -state normal 
    $symbolicName(CheckOutputButton) configure -state normal
    $symbolicName(ReduceButton) configure -state normal
    $symbolicName(CommandMenu) configure -state normal

    bind $symbolicName(BlifFileEntry) <Key-Return> {
        LoadBlifFromSelection
    }
    bind $symbolicName(RelationFileEntry) <Key-Return> {
        LoadBlifFromSelection
    }

    $symbolicName(FilesMenu) entryconfigure 0 -state normal
    $symbolicName(FilesMenu) entryconfigure 1 -state normal
    $symbolicName(FilesMenu) entryconfigure 3 -state normal

    $symbolicName(OptionMenu) entryconfigure 0 -state normal
    $symbolicName(OptionMenu) entryconfigure 1 -state normal

    update
}

# Procedure: DisableSignalSelection
proc DisableSignalSelection {} {
    global symbolicName

    foreach type "input output" {

        bind $symbolicName(${type}List) <Button-1>          { break }
        bind $symbolicName(${type}List) <B1-Motion>         { break }
        bind $symbolicName(${type}List) <Shift-Button-1>    { break }
        bind $symbolicName(${type}List) <B1-ButtonRelease>  { break }
        bind $symbolicName(${type}List) <Control-a>         { break }
        bind $symbolicName(${type}List) <Control-A>         { break }
        bind $symbolicName(${type}List) <Control-Button-1>  { break }
        bind $symbolicName(${type}List) <Control-B1-Motion> { break }
    }
}

# Procedure: EnableSignalSelection
proc EnableSignalSelection {} {
    global symbolicName
    global blifName

    SetSignalListBindingMode input 
    SetSignalListBindingMode output 
}

# Procedure: SetSignalListBindingMode
proc SetSignalListBindingMode {type} {
    global symbolicName

    bind $symbolicName(${type}List) <Control-a> "
        SelectOrPaintAll $type
        break
    "
    bind $symbolicName(${type}List) <Control-A> "
        SelectOrPaintAll $type
        break
    "
    bind $symbolicName(${type}List) <B1-ButtonRelease> "
        ReleasePaintSignal ${type}List
        break
    "
    bind $symbolicName(${type}List) <Shift-Button-1> "
        ShiftSelectOrPaintSignalFromCoords ${type}List \
            $${type}Palette(current) %W %x %y 
        break
    "
    bind $symbolicName(${type}List) <Control-Button-1> "
        SelectOrPaintSignalFromCoords ${type}List \
            $${type}Palette(current) %W %x %y 1
        break
    "
    bind $symbolicName(${type}List) <Button-1> "
        SelectOrPaintSignalFromCoords ${type}List \
            $${type}Palette(current) %W %x %y
        break
    "
    bind $symbolicName(${type}List) <Control-B1-Motion> "
        MotionSelectOrPaintSignalFromCoords ${type}List \
              $${type}Palette(current) %W %x %y 1
        break
    "
    bind $symbolicName(${type}List) <B1-Motion> "
        MotionSelectOrPaintSignalFromCoords ${type}List \
              $${type}Palette(current) %W %x %y
        break
    "
    bind $symbolicName(${type}List) <Enter> "
        focus $symbolicName(${type}List)
    "

}

proc RestoreSignalColors {} {
    global blifName
    global symbolicName

    set verif $blifName(verification)
    foreach list "inputList outputList" {
        set w $symbolicName($list)
        foreach el $blifName($list) {
            set tag [lindex $blifName($verif:$list:$el) 0]
            set start [lindex $blifName($verif:$list:$el) 1]
            set end [lindex $blifName($verif:$list:$el) 2]
            set selectTag [lindex $blifName($verif:$list:$el) 3]

            foreach oldtag [$w tag names $start] {
                $w tag remove $oldtag $start $end
            }
            $w tag add $tag $start $end
            if {$selectTag == 1} {
                $w tag add selected $start $end
            }
        }
    }
    update
}

# Procedure: PrintSyntax
proc PrintSyntax {} {

    puts stderr "--- xeve: Syntax: \"xeve -Help\": Prints this help"
    puts stderr "--- xeve: Syntax: \"xeve -info\": Prints program info"
    puts stderr "--- xeve:         \"xeve \[file.\[blif\]\]\": Displays Xeve GUI and load file.blif"
}

# Procedure: DisplayWhatMessage
proc DisplayWhatMessage {msg} {
    global symbolicName
    global blifName

    set w $blifName(CurrentResultPanel)
    if {[winfo exists $w]} {
        $w$symbolicName(WhatMsg) configure -text $msg
        update
    }
}


