# ***************************************************************************
# * FC2 PACKAGE SOURCE FILE
# * 
# * xeve-proc.tcl -- Tcl Procedures and Xeve Initialisations
# ***************************************************************************

# ***************************************************************************
# * General Procedures
# ***************************************************************************
# Procedure SendCommand
proc SendCommand {command {errorScript ""}} {
    global blifName


    if {[info exists blifName(XeveOneThread)]} {
#	puts stderr "Eval: $command"
	eval $command
    } {
#	puts stderr "Puts to command process: $command"
	puts stdout "$command"
    }
}
 
# startup source
proc StartupSrc {args} {
    global env
    global argc
    global argv
    global symbolicName
    global blifName
    global prefs
    global cb_tools

    if {$argc > 1} {
        puts stderr "*** xeve: error: too much arguments"
        PrintSyntax
        exit
    }
    for {set counter 0} {$counter < $argc} {incr counter 1} {
        case [lindex $argv $counter] in {
            {default} {
                set blifName(selectedFile) [lindex $argv $counter]
            }
        }
    }

    # Set up the balloon help text for input/output color palettes
    set blifName(colorList) "#000000 #a5a5a5 #0000ff #ff0000"
    set blifName(reduce,input) {
        {0 #000000 "Visible input signal" normal ""}
        {1 #a5a5a5  "Hidden input signal" normal ""}
        {2 #0000ff  "" disabled ""}
        {3 #ff0000   "" disabled ""}
    }
    set blifName(reduce,input:default) 0

    set blifName(reduce,output) {
        {0 #000000 "Visible output signal" normal ""}
        {1 #a5a5a5  "Hidden output signal" normal ""}
        {2 #0000ff  "" disabled ""}
        {3 #ff0000   "" disabled ""}
    }
    set blifName(reduce,output:default) 0

    set blifName(checkoutput,input) {
        {0 #000000 "Input signal can have any value" normal ""}
        {1 #a5a5a5  "" disabled ""}
        {2 #0000ff  "Input signal set as always absent" normal "0"}
        {3 #ff0000   "Input signal set as always present" normal "1"}
    }
    set blifName(checkoutput,input:default) 0

    set blifName(checkoutput,output) {
        {0 #000000 "No check on output signal" normal ""}
        {1 #a5a5a5  "" disabled ""}
        {2 #0000ff  "Check if output signal is possibly not emitted" normal ""}
        {3 #ff0000   "Check if output signal is possibly emitted" normal ""}
    }
    set blifName(checkoutput,outputdefault) 0

    set blifName(verification:initial) checkoutput
    set blifName(verification) checkoutput
    set blifName(preverif) checkoutput
    set cb_tools(balloon_help) 1

    # Variables related to the scale $symbolicName(Scale)
    set blifName(currentScaleValue) 0
    set blifName(scaleFrom) 0
    set blifName(scaleTo) 0

    # Check in PATH if Atg is reachable
    set blifName(AtgExists) 0
    set dirList [split $env(PATH) ":"]
    foreach dir $dirList {
        if {[file exists $dir/atg] && [file executable $dir/atg]} {
            set blifName(AtgExists) 1
            break
        }
    }
}

# end source
proc EndSrc {} {
    global symbolicName
    global blifName
    global cb_tools
    global argc
    global argv

    SetBalloonHelp
    SetSignalListDefaults

    if {$blifName(selectedFile) != ""} {
        DisableButtons
        SendCommand "read_blif $blifName(selectedFile)"
    } else {
        $symbolicName(OptionMenu) entryconfigure 0 -state disabled
    }
    RefreshFileSelection
    bind all <Control-q> {Quit}
    bind all <Control-Q> {Quit}
    SendCommand "set_tgr_flags 12"
    ShowConsole
}

# initialize global variables
proc InitGlobals {} {
    global env
    global blifName

    set blifName(Fc2File) {}
    set blifName(HideInputs) {1}
    set blifName(HideOutputs) {0}
    set blifName(inputList) {}
    set blifName(inputObs) {inputSee}
    set blifName(KeepActWires) {0}
    set blifName(KeepIfInWires) {0}
    set blifName(KeepIncr) {0}
    set blifName(outputList) {}
    set blifName(outputObs) {outputSee}
    set blifName(Relations) {1}
    set blifName(keepActWire) {0}
    set blifName(keepIfInWire) {0}
    set blifName(keepIncr) {0}
    set blifName(savePath) {0}
    set blifName(Beginner) {0}
    set {blifName(Beginner:Tip)} {InitialStep}
    set blifName(OnLineHelp) {0}
    set blifName(ExecNumber) {0}
    set blifName(AtgCallNumber) {0}
    set blifName(CheckOutputList) {}
    set blifName(FsmStats) 0
    set blifName(ReachableTrace) 0
    set blifName(DataPathSignals) 0
    set blifName(inputList:selectionDirection) 0
    set blifName(outputList:selectionDirection) 0
    set blifName(inputList:selectionStart) 0
    set blifName(outputList:selectionStart) 0
    set blifName(inputList:selectionLast) 0
    set blifName(outputList:selectionLast) 0

    set blifName(FileTypes) {
	{"Blif   Files"       {.blif}   }
	{"Bddf   Files"       {.bddf}   }
	{"Csimul Files"       {.esi .csimul} }
	{"Fc2    Files"       {.fc2}    }
	{"Atg    Files"       {.atg}    }
	{"All    Files"        *        }
    }

    set blifName(CurrentResultPanel) {}
    set blifName(selectedFile) {}
    set blifName(relationFile) {}

    set blifName(XeveShell) 0

    global processId

    global hideInputs
    set hideInputs {0}
    global hideOutputs
    set hideOutputs {0}
    global keepActWire
    set keepActWire {0}
    global keepIfInWire
    set keepIfInWire {0}
    global keepIncr
    set keepIncr {0}
    global outputObs
    set outputObs outputSee
    global result
    set result {}

    global symbolicName

    set symbolicName(root) {.}

    set symbolicName(CommandMenu) {.menu.verification}
    set symbolicName(FilesMenu)   {.menu.files.m}
    set symbolicName(OptionMenu)  {.menu.options.m}

    set symbolicName(WhatMsg)          {.frame3.message1}
    set symbolicName(EndMsg)           {.frame3.message2}
    set symbolicName(inputList)        {.frame3.frame4.frame.text0}
    set symbolicName(outputList)       {.frame3.frame5.frame.text0}

    set symbolicName(FsmFileLabel)      {.frame.files.fsm}
    set symbolicName(RelationFileLabel) {.frame.files.relation}
    set symbolicName(BlifFileEntry)     {.frame.files.frame1.entry2}
    set symbolicName(RelationFileEntry) {.frame.files.frame2.entry2}

    set symbolicName(StateBddNodes)       {.frame18.frame2.label9}
    set symbolicName(EquivalenceBddNodes) {.frame18.frame4.label9}

    set symbolicName(ReachableStates) {.frame7.frame1.label2}
    set symbolicName(MinimizedStates) {.frame7.frame2.label2}

    set symbolicName(DrawAutomaton) {.frame1.button5}
    set symbolicName(Dismiss)       {.frame1.button6}
    set symbolicName(AbortButton)   {.frame1.button7}

    set symbolicName(CheckOutputList) {.frame5.signals}

    set symbolicName(CheckOutputName)   {.frame18.output}
    set symbolicName(CheckOutputStatus) {.frame18.status}
    set symbolicName(CheckOutputFile)   {.frame18.file}

    set symbolicName(HelpContents) {.help.frame1.listbox}

    set symbolicName(VerifyButton)      {.verif.apply}
    set symbolicName(CheckOutputButton) {.verif.select.checkoutput}
    set symbolicName(ReduceButton)      {.verif.select.reduce}

    set symbolicName(Console)       {.console}
    set symbolicName(Console:Text)  {.console.text}
    set symbolicName(Console:Close) {.console.cmd.close}
    set symbolicName(Console:Clear) {.console.cmd.clear}

    set symbolicName(Scale)         {.topscale}
    set symbolicName(Scale:Message) {.topscale.frame.text}
    set symbolicName(Scale:Slider)  {.topscale.frame.scale.slider}

    set symbolicName(StatMessage) {.stats.msg}

    set symbolicName(inputPalette:SelectMode) {.frame3.frame4.frame1.select}
    set symbolicName(inputPalette:PaintMode)  {.frame3.frame4.frame1.brush}
    set symbolicName(outputPalette:SelectMode) {.frame3.frame5.frame1.select}
    set symbolicName(outputPalette:PaintMode)  {.frame3.frame5.frame1.brush}

    set symbolicName(DataPathSignals)  {.datapath}
    
    set symbolicName(XeveConsole) {.console}
    set symbolicName(XeveConsole:Text) {.console.text}

    if {![info exist env(XEVE_LIB)]} {
	set env(XEVE_LIB) [pwd]
    }

    if {[info exist env(HOME)] && [file exist $env(HOME)/.xeverc]} {
	if {[catch {source $env(HOME)/.xeverc} error]} {
	    Error ".xeverc load failed:\n$errorInfo"
	}
    }

    global blifName

    foreach sigType "input output" {
	foreach color {\#000000 \#a5a5a5 \#ff0000 \#0000ff} {
	    set blifName(reduce:$sigType:$color) \
		[image create bitmap -file "$env(XEVE_LIB)/square.xbm" \
		     -foreground ${color} -background \#ffffff ]
	}
    }
    foreach color {\#000000 \#a5a5a5 \#ff0000 \#0000ff} {
	set blifName(checkoutput:output:$color) \
	    [image create bitmap -file "$env(XEVE_LIB)/square.xbm" \
		 -foreground ${color} -background \#ffffff ]
    }

    set blifName(checkoutput:input:\#0000ff) \
	[image create bitmap -file "$env(XEVE_LIB)/square0.xbm" \
	     -foreground \#0000ff -background \#ffffff ]
    
    set blifName(checkoutput:input:\#ff0000) \
	[image create bitmap -file "$env(XEVE_LIB)/square1.xbm" \
	     -foreground \#ff0000 -background \#ffffff ]

    foreach color {\#000000 \#a5a5a5} {
	set blifName(checkoutput:input:$color) \
	    [image create bitmap -file "$env(XEVE_LIB)/square.xbm" \
		 -foreground ${color} -background \#ffffff ]
    }

    set blifName(photo:xeve) \
	[image create photo -file "$env(XEVE_LIB)/xeve-logo.gif" \
	     -format gif ]


    set blifName(CurrentDirectory) [pwd]

    # Under developpement flag
    global blifName
    set blifName(UnderDevelopment) 0
}

# Procedure: Quit
proc Quit {} {

   quit_xeve
}

# Procedure: XeveStartUp
proc XeveStartUp {} {
    global errorInfo

    StartupSrc

    InitGlobals
    wm withdraw .
    Message "Loading xeve, please wait..." 0

    ShowMainPanel

    DestroyMessage
    wm deiconify .

    EndSrc

    # trace variable errorInfo w PutsTraceVariable
    update
}

# Procedure: PutsTraceVariable
proc PutsTraceVariable {name1 name2 op} {
    global errorInfo

    if {$name1 == "errorInfo"} {
        puts stderr "$op on $name1 = \"$errorInfo\""
    }
}


# ***************************************************************************
# * File Manipulation Procedures
# ***************************************************************************
# Procedure: RefreshFileSelection
proc RefreshFileSelection {} {
    global symbolicName
    global blifName

    $symbolicName(BlifFileEntry) delete 0 end
    $symbolicName(RelationFileEntry) delete 0 end
    if {$blifName(selectedFile) != ""} {
        set fileName [file tail $blifName(selectedFile)]
        set dir [file dirname $blifName(selectedFile)]
        if {[string index $dir 0]  == "/"} {
            set blifName(CurrentDirectory) $dir
        } else {
            if {$dir != "."} {
                set blifName(CurrentDirectory) $blifName(CurrentDirectory)/$dir
            }
        }
        $symbolicName(BlifFileEntry) insert 0 $fileName
        $symbolicName(BlifFileEntry) xview moveto 1
    }
    if {$blifName(relationFile) != ""} {
        set fileName [file tail $blifName(relationFile)]
        $symbolicName(RelationFileEntry) insert 0 $fileName
        $symbolicName(RelationFileEntry) xview moveto 1
    }
    update
}

# Procedure: ClearEntry
proc ClearFileSelection {} {
    global symbolicName

    $symbolicName(BlifFileEntry) delete 0 end
    $symbolicName(RelationFileEntry) delete 0 end
    update
}

# Procedure: LoadBlif
proc LoadBlif { selectedFile {relationFile ""}} {
    global symbolicName
    global blifName
    global onLineHelp
    global resultName
    global errorInfo

    $symbolicName(OptionMenu) entryconfigure 0 -state normal
    set blifName(relationFile) $relationFile
    set blifName(selectedFile) $selectedFile

    RefreshFileSelection

    SetInputOutputList $blifName(selectedFile)

    set blifName(Fc2File) "[file rootname $blifName(selectedFile)].fc2"

    catch {unset resultName}

    EnableButtons

    ClearFsmStats
    SendCommand "get_fsm_stats"
    ShowFsmStats

    set blifName(Beginner:Tip) LoadBlif
    OnLineInfo LoadBlif

    update
    return 1
}

# Procedure: TestFileForOpening
proc TestFileForOpening { file} {

    set errorMsg "Open failed on $file"
    if {[file exists $file]==0} {
        Error "$errorMsg: file does not exist"
        return 0
    }
    if {[file isfile $file]==0} {
        Error "$errorMsg: not a regular file"
        return 0
    }
    if {[file readable $file]==0} {
        Error "$errorMsg: read permission denied"
        return 0
    }
    return 1
}

# Procedure: TestFileForWriting
proc TestFileForWriting { file } {

    set dir [file dirname $file]
    if {[file exists $file]} {
        if {[file isfile $file]} {
            if {[file writable $file]} {
                if {[file writable $dir]==0} {
                    Error "$dir: write directory permission denied"
                    return 0
                }
            } {
                Error "$file: write permission denied"
                return 0
            }
        } elseif {[file isdirectory $file]} {
            Error "$file: selected file is a directory"
        } {
            Error "$file: not a regular file"
        }
    } elseif {[file writable $dir]==0} {
        Error "$dir: write directory permission denied"
        return 0
    }
    update
    return 1
}

# Procedure: TestFileIsBlif
proc TestFileIsBlif { file} {

    if {[file extension $file] != ".blif"} {
        Error "Open failed on $file: not a blif file"
        return 0
    }
    return 1
}

# Procedure: LoadBlifFromBrowser
proc LoadBlifFromBrowser {loadRelation} {
    global blifName
    global symbolicName

    set fg [$symbolicName(FsmFileLabel) cget -foreground]
    set bg [$symbolicName(FsmFileLabel) cget -background]
    $symbolicName(FsmFileLabel) configure -foreground #ff0000 \
            -background #ffffff
    set selectedFile \
            [tk_getOpenFile -title "Select a FSM blif file" \
            -initialdir $blifName(CurrentDirectory) \
            -defaultextension blif -parent . \
            -filetypes {{"Blif Files" {.blif}}}]
    $symbolicName(FsmFileLabel) configure -foreground $fg \
            -background $bg
    if {$selectedFile != ""} {
        if {[file extension $selectedFile] != ".blif"} {
            Error "$selectedFile: bad blif file\
                    (Must have the \".blif\" extension)"
            return 0
        }
        set relationFile ""
        if {$loadRelation == "1" &&
        [YesNoQuestion "Do you want to open a Relation file \
                (defining input relations)?"] == 0} {
            set blifName(CurrentDirectory) [file dirname $selectedFile]
            set resultOk 0
            while {$resultOk == "0"} {
                set relationFile [LoadRelationBlifFromBrowser]
                if {$relationFile == $selectedFile} {
                    if {[YesNoQuestion "Bad choice for Relations: \
                            Blif file and Relation file are identical. \
                            Try again ?"] == 1} {
                        set resultOk 1
                    }
                    set relationFile ""
                } {
                    set resultOk 1
                }
            }
        }
        set blifName(CurrentDirectory) [file dirname $selectedFile]
        DisableButtons
        SendCommand "read_blif $selectedFile $relationFile"
    }
    return 1
}

# Procedure: LoadBddfFromBrowser
proc LoadBddfFromBrowser {} {
    global blifName
    global symbolicName
    global errorInfo

    set fg [$symbolicName(FsmFileLabel) cget -foreground]
    set bg [$symbolicName(FsmFileLabel) cget -background]
    $symbolicName(FsmFileLabel) configure  -foreground #ff0000 \
            -background #ffffff
    set selectedFile \
            [tk_getOpenFile -defaultextension bddf -parent . \
            -initialdir $blifName(CurrentDirectory) \
            -title "Select a FSM bddf file" \
	    -filetypes {{"Bddf Files" {.bddf}}}]
    $symbolicName(FsmFileLabel) configure -foreground $fg \
            -background $bg
    if {$selectedFile != ""} {
        if {[file extension $selectedFile] != ".bddf"} {
            Error "$selectedFile: bad bddf file\
                    (Must have the \".bddf\" extension)"
            return 0
        }
        set blifName(CurrentDirectory) [file dirname $selectedFile]
        DisableButtons
        SendCommand "read_blif $selectedFile"
    }
    return 1
}

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

    set fg [$symbolicName(RelationFileLabel) cget -foreground]
    set bg [$symbolicName(RelationFileLabel) cget -background]
    $symbolicName(RelationFileLabel) configure -background #ffffff \
            -foreground #ff0000
    set selectedFile \
            [tk_getOpenFile -defaultextension blif -parent . \
            -initialdir $blifName(CurrentDirectory) \
            -title "Select a Relation file" \
            -filetypes {{"Blif Files" {.blif}}}]
    $symbolicName(RelationFileLabel) configure -foreground $fg \
            -background $bg
    if {$selectedFile != ""} {
        if {[file extension $selectedFile] != ".blif"} {
            Error "$selectedFile: bad blif file\
                    (Must have the \".blif\" extension)"
            return ""
        }
    }
    return $selectedFile
}

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

    focus .
    set selectedFile [$symbolicName(BlifFileEntry) get]
    if {$selectedFile == ""} {
        RefreshFileSelection
        return
    }
    if {[file extension $selectedFile] != ".blif" &&
        [file extension $selectedFile] != ".bddf"} {
        Error "$selectedFile bad file. Must have the \".blif\" or \"bddf\" extension."
        RefreshFileSelection
        return
    }
    set list [file split $selectedFile]
    if {[lindex $list 0] != "/"} {
        set selectedDir $blifName(CurrentDirectory)
        if {$selectedDir != ""} {
            set selectedFile $selectedDir/$selectedFile
        }
    }
    set fileName [$symbolicName(RelationFileEntry) get]
    set relationFile ""
    if {$fileName != ""} {
        if {[file extension $fileName] != ".blif"} {
            Error "$fileName: bad relation file\
                    (Must have the \".blif\" extension)"
            RefreshFileSelection
            return
        }
        set list [file split $fileName]
        if {[lindex $list 0] != "/"} {
            set selectedDir $blifName(CurrentDirectory)
            if {$selectedDir != ""} {
                set relationFile $selectedDir/$fileName
            } {
                set relationFile $fileName
            }
        }
    }
    if {$selectedFile != $blifName(selectedFile) ||
    $relationFile != $blifName(relationFile)} {
        DisableButtons
        SendCommand "read_blif $selectedFile $relationFile"
    }
}

# Procedure: GetFc2FileNameFromUser
proc GetFc2FileNameFromUser {} {
    global fsBox
    global blifName

    set blifName(Beginner:Tip) Fc2File
    OnLineInfo Fc2File
    set fileName [file tail $blifName(Fc2File)]
    return [tk_getSaveFile -defaultextension fc2 -parent . \
            -initialdir $blifName(CurrentDirectory) \
            -title "Select a FC2 file" -initialfile $fileName \
            -filetypes {{"Fc2 Files" {.fc2}}}]
}

# Procedure: SaveFsmInBddf
proc SaveFsmInBddf {} {
    global fsBox
    global blifName

    if {$blifName(selectedFile) == ""} {
        Error "No FSM in current context"
        return
    }
    set blifName(BddfFile) "[file rootname $blifName(selectedFile)].bddf"
    set fileName [file tail $blifName(BddfFile)]
    set selectedBddfFile \
            [tk_getSaveFile -defaultextension fc2 -parent . \
            -initialfile $blifName(CurrentDirectory) \
            -title "Select a BDDF file" -initialfile $fileName \
            -filetypes {{"Bddf Files" {.bddf}}}]

    if {$selectedBddfFile != ""} {
        SendCommand "save_fsm $selectedBddfFile bddf"
    }
}

# Procedure: GetFc2FileName
proc GetFc2FileName {} {
    global blifName

    set blifName(SavedFc2File) ""
    set fileName [GetFc2FileNameFromUser]
    if {$fileName != "" && [TestFileForWriting $fileName]!=0} {
        set blifName(SavedFc2File) $fileName
        return 1
    }
    return 0
}


# ***************************************************************************
# * Signal List Manipulation Procedures
# ***************************************************************************
proc SignalPaintMode {sigType} {
    global symbolicName
    global ${sigType}Palette
    global blifName
    global env

    set list ${sigType}List
    set w $symbolicName($list)
    set verif $blifName(verification)

    set selectedSignalList [TagListToSignalList $list selected]
    foreach signal $selectedSignalList {
        set signalList $blifName($verif:$list:$signal)
        set startLine  [lindex $signalList 1]
        set endLine    [lindex $signalList 2]

        $w tag remove selected  $startLine $endLine

        set blifName($verif:$list:$signal) [lreplace $signalList 3 3 0]
    }

    $symbolicName(${sigType}Palette:SelectMode) configure -relief flat
    $symbolicName(${sigType}Palette:PaintMode) configure -relief sunken

    set blifName(${sigType}List:Mode) "painting"
    set blifName(${sigType}List:selectionStart) 0

    cb_balloonHelp $symbolicName(${sigType}List) \
        "Use palette and buttons below to color signals" 500
}

proc SignalSelectMode {sigType} {
    global symbolicName
    global blifName

    $symbolicName(${sigType}Palette:SelectMode) configure -relief sunken
    $symbolicName(${sigType}Palette:PaintMode) configure -relief flat

    $symbolicName(${sigType}List) configure -cursor {top_left_arrow}

    set blifName(${sigType}List:Mode) "selection"
    set blifName(${sigType}List:selectionStart) 0

    cb_balloonHelp $symbolicName(${sigType}List) \
        "Use palette and buttons below to color signals select signals" 500
}

# Procedure: ClearInputOutputList
proc ClearInputOutputList {} {
    global symbolicName

    EnableSignalLists
    $symbolicName(inputList) delete 0.0 end
    $symbolicName(outputList) delete 0.0 end
    update
    DisableSignalLists
}

proc SetSignalListDefaults {} {
    global symbolicName
    global blifName

    foreach type "input output" {
        $symbolicName(${type}List) tag configure "\#000000" \
            -foreground \#000000 -background \#ffffff
        $symbolicName(${type}List) tag configure "\#0000ff" \
            -foreground \#0000ff -background \#ffffff
        $symbolicName(${type}List) tag configure "\#ff0000" \
            -foreground \#ff0000 -background \#ffffff
        $symbolicName(${type}List) tag configure "\#a5a5a5" \
            -foreground \#a5a5a5 -background \#ffffff
        $symbolicName(${type}List) tag configure "selected" \
            -background \#c0c0c0
        $symbolicName(${type}List) tag raise selected

        cb_balloonHelp $symbolicName(${type}Palette:SelectMode) \
            "Selection mode: press the mouse left button, pass\
             over the signal names you want to select, and click on a color\
             to paint the selection"
        cb_balloonHelp $symbolicName(${type}Palette:PaintMode) \
            "Painting mode: choose a color, press the mouse left\
             button and pass over the signal names you want to color"

        SignalPaintMode $type
    }
}

proc SeeOrHideActionOutputs {} {
    global blifName

    SendCommand "signals -action $blifName(Signals:ActionOutputs)"
}

proc SeeOrHideTestInputs {} {
    global blifName

    SendCommand "signals -test_inputs $blifName(Signals:TestInputs)"
}

proc SeeOrHideTestOutputs {} {
    global blifName

    SendCommand "signals -test_outputs $blifName(Signals:TestOutputs)"
}

# Procedure: AddSignalInList
proc AddSignalInList {type name} {
    global symbolicName
    global blifName

    lappend blifName(${type}List) $name
}

# Procedure: EnableSignalLists
proc EnableSignalLists {} {
    global symbolicName

    $symbolicName(inputList) configure -state normal
    $symbolicName(outputList) configure -state normal
    update
}

# Procedure: DisableSignalLists
proc DisableSignalLists {} {
    global symbolicName

    $symbolicName(inputList) configure -state disabled
    $symbolicName(outputList) configure -state disabled
}

# Procedure: SetInputOutputList
proc SetInputOutputList { blifFile} {
    global symbolicName
    global blifName
    global inputPalette
    global outputPalette

    EnableSignalLists
    foreach list "inputList outputList" {
        foreach el $blifName($list) {
            set name [lindex $el 0]
            $symbolicName($list) insert end $name\n
        }
    }
    DisableSignalLists
    foreach type "reduce checkoutput" {
        foreach list "inputList outputList" {
            set w $symbolicName($list)
            set line 1
            foreach el $blifName($list) {
                set name [lindex $el 0]
                set startLine $line.0
                set endLine [$w index "$line.0 lineend"]
                set blifName($type:$list:$name) \
                    [list \#000000 $startLine $endLine 0]
                     incr line
            }
        }
    }
    update
}

# Procedure: SelectOrPaintAll
proc SelectOrPaintAll { type } {
    global ${type}Palette
    global blifName
    global symbolicName

    set list ${type}List

    if {$blifName($list:Mode) == "selection"} {
        set tag selected
        set id 3
        set newValue 1
    } {
        eval "set tag $${type}Palette(current)"
        set id 0
        set newValue $tag
    }
    set verif $blifName(verification)

    foreach signal $blifName($list) {
        set signalProp $blifName($verif:$list:$signal)
        set startLine [lindex $signalProp 1]
        set endLine   [lindex $signalProp 2]

        if {$blifName($list:Mode) != "selection"} {
            foreach oldtag [$symbolicName($list) tag names $startLine] {
                $symbolicName($list) tag remove $oldtag $startLine $endLine
            }
        }

        $symbolicName($list) tag add $tag $startLine $endLine
        set blifName($verif:$list:$signal) \
            [lreplace $blifName($verif:$list:$signal) $id $id $newValue]
    }
    update
}

# Procedure: SelectAll
proc SelectAll { list } {
    global blifName
    global symbolicName

    set verif $blifName(verification)
    foreach signal $blifName($list) {
        set signalProp $blifName($verif:$list:$signal)
        set startLine [lindex $signalProp 1]
        set endLine   [lindex $signalProp 2]

        $symbolicName($list) tag add selected $startLine $endLine
        set blifName($verif:$list:$signal) \
            [lreplace $blifName($verif:$list:$signal) 3 3 1]
    }
    update
}

# Procedure: UnselectAll
proc UnselectAll {list} {
    global blifName
    global symbolicName

    set w $symbolicName($list)
    set verif $blifName(verification)

    foreach signal $blifName($list) {
        set signalProp $blifName($verif:$list:$signal)
        set color     [lindex $signalProp 0]
        set startLine [lindex $signalProp 1]
        set endLine   [lindex $signalProp 2]

        $w tag remove selected $startLine $endLine

        set blifName($verif:$list:$signal) \
            [lreplace $blifName($verif:$list:$signal) 3 3 0]
    }
    update
}


# Procedure: ReleasePaintSignal
proc ReleasePaintSignal {list} {
    global blifName

    set blifName($list:selectionDirection) 0
}

# Procedure: SelectOrPaintSignalFromCoords
proc SelectOrPaintSignalFromCoords {list color w x y {add 0}} {
    global blifName

    set char [$w get "@$x,$y"]

    set startLine  [$w index "@$x,$y linestart"]
    set endLine    [$w index "@$x,$y lineend"]
    set name       [$w get $startLine $endLine]

    if {$name == "" || [string first $char $name] == -1} {
        set blifName($list:selectionStart) 0
        set blifName($list:selectionLast) 0
        set blifName($list:selectionDirection) 0
        UnselectAll $list
        update
        return
    }

    if {$blifName($list:Mode) == "selection"} {
        set verif      $blifName(verification)
        set signalProp $blifName($verif:$list:$name)
        set selected   [lindex $signalProp 3]

        set blifName($list:selectionStart) $startLine
        set blifName($list:selectionLast) $startLine
        if {$add == 0} {
            set wereSelected [expr [llength [$w tag ranges selected]]/2]
            UnselectAll $list
            if {$wereSelected > 1} {
                $w tag add selected $startLine $endLine
                set blifName($verif:$list:$name) \
                    [lreplace $blifName($verif:$list:$name) 3 3 1]
                return
            }
        }
        if {$selected == 0} {
            $w tag add selected $startLine $endLine
        } {
            $w tag remove selected $startLine $endLine
        }
        set blifName($verif:$list:$name) \
            [lreplace $blifName($verif:$list:$name) \
                 3 3 [expr ($selected+1)%2]]
    } {
        PaintSignalFromSignalName $list $name $color
    }
}

# Procedure: ShiftSelectOrPaintSignalFromCoords
proc ShiftSelectOrPaintSignalFromCoords {list color w x y } {
    global blifName
    
    set char [$w get "@$x,$y"]

    set startLine  [$w index "@$x,$y linestart"]
    set endLine    [$w index "@$x,$y lineend"]
    set name       [$w get $startLine $endLine]

    if {$name == "" || ($blifName($list:selectionStart) == 0 && 
                        [string first $char $name] == -1)} {
        if {[$w tag ranges selected] == {}} {
            set blifName($list:selectionStart) 0
            set blifName($list:selectionLast) 0
            set blifName($list:selectionDirection) 0
            UnselectAll $list
            update
        }
        return
    }

    set verif      $blifName(verification)
    set signalList $blifName($verif:$list:$name)
    set selected   [lindex $signalList 3]

    if {$blifName($list:Mode) == "selection"} {
        set tag selected
        set index 3
        set value 1
    } {
        set tag $color
        set index 0
        set value $color
    }
    if {$blifName($list:Mode) == "selection"} {
        if {$blifName($list:selectionStart) == 0} {
            set blifName($list:selectionStart) $startLine
            set blifName($list:selectionLast) $startLine
        }
        if {$blifName($list:selectionStart) == $startLine} {
            $w tag add selected $startLine $endLine
            set blifName($verif:$list:$name) \
                [lreplace $blifName($verif:$list:$name) 3 3 1]
        } {
            SelectFromStartToLast $w $list $blifName($list:selectionStart) \
                $startLine
        }
    } {
        PaintSignalFromSignalName $list $name $color
    }
    update
}

# Procedure: MotionSelectOrPaintSignalFromCoords
proc MotionSelectOrPaintSignalFromCoords {list color w x y {add 0}} {
    global blifName
    
    set char [$w get "@$x,$y"]

    set startLine  [$w index "@$x,$y linestart"]
    set endLine    [$w index "@$x,$y lineend"]
    set name       [$w get $startLine $endLine]

    if {$name == "" || ($blifName($list:selectionStart) == 0 && 
                        [string first $char $name] == -1)} {
        if {[$w tag ranges selected] == {}} {
            set blifName($list:selectionStart) 0
            set blifName($list:selectionLast) 0
            set blifName($list:selectionDirection) 0
            UnselectAll $list
            update
        }
        return
    }

    set verif      $blifName(verification)
    set signalList $blifName($verif:$list:$name)
    set selected   [lindex $signalList 3]

    if {$blifName($list:Mode) == "selection"} {
        set blifName($list:selectionLast) $startLine

        if {$blifName($list:selectionStart) == 0 || $add != 0} {
            set blifName($list:selectionStart) $startLine
        }
        if {$startLine < $blifName($list:selectionStart)} {
            set blifName($list:selectionDirection) -1
        } elseif {$startLine > $blifName($list:selectionStart)} {
            set blifName($list:selectionDirection) 1
        } else {
            set blifName($list:selectionDirection) 0
        }
        if {$blifName($list:selectionDirection) == 0} {
            $w tag add selected $startLine $endLine
            set blifName($verif:$list:$name) \
                [lreplace $blifName($verif:$list:$name) 3 3 1]
        } {
            SelectFromStartToLast $w $list $blifName($list:selectionStart) \
                $blifName($list:selectionLast) $add
        }
    } {
        PaintSignalFromSignalName $list $name $color
    }
    update
}

# Procedure: SelectFromStartToLast
proc SelectFromStartToLast {w list start last {add 0}} {
    global blifName

    if {$start < $last} {
        set from $start
        set to   $last
    } {
        set from $last
        set to   $start
    }

    set verif $blifName(verification)

    if {$add == 0} {
        set oldSelectedList [$w tag ranges selected]
        for {set i 0} {$i < [expr [llength $oldSelectedList]/2]} {incr i} {
            set sl [lindex $oldSelectedList [expr 2*$i]]
            set el [lindex $oldSelectedList [expr 2*$i+1]]
            
            if {$sl < $from || $sl > $to} {
                set name [$w get $sl $el]
                $w tag remove selected $sl $el
                set blifName($verif:$list:$name) \
                    [lreplace $blifName($verif:$list:$name) 3 3 0]
            }
        }
    }

    set i $from
    while {$i  <= $to} {
        set j [$w index "$i lineend"]
        $w tag add selected $i $j
        set name [$w get $i $j]
        set blifName($verif:$list:$name) \
            [lreplace $blifName($verif:$list:$name) 3 3 1]
        
        set i [expr $i + 1]
    }
    update
}

# Procedure: PaintSignalFromSignalName
proc PaintSignalFromSignalName {list name color} {
    global blifName
    global symbolicName

    set w $symbolicName($list)
    set verif $blifName(verification)
    set signalProp $blifName($verif:$list:$name)
    set startLine [lindex $signalProp 1]
    set endLine   [lindex $signalProp 2]

    foreach tag [$w tag names $startLine] {
        $w tag remove $tag $startLine $endLine
    }

    $w tag add $color $startLine $endLine
    set blifName($verif:$list:$name) \
        [lreplace $blifName($verif:$list:$name) 0 0 $color]

    update
}

# Procedure: PaintSelectedSignalsInColor
proc  PaintSelectedSignalsInColor {type color} {
    global blifName
    global symbolicName

    set list ${type}List
    set w $symbolicName($list)
    set verif $blifName(verification)

    set selectedSignalList [TagListToSignalList ${type}List selected]

    foreach signal $selectedSignalList {
        set signalProp $blifName($verif:$list:$signal)
        set oldColor   [lindex $signalProp 0]
        set startLine  [lindex $signalProp 1]
        set endLine    [lindex $signalProp 2]

        # $w tag remove selected  $startLine $endLine
        $w tag remove $oldColor $startLine $endLine
        $w tag add    $color    $startLine $endLine

        set blifName($verif:$list:$signal) [list $color $startLine $endLine 1]
    }

    update
}

# Procedure: SelectSignalFromCoords
proc SelectSignalFromCoords {list color w x y} {
    global blifName

    set startLine [$w index "@$x,$y linestart"]
    set endLine   [$w index "@$x,$y lineend"]

    set verif $blifName(verification)

    set signal [$w get $startLine $endLine]
    set signalProp $blifName($verif:$list:$signal)

    foreach tag [$w tag names @$x,$y] {
        $w tag remove $tag $startLine $endLine
    }

    $w tag add $color $startLine $endLine
    set signal [$w get $startLine $endLine]


    set blifName($verif:$list:$signal) [list $color $startLine $endLine]

    update
}

# Procedure: SelectSignalFromSignalName
proc SelectSignalFromSignalName {list color signal} {
    global blifName
    global symbolicName

    set w $symbolicName($list)

    set verif $blifName(verification)

    set startLine [lindex $blifName($verif:$list:$signal) 1]
    set endLine   [lindex $blifName($verif:$list:$signal) 2]

    foreach tag [$w tag names $startLine] {
        $w tag remove $tag $startLine $endLine
    }

    $w tag add $color $startLine $endLine

    set blifName($verif:$list:$signal) [list $color $startLine $endLine]

    update
}

# Procedure: TagListToSignalList
proc TagListToSignalList {type tag} {
    global symbolicName

    set indexList [$symbolicName($type) tag ranges $tag]
    set sigList ""
    for {set i 0} {$i <[expr [llength $indexList]/2]} {incr i} {
        lappend sigList  [$symbolicName($type) get [lindex $indexList [expr 2*$i]]  [lindex $indexList [expr 2*$i + 1]]]
    }
    return $sigList
}


# ***************************************************************************
# * Message Manipulation Procedures
# ***************************************************************************
# Procedures: Error
proc Error {msg {w .}} {
    global alertBox

    tk_messageBox -icon error -type ok -message $msg -parent $w
}

proc FatalError {msg} {
    global alertBox

    catch {destroy .checkoutput}
    catch {destroy .reduce}
    catch {destroy .advanced}
    wm withdraw .
    update
    tk_messageBox -icon error -type ok -message $msg
    abort_xeve
    exit 1
}

proc Warning {msg {w .}} {
    global alertBox

    tk_messageBox -icon warning -parent $w -type ok -message $msg
}


proc YesNoQuestion {msg {w .}} {

    set reply [tk_messageBox -icon question -parent $w \
            -type yesno -message $msg]
    if ![string compare $reply "no"] {
        return 1
    }
    return 0
}


proc Message {msg wait args} {
    global symbolicName

    catch {destroy .message}

    toplevel .message -class Message -width 200
    message .message.msg -aspect 1500 \
        -text $msg -anchor e

    set result ""
    if {[llength $args] > 0} {
        frame .message.buttons
        set i 0
        foreach arg $args {
            if {$arg == ""} {
                continue
            }
            set but [lindex $arg 0]
            if {[llength $arg] > 1} {
                button .message.buttons.b$i -text $but \
                    -command [lindex $arg 1]
            } {
                button .message.buttons.b$i -text $but \
                    -command "set result $i; destroy .message"
            }
            pack .message.buttons.b$i -side left -expand 1 \
                    -ipadx 1m -ipady 2m
            incr i
        }
        pack .message.buttons -side bottom -fill x
    }
    pack .message.msg -side top -expand 1 -fill both -ipadx 5m -ipady 3m

    wm withdraw .message
    update idletasks
    wm transient .message .
    wm group .message .

    set x [expr [winfo screenwidth .message]/2 - \
            [winfo reqwidth .message]/2 \
            - [winfo vrootx [winfo parent .message]]]
    set y [expr [winfo screenheight .message]/2 - \
            [winfo reqheight .message]/2 \
            - [winfo vrooty [winfo parent .message]]]
    wm geom .message +$x+$y

    wm title .message "MESSAGE"
    wm deiconify .message
    if {[llength $args] > 0 && $wait} {
        tkwait window .message
    }
    return $result
    update
}

proc DestroyMessage {} {

    catch {destroy .message}
}

proc OnLineInfo {info} {
    global onLineHelp
    global blifName

    if {$blifName(Beginner) == 0} {
        catch {destroy .message}
        return
    }

    if {$info == ""} {
        set info $blifName(Beginner:Tip)
    }
    set butPrev ""
    set butNext ""
    if {[info exists onLineHelp($info:previousTip)] != 0} {
        set butPrev \
            [list "Previous Tip" "OnLineInfo $onLineHelp($info:previousTip)"]
    }
    if {[info exists onLineHelp($info:nextTip)] != 0} {
        set butNext \
            [list "Next Tip" "OnLineInfo $onLineHelp($info:nextTip)"]
    }
    Message $onLineHelp($info) 0 "$butPrev" "$butNext" "Dismiss"

    update
}


# ***************************************************************************
# * Verification Function Procedures
# ***************************************************************************
# Procedure: Verify
proc Verify {} {
    global blifName
    global symbolicName

    if {$blifName(selectedFile) == ""} {
        Error "No FSM in current context"
        return
    }

    DisableButtons

    set signalArray(inputList) [TagListToSignalList inputList #a5a5a5]
    set signalArray(input0List) [TagListToSignalList inputList #0000ff]
    set signalArray(input1List) [TagListToSignalList inputList #ff0000]
    set signalArray(outputList) [TagListToSignalList outputList #a5a5a5]
    set signalArray(output0List) [TagListToSignalList outputList #0000ff]
    set signalArray(output1List) [TagListToSignalList outputList #ff0000]

    if {![string compare $blifName(verification) "reduce"]} {
        FsmMinimize signalArray
    } {
        CheckOutputs signalArray
    }
}


# Procedure: CheckOutputs
proc CheckOutputs {signalArray} {
    global blifName

    upvar $signalArray data

    set blifName(CurrentResultPanel) .checkoutput

    set blifName(Beginner:Tip) CheckOutput
    OnLineInfo CheckOutput

    SendCommand "check_outputs [list $data(inputList)]\
            [list $data(input0List)] [list $data(input1List)]\
            [list $data(outputList)] [list $data(output0List)]\
            [list $data(output1List)]"
}

# Procedure: FsmMinimize
proc FsmMinimize {signalArray} {
    global blifName
    global alertBox
    global symbolicName
    global resultName

    upvar $signalArray data

    set signalString "I:$data(inputList) I0:$data(input0List)\
            I1:$data(input1List) O:$data(outputList) O0:$data(output0List)\
            O1:$data(output1List)"

    if {[info exists resultName($signalString,Classes)]} {
        set msg "Computation registered as already done. Restore the results ?"
        set answer\
                [tk_messageBox -message $msg -icon question -type yesnocancel]

        case $answer {
            yes {
                set blifName(CurrentResultPanel) .reduce
                DisplayReduce
                set w .reduce
                $w$symbolicName(AbortButton) configure -state disabled
                set states $resultName($signalString,States)
                set mini $resultName($signalString,Classes)
                set blifName(SavedFc2File) $resultName($signalString,Fc2File)
                DisplayStateSizes $states
                DisplayEquivalenceSizes $mini
                EnableButtons
                # EnableSignalLists
                update
                return
            }
            no { }
            cancel {
                EnableButtons
                # EnableSignalLists
                return
            }
        }
    }
    if {[GetFc2FileName] == 0} {
        EnableButtons
        # EnableSignalLists
        return
    }
    if {$blifName(SavedFc2File) != ""} {
        ResetReducePanel
        set blifName(CurrentResultPanel) .reduce

        set blifName(Beginner:Tip) Reduce
        OnLineInfo Reduce

        SendCommand "fsm_minimize [list $data(inputList)]\
            [list $data(input0List)] [list $data(input1List)]\
            [list $data(outputList)] [list $data(output0List)]\
            [list $data(output1List)] $blifName(SavedFc2File)"

    }
}

proc SetCheckOutputList {list0 list1} {
    global symbolicName
    global blifName

    set w .checkoutput

    set blifName(CheckOutputList) "$list0 $list1"

    $w.frame5.signals delete 0 end
    set i 0
    foreach sig $list1 {
        $w.frame5.signals insert end $sig
        set blifName($sig,index) $i
        set blifName($sig,checked) 0
        set blifName($sig,status) none
        set blifName($sig,file) none
        set blifName($sig,goal) 1
        incr i
    }
    foreach sig $list0 {
        $w.frame5.signals insert end $sig
        set blifName($sig,index) $i
        set blifName($sig,checked) 0
        set blifName($sig,status) none
        set blifName($sig,file) none
        set blifName($sig,goal) 0
        incr i
    }

    update
}

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

    set w .checkoutput
    $w$symbolicName(CheckOutputList) delete 0 end
    $w$symbolicName(CheckOutputName) configure -text ""
    $w$symbolicName(CheckOutputFile) configure -text ""
    $w$symbolicName(CheckOutputStatus) configure -text ""
    foreach sig $blifName(CheckOutputList) {
        unset blifName($sig,file) blifName($sig,index) \
            blifName($sig,checked) blifName($sig,status) \
            blifName($sig,goal)
    }
    set blifName(CheckOutputList) {}
}

# Procedure: ReachableStates
proc ReachableStates {} {
    global blifName

    if {$blifName(selectedFile) == ""} {
        Error "No FSM in current context"
        return
    }

    set blifName(CurrentResultPanel) .reachable_states

    DisableButtons

    SendCommand "reachable_states"
}

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

    if {$blifName(preverif) == $blifName(verification)} {
        return
    }
    set blifName(preverif) $blifName(verification)
    ChangePaletteHelp
    RestoreSignalColors
}

# Procedure: AdvancedCheck
proc AdvancedCheck {} {
    global optionModality
    global optionProperty
    global symbolicName
    global blifName

    if {$blifName(selectedFile) == ""} {
        Error "No FSM in current context"
        return
    }

    set w .advanced

    DisableButtons

    set signalArray(inputList) [TagListToSignalList inputList \#a5a5a5]
    set signalArray(input0List) [TagListToSignalList inputList \#0000ff]
    set signalArray(input1List) [TagListToSignalList inputList \#ff0000]
    set signalArray(outputList) [TagListToSignalList outputList \#a5a5a5]
    set signalArray(output0List) [TagListToSignalList outputList \#0000ff]
    set signalArray(output1List) [TagListToSignalList outputList \#ff0000]

    $symbolicName(AdvancedCheckButton) configure -state disabled
    $w$symbolicName(AbortButton) configure -state normal
    $w$symbolicName(WhatMsg) configure -text ""
    $w$symbolicName(EndMsg) configure -text ""
    $w$symbolicName(Dismiss) configure -state disabled
    update

    set blifName(CurrentResultPanel) .advanced
    set inputList {}
    set outputList {}
    set iolist "I:$inputList O:$outputList"
    set option "$optionModality $optionProperty"
    if {[info exists resultName($iolist,$option)]} {
        $symbolicName(AdvancedCheckResult) configure \
                -text $resultName($iolist,$option)
        return
    }
    set opt ""
    switch -exact $option {
        "Can Terminate" {
            set opt "can exit"
        }
        "Must Terminate" {
            set opt "must exit"
        }
        "Can Idle Forever" {
            set opt "can idle"
        }
        "Must Idle Forever" {
            set opt "must idle"
        }
        default { EndOfAdvancedCheck }
    }
    SendCommand "fsm_prop $opt [list $signalArray(inputList)]\
            [list $signalArray(input0List)] [list $signalArray(input1List)]\
            [list $signalArray(outputList)] [list $signalArray(output0List)]\
            [list $signalArray(output1List)]"

    EndOfAdvancedCheck
    
}

# Procedure: SetAdvancedCheckResult
proc SetAdvancedCheckResult {entry result ilist ilist0 ilist1 olist olist0 olist1} {
    global resultName

    set resultName([list I:$ilist I0:$ilist0 I1:$ilist1 O:$olist O0:$olist0 O1:$olist1],$entry) $result
    global symbolicName
    $symbolicName(AdvancedCheckResult) configure -text $result
    update
}

# Procedure: SetAdvancedCheckButton
proc SetAdvancedCheckButton {ilist olist} {
    global resultName
    global optionProperty
    global optionModality
    global symbolicName

    set option "$optionModality $optionProperty"
    if {[info exists resultName([list I:$ilist O:$olist],$option)]}{
        $symbolicName(AdvancedCheckButton) configure -state disabled
    } {
        $symbolicName(AdvancedCheckButton) configure -state normal
    }
    update
}

# Procedure: ShowAdvancedCheckResult
proc ShowAdvancedCheckResult {menu entry} {
    global resultName
    global symbolicName
    global optionModality
    global optionProperty

    set ilist {}
    set olist {}
    $symbolicName(AdvancedOption${menu}) configure -text $entry
    set option$menu $entry
    set option "$optionModality $optionProperty"
    if {[info exists resultName([list I:$ilist O:$olist],$option)]} {
        $symbolicName(AdvancedCheckResult) configure \
                -text $resultName([list I:$ilist O:$olist],$option)
    } {
        $symbolicName(AdvancedCheckResult) configure -text ""
    }
    update
}

   
# Procedure: DisplayStateSizes
proc DisplayStateSizes {states} {
    global symbolicName
    global blifName
    global resultName

    set w $blifName(CurrentResultPanel)
    set resultName(ReachableStates) $states

    set blifName(fsm:stat:states) $states

    RefreshFsmStats

    if {[winfo exists $w]} {
        $w$symbolicName(ReachableStates) configure -text $states
        update
    }
}

# Procedure: DisplayEquivalenceSizes
proc DisplayEquivalenceSizes {states} {
    global symbolicName

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

# Procedure: SetTgrTraceFlags
proc SetTgrTraceFlags {} {
    global blifName

    if {$blifName(ReachableTrace) == 0} {
        SendCommand "set_tgr_flags 0"
    } else {
        SendCommand "set_tgr_flags 12"
    }
}

# Procedure: EndOfReachableStates
proc EndOfReachableStates {} {
    global symbolicName

    set w .reachable_states
    if {[winfo exists $w]} {
        $w$symbolicName(AbortButton) configure -state disabled
        $w$symbolicName(Dismiss) configure -state normal
        $w$symbolicName(WhatMsg) configure -text "Execution complete"
        update
    }
    EnableButtons
}

# Procedure: EndOfCheckOutput
proc EndOfCheckOutput {} {
    global symbolicName

    set w .checkoutput
    if {[winfo exists $w]} {
        $w$symbolicName(AbortButton) configure -state disabled
        $w$symbolicName(WhatMsg) configure -text "Execution complete"
        $w$symbolicName(EndMsg) configure -text \
                "`.esi' generated files (if any) can be simulated\
                using \"xes\""
        update
    }
    EnableButtons
    EnableSignalSelection
}

# Procedure: EndOfAdvancedCheck
proc EndOfAdvancedCheck {} {
    global symbolicName

    set w .advanced
    if {[winfo exists $w]} {
        $symbolicName(AdvancedCheckButton) configure -state normal
        $w$symbolicName(AbortButton) configure -state disabled
        $w$symbolicName(Dismiss) configure -state normal
        $w$symbolicName(WhatMsg) configure -text "Execution complete"
        $w$symbolicName(EndMsg) configure -text "If result is \"Yes\",\
                click on \"Save Path\" to save an example of execution path"
        update
    }
    EnableButtons
    EnableSignalSelection
}

# Procedure: EndOfReduction
proc EndOfReduction {inputList input0List input1List outputList
         output0List output1List} {
    global symbolicName
    global blifName
    global resultName

    set w .reduce
    if {[winfo exists $w]} {
        set signalString "I:$inputList I0:$input0List I1:$input1List\
                O:$outputList O0:$output0List O1:$output1List"

        set resultName($signalString,States) \
            [$w$symbolicName(ReachableStates) cget -text]
        set resultName($signalString,Classes) \
            [$w$symbolicName(MinimizedStates) cget -text]
        set resultName($signalString,Fc2File) $blifName(SavedFc2File)
        $w$symbolicName(AbortButton) configure -state disabled
        $w$symbolicName(WhatMsg) configure -text "Execution complete"
        update
        if {$blifName(SavedFc2File) != ""} {
            $w$symbolicName(EndMsg) configure -text \
                "Result generated in fc2 file \"$blifName(Fc2File)\".\n\
                You can explore the FSM graphically invoking Atg (Draw\
                Automaton Button bellow)"
            if {$blifName(AtgExists) == 1} {
                $w$symbolicName(DrawAutomaton) configure -state normal
            } {
                if {[info exists blifName(AtgWarning)] == 0 ||
                $blifName(AtgWarning) != 1} {
                    if {[YesNoQuestion \
                            "Could not find any atg to execute in your PATH.\
                            Can not set on the \"Draw Automaton\" button.\
                            Do you want this message to be displayed\
                            next time ?"] == 1} {
                        set blifName(AtgWarning) 1
                    }
                }
            }
            update
        }
        $w$symbolicName(Dismiss) configure -state normal
        update
    }
    EnableButtons
    EnableSignalSelection
}

# Procedure: DrawAutomaton
proc DrawAutomaton {fc2file} {
    global symbolicName
    global blifName

    set w .reduce
    $w$symbolicName(DrawAutomaton) configure -state disabled
    update
    if {$blifName(AtgCallNumber) > 0} {
        if {[YesNoQuestion "ATG has already been called\
                $blifName(AtgCallNumber) time(s). If still running,\ you can\
                load your fc2 file using its File menu.\
                Call a new ATG anyway?"]==0} {
            SendCommand "call_atg $fc2file"
            incr blifName(AtgCallNumber)
        }
    } {
        # catch {exec atg $fc2file &}
        SendCommand "call_atg $fc2file"
        incr blifName(AtgCallNumber)
    }

    set blifName(Beginner:Tip) DrawFc2File
    OnLineInfo DrawFc2File

    update
}


# ***************************************************************************
# * Xeve Initialisation Procedures
# ***************************************************************************
# Prompt for interactive session
set tcl_prompt1 Prompt
set tcl_prompt2 Prompt
proc Prompt { } { puts "xeve% " }


# Xeve GUI startup procedure
XeveStartUp
