#  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 MENU
global MENUITEMS
global MENUBG
global MENUFG

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

$MENUVERSIS add command  -command menu_versis_compose -label "versis_compose"
$MENUVERSIS add command  -command menu_versis_composeStep -label "versis_compose_step"
$MENUVERSIS add separator
$MENUVERSIS add command  -command menu_versis_strongEquivalence -label "versis_strong_equivalence"
$MENUVERSIS add command  -command menu_versis_weakEquivalence -label "versis_weak_equivalence"
$MENUVERSIS add command  -command menu_versis_testingEquivalence -label "versis_testing_equivalence"
$MENUVERSIS add command  -command menu_versis_traceEquivalence -label "versis_trace_equivalence"
$MENUVERSIS add separator
$MENUVERSIS add command  -command menu_versis_strongMinimization -label "versis_strong_minimization"
$MENUVERSIS add command  -command menu_versis_weakMinimization -label "versis_weak_minimization"
$MENUVERSIS add command  -command menu_versis_traceMinimization -label "versis_trace_minimization"
$MENUVERSIS add command  -command menu_versis_wcaMinimization -label "versis_wca_minimization"
$MENUVERSIS add separator
$MENUVERSIS add command  -command menu_versis_changeRename -label "versis_change_rename"
$MENUVERSIS add command  -command menu_versis_changeHide -label "versis_change_hide"
$MENUVERSIS add command  -command menu_versis_changeForbid -label "versis_change_forbid"
$MENUVERSIS add command  -command menu_versis_checkDeadlock -label "versis_check_deadlock"
$MENUVERSIS add command  -command menu_versis_checkDivergence -label "versis_check_divergence"
$MENUVERSIS add separator
$MENUVERSIS add command  -command versis_about -label "versis_about"

lappend MENUITEMS $MENUVERSIS
refresh

proc versis_about {  } {
    global BINDIR

    outline ""
    outline "\#\#\# "
    out "\# "
    versis_aboutPkg

    set OK ""
    if {[file isfile "/usr/lib/est2ed/versis.about"]} {
      set OK "OK"
      set f [open "/usr/lib/est2ed/versis.about" r]
    } else {
      if {[file isfile "$BINDIR/versis.about"]} {
        set OK "OK"
        set f [open "$BINDIR/versis.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
#
# ##########################################################

global BROWSETYPE

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

proc comtypeBrowse {  } {
  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 " \
    {<0> CCS composition} \
    {<1> CCS composition specifying allowed actions} \
    {<2> CCS composition specifying restricted actions} \
    {<3> multi-way composition} \
    {<4> multi-way composition specifying allowed actions} \
    {<5> multi-way composition specifying restricted actions} \
    {<6> fundamental-mode multi-way composition} \
    {<7> fundamental-mode multi-way composition specifying allowed actions} \
    {<8> fundamental-mode multi-way composition specifying restricted actions} \
  "

  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 false -relief solid -anchor w -padx 5
  $menu configure -borderwidth 1 -font MENUFONT -activeborderwidth 1 -activebackground #ffffc0 -activeforeground #000040 -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_versis_compose {  } {
    global NAME
    global SYNOPSIS
    global SYNTAX
    global EXAMPLE
    global EXPLANATION
    global BROWSE
    global CMD
    global CMDEND

    set NAME "versis_compose"
    set SYNOPSIS "Compose processes."
    set SYNTAX "comtype%d pname%s plist%s alist%s"
    set EXAMPLE "versis_compose 1 c \"p1 p2\" \"a1\""
    set EXPLANATION "Compose proceses p1 and p2, a1 is the only non-restricted action"
    set BROWSE [list \
        {comtype "Select composition type" ""} \
        {nonempty "Composition name" 30} \
        {list "Select list of processes" proc} \
        {required "List of action names" 30} \
        {optional "On-the-fly \[0/1\] (optional)" 10 ""} \
    ]

    set CMD $NAME
    set CMDEND ""

    commonDialog
}

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

    set NAME "versis_compose_step"
    set SYNOPSIS "Initialize or calculate N steps of parallel composition."
    set SYNTAX "cname%s N%d"
    set EXAMPLE "versis_compose_step c N"
    set EXPLANATION "Calculate N steps (N = 0 means initialization)"
    set BROWSE [list \
        {name "Select composition" comp} \
        {nonempty "Number of steps" 30} \
    ]

    set CMD $NAME
    set CMDEND ""

    commonDialog
}

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

    set NAME "versis_strong_equivalence"
    set SYNOPSIS "Checking strong observational equivalence."
    set SYNTAX "ptype%d pname%s ptype%d pname%s"
    set EXAMPLE "versis_strong_equivalence 0 p 1 c"
    set EXPLANATION "Checking strong equivalence between proces p and composition c"
    set BROWSE [list \
        {name "Select first process/composition" proccomp} \
        {name "Select second process/composition" proccomp} \
    ]

    set CMD $NAME
    set CMDEND ""

    commonDialog
}

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

    set NAME "versis_weak_equivalence"
    set SYNOPSIS "Checking weak observational equivalence."
    set SYNTAX "ptype%d pname%s ptype%d pname%s"
    set EXAMPLE "versis_weak_equivalence 0 p 1 c"
    set EXPLANATION "Checking weak equivalence between proces p and composition c"
    set BROWSE [list \
        {name "Select first process/composition" proccomp} \
        {name "Select second process/composition" proccomp} \
    ]

    set CMD $NAME
    set CMDEND ""

    commonDialog
}

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

    set NAME "versis_testing_equivalence"
    set SYNOPSIS "Checking testing equivalence."
    set SYNTAX "ptype%d pname%s ptype%d pname%s"
    set EXAMPLE "versis_testing_equivalence 0 p 1 c"
    set EXPLANATION "Checking testing equivalence between proces p and composition c"
    set BROWSE [list \
        {name "Select first process/composition" proccomp} \
        {name "Select second process/composition" proccomp} \
    ]

    set CMD $NAME
    set CMDEND ""

    commonDialog
}

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

    set NAME "versis_trace_equivalence"
    set SYNOPSIS "Checking trace equivalence."
    set SYNTAX "ptype%d pname%s ptype%d pname%s"
    set EXAMPLE "versis_trace_equivalence 0 p 1 c"
    set EXPLANATION "Checking trace equivalence between proces p and composition c"
    set BROWSE [list \
        {name "Select first process/composition" proccomp} \
        {name "Select second process/composition" proccomp} \
    ]

    set CMD $NAME
    set CMDEND ""

    commonDialog
}

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

    set NAME "versis_strong_minimization"
    set SYNOPSIS "Creating minimal strong equivalent process"
    set SYNTAX "ptype%d pname%s"
    set EXAMPLE "versis_strong_minimization 1 c"
    set EXPLANATION "Creating minimal process which is strong equivalent to composition c"
    set BROWSE [list \
        {name "Select process/composition" proccomp} \
    ]

    set CMD $NAME
    set CMDEND ""

    commonDialog
}

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

    set NAME "versis_weak_minimization"
    set SYNOPSIS "Creating minimal weak equivalent process"
    set SYNTAX "ptype%d pname%s"
    set EXAMPLE "versis_weak_minimization 1 c"
    set EXPLANATION "Creating minimal process which is weak equivalent to composition c"
    set BROWSE [list \
        {name "Select process/composition" proccomp} \
    ]

    set CMD $NAME
    set CMDEND ""

    commonDialog
}

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

    set NAME "versis_trace_minimization"
    set SYNOPSIS "Creating minimal trace equivalent process"
    set SYNTAX "ptype%d pname%s"
    set EXAMPLE "versis_trace_minimization 1 c"
    set EXPLANATION "Creating minimal process which is trace equivalent to composition c"
    set BROWSE [list \
        {name "Select process/composition" proccomp} \
    ]

    set CMD $NAME
    set CMDEND ""

    commonDialog
}

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

    set NAME "versis_wca_minimization"
    set SYNOPSIS "Remove duplicated paths from generated WCA"
    set SYNTAX "0 pname%s"
    set EXAMPLE "versis_wca_minimization 0 wc1"
    set EXPLANATION "Creating automaton from WCA wc1"
    set BROWSE [list \
        {name "Select process/composition" proccomp} \
    ]

    set CMD $NAME
    set CMDEND ""

    commonDialog
}

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

    set NAME "versis_change_rename"
    set SYNOPSIS "Rename action in the process."
    set SYNTAX "pname%s aname%s aname%s"
    set EXAMPLE "versis_change_rename p a1 b1"
    set EXPLANATION "In process p rename action a1 to b1"
    set BROWSE [list \
        {name "Select process" proc} \
        {nonempty "Original action name" 30} \
        {nonempty "New action name" 30} \
    ]

    set CMD $NAME
    set CMDEND ""

    commonDialog
}

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

    set NAME "versis_change_hide"
    set SYNOPSIS "Hide action in the process."
    set SYNTAX "pname%s aname%s"
    set EXAMPLE "versis_change_hide p a"
    set EXPLANATION "In process p hide action a"
    set BROWSE [list \
        {name "Select process" proc} \
        {nonempty "Action name" 30} \
    ]

    set CMD $NAME
    set CMDEND ""

    commonDialog
}

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

    set NAME "versis_change_forbid"
    set SYNOPSIS "Forbid action in the process."
    set SYNTAX "pname%s aname%s"
    set EXAMPLE "versis_change_forbid p a"
    set EXPLANATION "In process p forbid action a"
    set BROWSE [list \
        {name "Select process" proc} \
        {nonempty "Action name" 30} \
    ]

    set CMD $NAME
    set CMDEND ""

    commonDialog
}

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

    set NAME "versis_check_deadlock"
    set SYNOPSIS "Check possibility of deadlock in process."
    set SYNTAX "pname%s"
    set EXAMPLE "versis_check_deadlock p"
    set EXPLANATION "Check if there exists deadlock in process p"
    set BROWSE [list \
        {name "Select process" proc} \
    ]

    set CMD $NAME
    set CMDEND ""

    commonDialog
}

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

    set NAME "versis_check_divergence"
    set SYNOPSIS "Check possibility of divergence in process."
    set SYNTAX "pname%s"
    set EXAMPLE "versis_check_divergence p"
    set EXPLANATION "Check if there exists divergent state in process p"
    set BROWSE [list \
        {name "Select process" proc} \
    ]

    set CMD $NAME
    set CMDEND ""

    commonDialog
}
