#  Authors     [Robert Meolic (meolic@uni-mb.si)]
#  Revision    [$Revision: 76 $]
#  Date        [$Date: 2013-04-26 14:26:09 +0200 (pet, 26 apr 2013) $]
#
#  Copyright   [This file is part of EST (Efficient Symbolic Tools).
#               Copyright (C) 2003, 2013
#               UM-FERI, Smetanova ulica 17, SI-2000 Maribor, Slovenia
#
#               EST is free software; you can redistribute it and/or modify
#               it under the terms of the GNU General Public License as
#               published by the Free Software Foundation; either version 2
#               of the License, or (at your option) any later version.
#
#               EST is distributed in the hope that it will be useful,
#               but WITHOUT ANY WARRANTY; without even the implied warranty of
#               MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
#               GNU General Public License for more details.
#
#               You should have received a copy of the GNU General Public
#               License along with this program; if not, write to the Free
#               Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
#               Boston, MA 02110-1301 USA.]

global diagnostic
global automaton
global explain
global minimize
global tracepath
global progress

set diagnostic 0
set explain 0
set tracepath 0
set automaton 0
set explain 0
set minimize 0
set progress 0

global MENU
global MENUITEMS
global MENUBG
global MENUFG

set MENUMC $MENU.mc
menu $MENUMC -activeborderwidth 1 -activebackground #ffffc0 -activeforeground #000040 -font MENUFONT -relief groove -borderwidth 4 -tearoff false
$MENU insert [expr [$MENU index last]] cascade -menu $MENUMC -activebackground #ffffc0 -activeforeground #000040 -font MENUFONT -label "Model checking"

$MENUMC add command  -command menu_mc_readACTL -label "mc_read_actl"
$MENUMC add command  -command menu_mc_writeACTL -label "mc_write_actl"
$MENUMC add separator
$MENUMC add command  -command menu_mc_readACTLFile -label "mc_read_actl_file"
$MENUMC add command  -command menu_mc_checkACTLFile -label "mc_check_actl_file"
$MENUMC add separator
$MENUMC add command  -command menu_mc_checkACTL -label "mc_check_actl"
$MENUMC add command  -command menu_mc_checkACTLString -label "mc_check_actl_string"
$MENUMC add separator
$MENUMC add check -label "Generate diagnostic" -variable diagnostic
$MENUMC add check -label "Explain diagnostic" -variable explain
$MENUMC add check -label "Trace complete paths" -variable tracepath
$MENUMC add separator
$MENUMC add check -label "Generate automaton" -variable automaton
$MENUMC add check -label "Explain automaton" -variable explain
$MENUMC add check -label "Minimize automaton" -variable minimize
$MENUMC add separator
$MENUMC add check -label "Show progress" -variable progress
$MENUMC add separator
$MENUMC add command  -command menu_mc_generateWCA -label "mc_generate_wca"
$MENUMC add separator
$MENUMC add command  -command mc_about -label "mc_about"

lappend MENUITEMS $MENUMC
refresh

proc mc_about {  } {
    global BINDIR

    outline ""
    outline "\#\#\# "
    out "\# "
    mc_aboutPkg

    set OK ""
    if {[file isfile "/usr/lib/est2ed/mc.about"]} {
      set OK "OK"
      set f [open "/usr/lib/est2ed/mc.about" r]
    } else {
      if {[file isfile "$BINDIR/mc.about"]} {
        set OK "OK"
        set f [open "$BINDIR/mc.about" r]
      }
    }

    if { $OK == "OK"} {
      while {[gets $f line] >= 0} {
        out "\# "
        outline $line
      }
      outline "\#\#\# "
      close $f
    }
}

# ##########################################################
# FIELD1: Initial string/value
# FIELD2: List of arguments/values (where applicable)
#
# BROWSE types defined in mi.tcl
#
# file%s        filename
# boolean%s     false or true
# term%s        list of given terminals
# optional%s    optional parameter, can be left out
# required%s    required parameter, if empty then use ""
# nonempty%s    required parameter, must not be equal to ""
#
# BROWSE types defined in paDialog.tcl
#
# name%s        sort/process/composition name
# list%s        list of sorts/processes/compositions
#
# BROWSE types defined in versisDialog.tcl
#
# comtype%d     composition type
#
# BROWSE types defined in mcDialog.tcl
#
# form%s        formula
#
# ##########################################################

global BROWSETYPE

if {[string compare [string range $tcl_patchLevel 0 2] "8.5"] == -1} {
  array set BROWSETYPE {form {{list {Select...}} {lindex $item 2} {formBrowse}}}
} else {
  dict set BROWSETYPE form {{list {Select...}} {lindex $item 2} {formBrowse}}
}

proc formBrowse {  } {
  global MENUFG
  global MENUBG
  global FIELD1
  global FIELD2
  global FIELD3
  global IFIELD
  global tcl_patchLevel

  if {[info exists FIELD3($IFIELD)]} {unset FIELD3($IFIELD)}
  set FIELD3($IFIELD) $FIELD1($IFIELD)

  set list [mc_list_formulae]

  set menu [eval tk_optionMenu .commonDialog.dialogFrame.browse.$IFIELD.field FIELD3($IFIELD) {$FIELD1($IFIELD)} $list]
  .commonDialog.dialogFrame.browse.$IFIELD.field configure -font MENUFONT -highlightthickness 0 -borderwidth 1 -indicatoron true -relief solid -anchor w -padx 5
  $menu configure -borderwidth 1 -font MENUFONT -activebackground #ffffc0 -activeforeground #000040 -activeborderwidth 1 -relief groove -tearoff 0

  if {[string compare [string range $tcl_patchLevel 0 2] "8.4"] >= 0} {
    if {![string equal [tk windowingsystem] "aqua"]} {
      .commonDialog.dialogFrame.browse.$IFIELD.field configure -foreground $MENUFG -background $MENUBG -activeforeground $MENUFG -activebackground $MENUBG
      $menu configure -foreground $MENUFG -background $MENUBG
    }
  }

  if {[string compare [string range $tcl_patchLevel 0 2] "8.4"] == -1} {
    trace variable FIELD3($IFIELD) w refreshCmd
  } else {
    trace add variable FIELD3($IFIELD) write refreshCmd
  }
}

proc menu_mc_readACTL {  } {
    global NAME
    global SYNOPSIS
    global SYNTAX
    global EXAMPLE
    global EXPLANATION
    global BROWSE
    global CMD
    global CMDEND

    set NAME "mc_read_actl"
    set SYNOPSIS "Read ACTL/ACTLW formula."
    set SYNTAX "fname%s formula%s"
    set EXAMPLE "mc_read_actl F1 \"EEF {stop!};\""
    set EXPLANATION "Read formula F1 = \"EEF {stop!}\""
    set BROWSE [list \
        {nonempty "Formula name" 60} \
        {nonempty "ACTL/ACTLW Formula" 60} \
    ]

    set CMD $NAME
    set CMDEND ""

    commonDialog
}

proc menu_mc_readACTLFile {  } {
    global NAME
    global SYNOPSIS
    global SYNTAX
    global EXAMPLE
    global EXPLANATION
    global BROWSE
    global CMD
    global CMDEND

    set NAME "mc_read_actl_file"
    set SYNOPSIS "Read ACTL/ACTLW formulae from file."
    set SYNTAX "file%s"
    set EXAMPLE "mc_read_actl_file safety.actl"
    set EXPLANATION "Read formulae from file safety.actl."
    set BROWSE [list \
        {file "Select file with ACTL/ACTLW formulae" {{{ACTL/ACTLW formulae} {.actl}}}} \
    ]

    set CMD $NAME
    set CMDEND ""

    commonDialog
}

proc menu_mc_writeACTL {  } {
    global NAME
    global SYNOPSIS
    global SYNTAX
    global EXAMPLE
    global EXPLANATION
    global BROWSE
    global CMD
    global CMDEND

    set NAME "mc_write_actl"
    set SYNOPSIS "Write ACTL/ACTLW formula."
    set SYNTAX "fname%s"
    set EXAMPLE "mc_write_actl F1"
    set EXPLANATION "Write formula F1"
    set BROWSE [list \
        {form "Select formula"} \
    ]

    set CMD $NAME
    set CMDEND ""

    commonDialog
}

proc menu_mc_checkACTL {  } {
    global NAME
    global SYNOPSIS
    global SYNTAX
    global EXAMPLE
    global EXPLANATION
    global BROWSE
    global CMD
    global CMDEND

    global diagnostic
    global automaton
    global explain
    global minimize
    global tracepath
    global progress

    set PARAM ""
    if {$diagnostic == 1} {set PARAM "$PARAM | \$mc_diagnostic"}
    if {$automaton == 1} {set PARAM "$PARAM | \$mc_automaton"}
    if {$minimize == 1} {set PARAM "$PARAM | \$mc_minimize"}
    if {$explain == 1} {set PARAM "$PARAM | \$mc_explain"}
    if {$tracepath == 1} {set PARAM "$PARAM | \$mc_tracepath"}
    if {$progress == 1} {set PARAM "$PARAM | \$mc_progress"}
    if {$PARAM != ""} {set PARAM "[string range $PARAM 3 [string length $PARAM]]"}
    if {$PARAM != ""} {set PARAM "\[expr $PARAM\]"}

    set NAME "mc_check_actl"
    set SYNOPSIS "ACTL/ACTLW model checking"
    set SYNTAX "ptype%d pname%s fname%s param%d"
    set EXAMPLE "mc_check_actl 0 P F1 simple"
    set EXPLANATION "Check ACTL/ACTLW formula F1 on process P"
    set BROWSE [list \
        {name "Select process/composition" proccomp} \
        {form "Select formula"} \
        [concat {optional "Parameter (optional)" 60} \"$PARAM\"] \
    ]

    set CMD $NAME
    set CMDEND ""

    commonDialog
}

proc menu_mc_checkACTLString {  } {
    global NAME
    global SYNOPSIS
    global SYNTAX
    global EXAMPLE
    global EXPLANATION
    global BROWSE
    global CMD
    global CMDEND

    global diagnostic
    global automaton
    global explain
    global minimize
    global tracepath
    global progress

    set PARAM ""
    if {$diagnostic == 1} {set PARAM "$PARAM | \$mc_diagnostic"}
    if {$automaton == 1} {set PARAM "$PARAM | \$mc_automaton"}
    if {$minimize == 1} {set PARAM "$PARAM | \$mc_minimize"}
    if {$explain == 1} {set PARAM "$PARAM | \$mc_explain"}
    if {$tracepath == 1} {set PARAM "$PARAM | \$mc_tracepath"}
    if {$progress == 1} {set PARAM "$PARAM | \$mc_progress"}
    if {$PARAM != ""} {set PARAM "[string range $PARAM 2 [string length $PARAM]]"}
    if {$PARAM != ""} {set PARAM "\[expr $PARAM\]"}

    set NAME "mc_check_actl_string"
    set SYNOPSIS "ACTL/ACTLW model checking"
    set SYNTAX "ptype%d pname%s formula%s param%d"
    set EXAMPLE "mc_check_actl_string 0 P \"EEF {stop!};\" simple"
    set EXPLANATION "Check ACTLW formula \"EEF {stop!}\" on process P"
    set BROWSE [list \
        {name "Select process/composition" proccomp} \
        {nonempty "ACTL/ACTLW Formula" 60} \
        [concat {optional "Parameter (optional)" 60} \"$PARAM\"] \
    ]

    set CMD $NAME
    set CMDEND ""

    commonDialog
}

proc menu_mc_checkACTLFile {  } {
    global NAME
    global SYNOPSIS
    global SYNTAX
    global EXAMPLE
    global EXPLANATION
    global BROWSE
    global CMD
    global CMDEND

    global diagnostic
    global automaton
    global explain
    global minimize
    global tracepath
    global progress

    set PARAM ""
    if {$diagnostic == 1} {set PARAM "$PARAM | \$mc_diagnostic"}
    if {$automaton == 1} {set PARAM "$PARAM | \$mc_automaton"}
    if {$minimize == 1} {set PARAM "$PARAM | \$mc_minimize"}
    if {$explain == 1} {set PARAM "$PARAM | \$mc_explain"}
    if {$tracepath == 1} {set PARAM "$PARAM | \$mc_tracepath"}
    if {$progress == 1} {set PARAM "$PARAM | \$mc_progress"}
    if {$PARAM != ""} {set PARAM "[string range $PARAM 2 [string length $PARAM]]"}
    if {$PARAM != ""} {set PARAM "\[expr $PARAM\]"}

    set NAME "mc_check_actl_file"
    set SYNOPSIS "ACTL/ACTLW model checking"
    set SYNTAX "ptype%d pname%s file%s param%d"
    set EXAMPLE "mc_check_actl_file 0 P safety.actl simple"
    set EXPLANATION "Check ACTL/ACTLW formulae in file safety.actl on process P"
    set BROWSE [list \
        {name "Select process/composition" proccomp} \
        {file "Select file with ACTL/ACTLW formulae" {{{ACTL/ACTLW formulae} {.actl}}}} \
        [concat {optional "Parameter (optional)" 60} \"$PARAM\"] \
    ]

    set CMD $NAME
    set CMDEND ""

    commonDialog
}

proc menu_mc_generateWCA {  } {
    global NAME
    global SYNOPSIS
    global SYNTAX
    global EXAMPLE
    global EXPLANATION
    global BROWSE
    global CMD
    global CMDEND

    set NAME "mc_generate_wca"
    set SYNOPSIS "Generate witness/counterexample automaton"
    set SYNTAX "pname%s fname%s aname%s"
    set EXAMPLE "mc_generate_wca P F1 WCA_P"
    set EXPLANATION "Generate automaton WCA_P for formula F1 on process P"
    set BROWSE [list \
        {name "Select process/composition" proc} \
        {form "Select formula"} \
        {nonempty "Automaton name" 30} \
    ]

    set CMD $NAME
    set CMDEND ""

    commonDialog
}
