#Author: Xiaoyu Jin
#reference: http://sebsauvage.net/python/gui/
#!/usr/bin/env python
# import GUI module
try:
    # for Python2
    from Tkinter import *
except ImportError:
    # for Python3
    from tkinter import * 
try:
    # for Python2
    import tkMessageBox
except ImportError:
    # for Python3
    import tkinter.messagebox

#process folder and file
import os

#open file with notepad
import subprocess as sp

#compare two strings
from difflib import SequenceMatcher as SM

# insert a line into a file
import fileinput
import xml.etree.ElementTree as ET
from tkinter import ttk
from tkinter import filedialog
from tkinter.filedialog import askopenfilename
import random

import sys

import re

import tkHyperlinkManager


print (sys.version)

class specToAssertion(tkinter.Tk):
    def __init__(self, parent = None):
        tkinter.Tk.__init__(self,parent)
        self.parent = parent
        self.createWidgets()
             
    def createWidgets(self):
        self.grid()
    
        ## first row
        verificationStarter = Label(self, text = '-----------------------------------------------------------------------------------------------------------------------------------------')
        verificationStarter.grid(column = 0,row = 0,columnspan = 1000,sticky = 'EW')

        
        SpecFile = Button(self,text = 'Seclect xml Specification File', command=self.openfile)
        SpecFile.grid(column = 0,row = 2,sticky = 'W')

        self.SpecFileName = StringVar()
        SpecFileNameLabel = Label(self, textvariable = self.SpecFileName, bg = 'white',width = 60)
        SpecFileNameLabel.grid(column = 10,row = 2)

        verificationStarter = Label(self, text = '----------------------------------------------------------------------------------------------------------------------------------------')
        verificationStarter.grid(column = 0,row = 3,columnspan = 1000,sticky = 'EW')


        FolderLoc = Label(self,text = "Searched Source Code Path")
        FolderLoc.grid(column = 0,row = 4,sticky = 'W')
        
        self.SourceCodePath = StringVar()
        FolderPath = Label(self, textvariable = self.SourceCodePath, bg = 'white', width = 60)
        FolderPath.grid(column = 10,row = 4,sticky = 'W')

        verificationStarter = Label(self, text = '-----------------------------------------------------------------------------------------------------------------------------------------')
        verificationStarter.grid(column = 0,row = 5,columnspan = 1000,sticky = 'EW')

        self.IOvar = IntVar()
        IOstarter = Checkbutton(self,text = "Input/Output Specifications", variable = self.IOvar)
        IOstarter.grid(column = 0,row = 6,sticky = 'W')

        self.computationVar = IntVar()        
        computationStarter = Checkbutton(self,text = "Computation Specifications", variable = self.computationVar )
        computationStarter.grid(column = 10,row = 6,sticky = 'W')

        self.constraintVar = IntVar()
        constraintStarter = Checkbutton(self,text = "Constraint Specifications", variable = self.constraintVar)
        constraintStarter.grid(column = 0,row = 10,sticky = 'W')

        self.manualErrVar = IntVar()
        manualErrStarter = Checkbutton(self,text = "Manual Mistake Specifications", variable = self.manualErrVar)
        manualErrStarter.grid(column = 10,row = 10,sticky = 'W')


        verificationStarter = Label(self, text = '-----------------------------------------------------------------------------------------------------------------------------------------')
        verificationStarter.grid(column = 0,row = 11,columnspan = 1000,sticky = 'EW')

        verificationStarter = Label(self, text = '-----------------------------------------------------------------------------------------------------------------------------------------')
        verificationStarter.grid(column = 0,row = 12,columnspan = 1000,sticky = 'EW')

        Settings = Button(self,text = "Settings", command = self.createSettingWindow)
        Settings.grid(column = 20,row = 10,sticky = 'W')

        VerifySelected = Button(self,text = "Verify", command = self.verificationTrigger)
        VerifySelected.grid(column = 30,row = 10,sticky = 'W')




        

        SpecFile = Button(self,text = 'Seclect xml validation setting file', command=self.openValidationSettingFile)
        SpecFile.grid(column = 0,row = 14,sticky = 'W')

        self.validationFileName = StringVar()
        SpecFileNameLabel = Label(self, textvariable = self.validationFileName, bg = 'white',width = 60)
        SpecFileNameLabel.grid(column = 10,row = 14)

        self.flowChartMark = 0
        self.callGraphMark = 0
        self.validatedPartMark = 0
        self.validationWindow=0
        
        #self.window = tkinter.Toplevel(height = 400, width = 600)
        #self.window.title('Validation Results')


        SpecFile = Button(self,text = 'Validated Path', command=self.showValidatedPath)
        SpecFile.grid(column = 10,row = 15,sticky = 'W')


        SpecFile = Button(self,text = 'Settings', command=self.validationSettings)
        SpecFile.grid(column = 20,row = 16,sticky = 'W')

        SpecFile = Button(self,text = 'Run and Validate', command=self.validateRun)
        SpecFile.grid(column = 30,row = 16,sticky = 'W')

        verificationStarter = Label(self, text = '-----------------------------------------------------------------------------------------------------------------------------------------')
        verificationStarter.grid(column = 0,row = 19,columnspan = 1000,sticky = 'EW')

        verificationStarter = Label(self, text = '-----------------------------------------------------------------------------------------------------------------------------------------')
        verificationStarter.grid(column = 0,row = 20,columnspan = 1000,sticky = 'EW')

        self.validationSettingFile = ''


    #######
        #####
        ##### validation part

    

    def validateRun(self):
        window = tkinter.Toplevel(height = 400, width = 600)

        text = Text(window,fg="yellow",)
        text.grid(row = 0,column = 1, columnspan = 30, sticky = "W")

        hyperlink = tkHyperlinkManager.HyperlinkManager(text)

        def click1():
            self.procedure = '3-Procedure1.c'
            self.verificationTrigger2()

        
        def click2():
            table = tkinter.Toplevel(height = 400, width = 600)
            table.title('Procedure1')

            b = Entry(table, width = 30,font = "Helvetica 12 bold")
            b.insert(0,"Specification")
            b.grid(row=0, column=1)
            b = Entry(table, width = 25,font = "Helvetica 12 bold")
            b.insert(0,"Validation")
            b.grid(row=0, column=2)
            b = Entry(table, width = 25,font = "Helvetica 12 bold")
            b.insert(0,"Verification")
            b.grid(row=0, column=4)
            b = Button(table,text = "Failed Cases",  command=self.showFailedCases,width = 20,font = "Helvetica 12 bold")
            #b.insert(0,"Failed Cases")
            b.grid(row=2, column=6)

            
            b = Text(table, height = 4, width = 30,font = "Helvetica 12 bold")
            b.insert(INSERT,'Computation: b*b - 4 * a * c >= 0')
            b.grid(row=1, column=1,rowspan = 3)
            b = Text(table,height = 4, width = 25,font = "Helvetica 12 bold")
            b.insert(INSERT,"Pass")
            b.grid(row=1, column=2,rowspan = 3)
            b = Text(table, height = 4,width = 25,font = "Helvetica 12 bold")
            b.insert(INSERT,"Fail: 10% nan")
            b.grid(row=1, column=4,rowspan = 3)

        text.insert(INSERT, "Procedure1\n\t",hyperlink.add(click1))
        text.tag_add("firstline", "1.0", "1.end")
        text.tag_config("firstline", background="yellow")

        text.insert(INSERT, "Procedure2\n\t", hyperlink.add(click2))
        text.tag_add("secondline", "2.1", "2.end")
        text.tag_config("secondline", background="orange")

    def showFailedCases(self):
        table = tkinter.Toplevel(height = 400, width = 600)
        table.title('Failed Cases')
        b = Text(table,width = 30,font = "Helvetica 12 bold")
        b.insert(END,"""Case1:
a:4.5
b:2.6
c:5.2

result:nan
""")
        b.grid(row=0, column=0)
        
        b = Text(table,width = 30,font = "Helvetica 12 bold")
        b.insert(END,"""Case2:
a:3.6
b:3.8
c:6.5

result:nan
""")
        b.grid(row=0, column=1)

    def showValidatedPath(self):
        window = tkinter.Toplevel(height = 400, width = 600)

        text = Text(window,fg="yellow",)
        text.grid(row = 0,column = 1, columnspan = 30, sticky = "W")

        hyperlink = tkHyperlinkManager.HyperlinkManager(text)
        

        def click1():
            table = tkinter.Toplevel(height = 400, width = 600)
            table.title('Procedure1.c')

            #table2 = tktable.Table(table, rows = 5, cols = 5)
            #table2.pack()

            b = Entry(table, width = 40,font = "Helvetica 12 bold")
            b.insert(0,"Procedure")
            b.grid(row=0, column=0)
            b = Entry(table, width = 40,font = "Helvetica 12 bold")
            b.insert(0,"Specification")
            b.grid(row=0, column=1)
            b = Entry(table, width = 25,font = "Helvetica 12 bold")
            b.insert(0,"Validation")
            b.grid(row=0, column=2)
            b = Entry(table, width = 25,font = "Helvetica 12 bold")
            b.insert(0,"Verification")
            b.grid(row=0, column=3)
            b = Entry(table, width = 15,font = "Helvetica 12 bold")
            b.insert(0,"Risk")
            b.grid(row=0, column=4)
            b = Entry(table, width = 15,font = "Helvetica 12 bold")
            b.insert(0,"Overall Risk")
            b.grid(row=0, column=5)

            b = Entry(table, width = 40,font = "Helvetica 12 bold")
            b.insert(0,"Procedure1.c")
            b.grid(row=1, column=0,rowspan = 5,ipady=35)
            
            b = Entry(table, width = 40,font = "Helvetica 12 bold")
            b.insert(0,"IO")
            b.grid(row=1, column=1)
            b = Entry(table, width = 25,font = "Helvetica 12 bold")
            b.insert(0,"Uncertain(Pass:99.5%)")
            b.grid(row=1, column=2)
            b = Entry(table, width = 25,font = "Helvetica 12 bold")
            b.insert(0,"Uncertain(Pass:45.4%)")
            b.grid(row=1, column=3)
            b = Entry(table,bg = "yellow",width = 15,font = "Helvetica 12 bold")
            b.insert(0,"Yellow")
            b.grid(row=1, column=4)

            b = Entry(table, width = 40,font = "Helvetica 12 bold")
            b.insert(0,"Computation")
            b.grid(row=2, column=1)
            b = Entry(table, width = 25,font = "Helvetica 12 bold")
            b.insert(0,"Pass")
            b.grid(row=2, column=2)
            b = Entry(table, width = 25,font = "Helvetica 12 bold")
            b.insert(0,"Pass")
            b.grid(row=2, column=3)
            b = Entry(table, bg = "green",width = 15,font = "Helvetica 12 bold")
            b.insert(0,"Green")
            b.grid(row=2, column=4)

            b = Entry(table, bg = "yellow",width = 15,font = "Helvetica 12 bold")
            b.insert(0,"Yellow")
            b.grid(row=1, column=5,rowspan = 5,ipady=35)



        text.insert(INSERT, "Procedure1\n\t",hyperlink.add(click1))
        text.tag_add("firstline", "1.0", "1.end")
        text.tag_config("firstline", background="yellow")

        def click2():
            table = tkinter.Toplevel(height = 400, width = 600)
            table.title('Procedure2')

            #table2 = tktable.Table(table, rows = 5, cols = 5)
            #table2.pack()

            b = Entry(table, width = 40,font = "Helvetica 12 bold")
            b.insert(0,"Procedure")
            b.grid(row=0, column=0)
            b = Entry(table, width = 40,font = "Helvetica 12 bold")
            b.insert(0,"Specification")
            b.grid(row=0, column=1)
            b = Entry(table, width = 25,font = "Helvetica 12 bold")
            b.insert(0,"Validation")
            b.grid(row=0, column=2)
            b = Entry(table, width = 25,font = "Helvetica 12 bold")
            b.insert(0,"Verification")
            b.grid(row=0, column=3)
            b = Entry(table, width = 15,font = "Helvetica 12 bold")
            b.insert(0,"Risk")
            b.grid(row=0, column=4)
            b = Entry(table, width = 15,font = "Helvetica 12 bold")
            b.insert(0,"Overall Risk")
            b.grid(row=0, column=5)

            b = Entry(table, width = 40,font = "Helvetica 12 bold")
            b.insert(0,"sedlib_proc_find_percent_finer")
            b.grid(row=1, column=0,rowspan = 5,ipady=35)
            
            b = Entry(table, width = 40,font = "Helvetica 12 bold")
            b.insert(0,"IO")
            b.grid(row=1, column=1)
            b = Entry(table, width = 25,font = "Helvetica 12 bold")
            b.insert(0,"Pass")
            b.grid(row=1, column=2)
            b = Entry(table, width = 25,font = "Helvetica 12 bold")
            b.insert(0,"Uncertain(Pass:94.8%)")
            b.grid(row=1, column=3)
            b = Entry(table,bg = "green",width = 15,font = "Helvetica 12 bold")
            b.insert(0,"Green")
            b.grid(row=1, column=4)

            b = Entry(table, width = 40,font = "Helvetica 12 bold")
            b.insert(0,"Computation")
            b.grid(row=2, column=1)
            b = Entry(table, width = 25,font = "Helvetica 12 bold")
            b.insert(0,"Pass")
            b.grid(row=2, column=2)
            b = Entry(table, width = 25,font = "Helvetica 12 bold")
            b.insert(0,"Fail")
            b.grid(row=2, column=3)
            b = Entry(table, bg = "orange",width = 15,font = "Helvetica 12 bold")
            b.insert(0,"Orange")
            b.grid(row=2, column=4)


            b = Entry(table, bg = "orange",width = 15,font = "Helvetica 12 bold")
            b.insert(0,"Orange")
            b.grid(row=1, column=5,rowspan = 5,ipady=35)

        text.insert(INSERT, "Procedure2\n\t", hyperlink.add(click2))
        text.tag_add("secondline", "2.1", "2.end")
        text.tag_config("secondline", background="orange")

    def openValidationSettingFile(self):
        validationFilePath = askopenfilename()
        validationFile = os.path.basename(validationFilePath)
        self.validationSettingFile = validationFile
        self.validationFileName.set(validationFile)
        self.parseValidationXML(validationFile)

    def parseValidationXML(self, validationFile):
        tree = ET.parse(validationFile)
        print (tree)
        root = tree.getroot()
        startingFile = root.tag
        
        for StartProcedure in root.iter('StartProcedure'):
            startProcedureName = StartProcedure.text
        self.findCalledProcedures(startProcedureName)

    def findCalledProcedures(self, startProcedureName):
        subFolders = next(os.walk('.'))[1]
        startProcedureName.strip()
        print (startProcedureName)
        for folder in subFolders:
            if folder == 'sed':
                for filename in os.listdir(folder):
                    if filename == startProcedureName:
                        filepath = folder + '\\' + filename
                        f = open(filepath,'r')
                        p = re.compile(r'.+\(.+\);$')
                        for line in f:
                            m = p.search(line)
                            #print (m)
                            if m:
                                print (m.group())

    def validationSettings(self):
        pass


    #######
        #####
        ##### verification part

    def frac(self, n):
        return 360.*n/1000

    #verify the four categories of specifications for a procedure
    def verificationTrigger(self):
        ##Create A New Window with Tabs
        
        window = tkinter.Toplevel(height = 400, width = 600)
        window.title('Verification Results')
        nb = ttk.Notebook(window)
        f1 = ttk.Frame(nb)   # first page, which would get widgets gridded into it
        f2 = ttk.Frame(nb)   # second page
        f3 = ttk.Frame(nb)
        f4 = ttk.Frame(nb)

        nb.pack(expand=1, fill='both')

        ## Haddle computation Verification
        if (self.computationVar.get() == 1):
            nb.add(f2, text='Computation')
            Results = Text(f2,height = 20,width = 110)
            Results.grid(column = 0,row = 0,columnspan=3,sticky = 'W')
            procedureName = self.procedure.split('.')[0]
            procedureName = procedureName.split('-')[1]

            if (procedureName == 'Procedure1'):
                Results.insert(INSERT,'Procedure: Procedure1.c\n')
                Results.insert(INSERT,'\n')
                Results.insert(INSERT,'Assertions Inserted to Source Code:\n')
                Results.insert(INSERT,'\tA1:assert(2*a != 0);\n')
                Results.insert(INSERT,'\ttemp1 = -b/(2*a);\n')
                Results.insert(INSERT,'\n')

                Results1 = Text(f2,height = 10,width = 110)
                Results1.grid(column = 0,row = 1,columnspan=3,sticky = 'W')
                Results1.insert(INSERT,'\n\n')
                Results1.insert(INSERT,'Verification Results:\n')
                Results1.tag_config("notV",background="yellow",foreground="red")
                Results1.tag_config("V",foreground="green")
                Results1.insert(INSERT,'\tA1\t\tTemporarily Verified\n',("V"))

            if (procedureName == 'Procedure2'):
                Results.insert(INSERT,'Procedure: Procedure2.c\n')
                Results.insert(INSERT,'\n')
                Results.insert(INSERT,'Assertions Inserted to Source Code:\n')
                Results.insert(INSERT,'\tA1:assert(b*b - 4 * a *c >= 0);\n')
                Results.insert(INSERT,'\ttemp2 = sqrt(b*b - 4 * a *c);\n')
                Results.insert(INSERT,'\n')

                Results1 = Text(f2,height = 10,width = 110)
                Results1.grid(column = 0,row = 1,columnspan=3,sticky = 'W')
                Results1.insert(INSERT,'\n\n')
                Results1.insert(INSERT,'Verification Results:\n')
                Results1.tag_config("notV",background="yellow",foreground="red")
                Results1.tag_config("V",foreground="green")
                Results1.insert(INSERT,'\tA1\t\tNot Verified!!!\n',("notV"))
                Results1.insert(INSERT,'\t\t\t Failure Condition: \n',("notV"))
                Results1.insert(INSERT,'\t\t\t\t a: 4.5\n',("notV"))
                Results1.insert(INSERT,'\t\t\t\t b: 2.2\n',("notV"))
                Results1.insert(INSERT,'\t\t\t\t c: 5.6\n',("notV"))

        if (self.IOvar.get() == 1):
            nb.add(f1, text='Input/Output')
            Results = Text(f1,height = 12,width = 80,font = 30)
            Results.grid(column = 0,row = 0,columnspan=12,sticky = 'EW')
            procedureName = self.procedure.split('.')[0]
            procedureName = procedureName.split('-')[1]
            
            Results.tag_config("Emphasize",background="yellow")

            if (procedureName == 'Procedure1'):
                Results.insert(INSERT,'Procedure: Procedure1.c\n')
                Results.insert(INSERT,'\n')
                Results.insert(INSERT,'Input Specifications:\n')
                Results.insert(INSERT,'\t 0 <a <5\n')
                Results.insert(INSERT,'\t0 < b < 90\n',("Emphasize"))

                Results.insert(INSERT,'Output Specifications:\n')
                Results.insert(INSERT,'\t0 < temp1 < 1\n')
                Results.insert(INSERT,'In-Range Input -------> In-Range Output:\n')
                Results.insert(INSERT,'\tStatistical Results of 1000 Tests(see below):\n')

                blank = Label(f1)
                blank.grid(column = 0, row = 1, columnspan = 5, sticky = 'EW')

                greenLegend = Label(f1,width = 7, bg = 'green')
                greenLegend.grid(column = 0, row = 2, sticky = 'EW')
                greenText = Label(f1, text = 'In Range (0,1)',font = 2)
                greenText.grid(column = 2, row = 2, sticky = 'W')
                
                yellowLegend = Label(f1,width = 7, bg = 'yellow')
                yellowLegend.grid(column = 0, row = 3, sticky = 'EW')
                yellowText = Label(f1, text = 'Equal to 0',font = 2)
                yellowText.grid(column = 2, row = 3, sticky = 'W')
                               
                c = Canvas(f1,width=260, height=260)
                c.grid(column = 0,row = 4,columnspan = 4, sticky = 'W')
                c.create_arc((40,40,200,200),fill="green", start=self.frac(0),extent = self.frac(948))
                Inrange = 948/1000 * 100
                c.create_text(120,88,fill="black", text = '(0, 1): '+str(Inrange)+'%', font = 2)
                c.create_arc((40,40,200,200), fill="yellow", start=self.frac(948), extent = self.frac(52))
                Outrange = 52/1000 *100
                c.create_text(200,128,fill="black", text = 'Equal to 0: '+str(Outrange)+'%', font = 2)
                #c.create_arc((2,2,98,98), fill="green", start=self.frac(400), extent = self.frac(100))

                equal0 = 52
                rangeMin = 0
                rangeMax = 0.001482
                #data = [52,900,48,0]
                #data = [20, 15, 10, 7, 5, 4, 3, 2, 1, 1, 0]
                data = [5.2, 7.3,15.2,23.5, 28.7, 20.1, 0]
                dataRange = ['       0','(0-0.0003)','(0.0003-0.0006)','(0.0006-0.0009)','(0.0009-0.0012)','(0.0012-0.0015)','(0.0015-1.0)']

                c_width = 590
                c_height = 400/2
                c2 = Canvas(f1,width=c_width, height=c_height, bg = 'white')
                c2.grid(column = 6,row = 4,columnspan = 5, sticky = 'W')
                y_stretch = 15/3
                y_gap = 20/2
                x_stretch = 70/2
                x_width = 100/2
                x_gap = 2/2
                for x, y in enumerate(data):
                    # calculate reactangle coordinates (integers) for each bar
                    x0 = x * x_stretch + x * x_width + x_gap
                    y0 = c_height - (y * y_stretch + y_gap)
                    x1 = x * x_stretch + x * x_width + x_width + x_gap
                    y1 = c_height - y_gap
                    # draw the bar
                    c2.create_rectangle(x0, y0, x1, y1, fill="blue")
                    # put the y value above each bar
                    c2.create_text(x0+10, y0, anchor=SW, text=str(y*10))
                    c2.create_text(x0-5, c_height+5, anchor=SW, text=str(dataRange[x]))

                piechartTitle = Label(f1,text = 'Pie Chart Results Distribution',font = 2)
                piechartTitle.grid(column = 0,row = 5,rowspan = 2, columnspan = 4, sticky = 'EW')

                histogramTitle = Label(f1, text = 'Histogram of Results Distribution', font = 2)
                histogramTitle.grid(column = 6, row = 5, rowspan = 2, columnspan = 5, sticky = 'EW')

                blank = Label(f1)
                blank.grid(column = 0, row = 7, columnspan = 10, sticky = 'EW')

                self.clickNumber = 1
                TestUndisiredInput = Button(f1, text = 'Undesired Input Test', font = 36, activebackground = 'blue', command = self.inputTest1)
                TestUndisiredInput.grid(column = 10,row = 8,columnspan=1,sticky = 'E')


            if (procedureName == 'Procedure2'):
                Results.insert(INSERT,'Procedure: Procedure2.c\n')
                Results.insert(INSERT,'\n')
                Results.insert(INSERT,'Input Specifications:\n')
                Results.insert(INSERT,'\t 0 <a <5\n')
                Results.insert(INSERT,'\t0 < b < 90\n',("Emphasize"))
                Results.insert(INSERT,'\t0 < c < 10\n',("Emphasize"))

                Results.insert(INSERT,'Output Specifications:\n')
                Results.insert(INSERT,'\t0 < temp2 < 2\n')
                Results.insert(INSERT,'In-Range Input -------> In-Range Output:\n')
                Results.insert(INSERT,'\tStatistical Results of 1000 Tests(see below):\n')

                blank = Label(f1)
                blank.grid(column = 0, row = 1, columnspan = 5, sticky = 'EW')

                greenLegend = Label(f1,width = 7, bg = 'green')
                greenLegend.grid(column = 0, row = 2, sticky = 'EW')
                greenText = Label(f1, text = 'In Range (0,2)',font = 2)
                greenText.grid(column = 2, row = 2, sticky = 'W')
                
                yellowLegend = Label(f1,width = 7, bg = 'yellow')
                yellowLegend.grid(column = 0, row = 3, sticky = 'EW')
                yellowText = Label(f1, text = 'Equal to 0',font = 2)
                yellowText.grid(column = 2, row = 3, sticky = 'W')
                               
                c = Canvas(f1,width=260, height=260)
                c.grid(column = 0,row = 4,columnspan = 4, sticky = 'W')
                c.create_arc((40,40,200,200),fill="green", start=self.frac(0),extent = self.frac(948))
                Inrange = 948/1000 * 100
                c.create_text(120,88,fill="black", text = '(0, 1): '+str(Inrange)+'%', font = 2)
                c.create_arc((40,40,200,200), fill="yellow", start=self.frac(948), extent = self.frac(52))
                Outrange = 52/1000 *100
                c.create_text(200,128,fill="black", text = 'Equal to 0: '+str(Outrange)+'%', font = 2)
                #c.create_arc((2,2,98,98), fill="green", start=self.frac(400), extent = self.frac(100))

                equal0 = 52
                rangeMin = 0
                rangeMax = 0.001482
                #data = [52,900,48,0]
                #data = [20, 15, 10, 7, 5, 4, 3, 2, 1, 1, 0]
                data = [5.2, 7.3,15.2,23.5, 28.7, 20.1, 0]
                dataRange = ['       0','(0-0.0003)','(0.0003-0.0006)','(0.0006-0.0009)','(0.0009-0.0012)','(0.0012-0.0015)','(0.0015-1.0)']

                c_width = 590
                c_height = 400/2
                c2 = Canvas(f1,width=c_width, height=c_height, bg = 'white')
                c2.grid(column = 6,row = 4,columnspan = 5, sticky = 'W')
                y_stretch = 15/3
                y_gap = 20/2
                x_stretch = 70/2
                x_width = 100/2
                x_gap = 2/2
                for x, y in enumerate(data):
                    # calculate reactangle coordinates (integers) for each bar
                    x0 = x * x_stretch + x * x_width + x_gap
                    y0 = c_height - (y * y_stretch + y_gap)
                    x1 = x * x_stretch + x * x_width + x_width + x_gap
                    y1 = c_height - y_gap
                    # draw the bar
                    c2.create_rectangle(x0, y0, x1, y1, fill="blue")
                    # put the y value above each bar
                    c2.create_text(x0+10, y0, anchor=SW, text=str(y*10))
                    c2.create_text(x0-5, c_height+5, anchor=SW, text=str(dataRange[x]))

                piechartTitle = Label(f1,text = 'Pie Chart Results Distribution',font = 2)
                piechartTitle.grid(column = 0,row = 5,rowspan = 2, columnspan = 4, sticky = 'EW')

                histogramTitle = Label(f1, text = 'Histogram of Results Distribution', font = 2)
                histogramTitle.grid(column = 6, row = 5, rowspan = 2, columnspan = 5, sticky = 'EW')

                blank = Label(f1)
                blank.grid(column = 0, row = 7, columnspan = 10, sticky = 'EW')

                self.clickNumber = 1
                TestUndisiredInput = Button(f1, text = 'Undesired Input Test', font = 36, activebackground = 'blue', command = self.inputTest2)
                TestUndisiredInput.grid(column = 10,row = 8,columnspan=1,sticky = 'E')

        if (self.constraintVar.get() == 1):
            nb.add(f3, text='Constraint')
            Results = Text(f3,height = 35,width = 130,font = 30)
            Results.pack()
            procedureName = self.procedure.split('.')[0]
            procedureName = procedureName.split('-')[1]
            Results.tag_config("Err",foreground="red")
            Results.tag_config("Chg",foreground="yellow")
            if (procedureName == 'Procedure1'):
                Results.insert(INSERT,'No Constraint Specification For This Procedure')
            if (procedureName == 'Procedure2'):
                Results.insert(INSERT,'No Constraint Specification For This Procedure')

        if (self.manualErrVar.get() == 1):
            nb.add(f4, text='Manual Error')
            Results = Text(f4,height = 50,width = 130,font = 30)
            Results.pack()
            Results.tag_config("Hypo",foreground="blue")
            procedureName = self.procedure.split('.')[0]
            procedureName = procedureName.split('-')[1]
            if (procedureName == 'Procedure1'):
                Results.insert(INSERT,'No Manual Mistake Found For this Procedure')
            if (procedureName == 'Procedure2'):
                Results.insert(INSERT,'No Manual Mistake Found For this Procedure')

    def verificationTrigger2(self):
        ##Create A New Window with Tabs
        
        window = tkinter.Toplevel(height = 400, width = 600)
        window.title('Verification Results')
        nb = ttk.Notebook(window)
        f1 = ttk.Frame(nb)   # first page, which would get widgets gridded into it
        f2 = ttk.Frame(nb)   # second page
        f3 = ttk.Frame(nb)
        f4 = ttk.Frame(nb)

        nb.pack(expand=1, fill='both')

        ## Haddle computation Verification

        nb.add(f2, text='Computation')
        Results = Text(f2,height = 20,width = 110)
        Results.grid(column = 0,row = 0,columnspan=3,sticky = 'W')
        procedureName = self.procedure.split('.')[0]
        procedureName = procedureName.split('-')[1]

        if (procedureName == 'Procedure1'):
            Results.insert(INSERT,'Procedure: Procedure1.c\n')
            Results.insert(INSERT,'\n')
            Results.insert(INSERT,'Assertions Inserted to Source Code:\n')
            Results.insert(INSERT,'\tA1:assert(2*a != 0);\n')
            Results.insert(INSERT,'\ttemp1 = -b/(2*a);\n')
            Results.insert(INSERT,'\n')

            Results1 = Text(f2,height = 10,width = 110)
            Results1.grid(column = 0,row = 1,columnspan=3,sticky = 'W')
            Results1.insert(INSERT,'\n\n')
            Results1.insert(INSERT,'Verification Results:\n')
            Results1.tag_config("notV",background="yellow",foreground="red")
            Results1.tag_config("V",foreground="green")
            Results1.insert(INSERT,'\tA1\t\tTemporarily Verified\n',("V"))

        if (procedureName == 'Procedure2'):
            Results.insert(INSERT,'Procedure: Procedure2.c\n')
            Results.insert(INSERT,'\n')
            Results.insert(INSERT,'Assertions Inserted to Source Code:\n')
            Results.insert(INSERT,'\tA1:assert(b*b - 4 * a *c >= 0);\n')
            Results.insert(INSERT,'\ttemp2 = sqrt(b*b - 4 * a *c);\n')
            Results.insert(INSERT,'\n')

            Results1 = Text(f2,height = 10,width = 110)
            Results1.grid(column = 0,row = 1,columnspan=3,sticky = 'W')
            Results1.insert(INSERT,'\n\n')
            Results1.insert(INSERT,'Verification Results:\n')
            Results1.tag_config("notV",background="yellow",foreground="red")
            Results1.tag_config("V",foreground="green")
            Results1.insert(INSERT,'\tA1\t\tNot Verified!!!\n',("notV"))
            Results1.insert(INSERT,'\t\t\t Failure Condition: \n',("notV"))
            Results1.insert(INSERT,'\t\t\t\t a: 4.5\n',("notV"))
            Results1.insert(INSERT,'\t\t\t\t b: 2.2\n',("notV"))
            Results1.insert(INSERT,'\t\t\t\t c: 5.6\n',("notV"))

        nb.add(f1, text='Input/Output')
        Results = Text(f1,height = 12,width = 80,font = 30)
        Results.grid(column = 0,row = 0,columnspan=12,sticky = 'EW')
        procedureName = self.procedure.split('.')[0]
        procedureName = procedureName.split('-')[1]
        
        Results.tag_config("Emphasize",background="yellow")

        if (procedureName == 'Procedure1'):
            Results.insert(INSERT,'Procedure: Procedure1.c\n')
            Results.insert(INSERT,'\n')
            Results.insert(INSERT,'Input Specifications:\n')
            Results.insert(INSERT,'\t 0 <a <5\n')
            Results.insert(INSERT,'\t0 < b < 90\n',("Emphasize"))

            Results.insert(INSERT,'Output Specifications:\n')
            Results.insert(INSERT,'\t0 < temp1 < 1\n')
            Results.insert(INSERT,'In-Range Input -------> In-Range Output:\n')
            Results.insert(INSERT,'\tStatistical Results of 1000 Tests(see below):\n')

            blank = Label(f1)
            blank.grid(column = 0, row = 1, columnspan = 5, sticky = 'EW')

            greenLegend = Label(f1,width = 7, bg = 'green')
            greenLegend.grid(column = 0, row = 2, sticky = 'EW')
            greenText = Label(f1, text = 'In Range (0,1)',font = 2)
            greenText.grid(column = 2, row = 2, sticky = 'W')
            
            yellowLegend = Label(f1,width = 7, bg = 'yellow')
            yellowLegend.grid(column = 0, row = 3, sticky = 'EW')
            yellowText = Label(f1, text = 'Equal to 0',font = 2)
            yellowText.grid(column = 2, row = 3, sticky = 'W')
                           
            c = Canvas(f1,width=260, height=260)
            c.grid(column = 0,row = 4,columnspan = 4, sticky = 'W')
            c.create_arc((40,40,200,200),fill="green", start=self.frac(0),extent = self.frac(948))
            Inrange = 948/1000 * 100
            c.create_text(120,88,fill="black", text = '(0, 1): '+str(Inrange)+'%', font = 2)
            c.create_arc((40,40,200,200), fill="yellow", start=self.frac(948), extent = self.frac(52))
            Outrange = 52/1000 *100
            c.create_text(200,128,fill="black", text = 'Equal to 0: '+str(Outrange)+'%', font = 2)
            #c.create_arc((2,2,98,98), fill="green", start=self.frac(400), extent = self.frac(100))

            equal0 = 52
            rangeMin = 0
            rangeMax = 0.001482
            #data = [52,900,48,0]
            #data = [20, 15, 10, 7, 5, 4, 3, 2, 1, 1, 0]
            data = [5.2, 7.3,15.2,23.5, 28.7, 20.1, 0]
            dataRange = ['       0','(0-0.0003)','(0.0003-0.0006)','(0.0006-0.0009)','(0.0009-0.0012)','(0.0012-0.0015)','(0.0015-1.0)']

            c_width = 590
            c_height = 400/2
            c2 = Canvas(f1,width=c_width, height=c_height, bg = 'white')
            c2.grid(column = 6,row = 4,columnspan = 5, sticky = 'W')
            y_stretch = 15/3
            y_gap = 20/2
            x_stretch = 70/2
            x_width = 100/2
            x_gap = 2/2
            for x, y in enumerate(data):
                # calculate reactangle coordinates (integers) for each bar
                x0 = x * x_stretch + x * x_width + x_gap
                y0 = c_height - (y * y_stretch + y_gap)
                x1 = x * x_stretch + x * x_width + x_width + x_gap
                y1 = c_height - y_gap
                # draw the bar
                c2.create_rectangle(x0, y0, x1, y1, fill="blue")
                # put the y value above each bar
                c2.create_text(x0+10, y0, anchor=SW, text=str(y*10))
                c2.create_text(x0-5, c_height+5, anchor=SW, text=str(dataRange[x]))

            piechartTitle = Label(f1,text = 'Pie Chart Results Distribution',font = 2)
            piechartTitle.grid(column = 0,row = 5,rowspan = 2, columnspan = 4, sticky = 'EW')

            histogramTitle = Label(f1, text = 'Histogram of Results Distribution', font = 2)
            histogramTitle.grid(column = 6, row = 5, rowspan = 2, columnspan = 5, sticky = 'EW')

            blank = Label(f1)
            blank.grid(column = 0, row = 7, columnspan = 10, sticky = 'EW')

            self.clickNumber = 1
            TestUndisiredInput = Button(f1, text = 'Undesired Input Test', font = 36, activebackground = 'blue', command = self.inputTest1)
            TestUndisiredInput.grid(column = 10,row = 8,columnspan=1,sticky = 'E')


        if (procedureName == 'Procedure2'):
            Results.insert(INSERT,'Procedure: Procedure2.c\n')
            Results.insert(INSERT,'\n')
            Results.insert(INSERT,'Input Specifications:\n')
            Results.insert(INSERT,'\t 0 <a <5\n')
            Results.insert(INSERT,'\t0 < b < 90\n',("Emphasize"))
            Results.insert(INSERT,'\t0 < c < 10\n',("Emphasize"))

            Results.insert(INSERT,'Output Specifications:\n')
            Results.insert(INSERT,'\t0 < temp2 < 2\n')
            Results.insert(INSERT,'In-Range Input -------> In-Range Output:\n')
            Results.insert(INSERT,'\tStatistical Results of 1000 Tests(see below):\n')

            blank = Label(f1)
            blank.grid(column = 0, row = 1, columnspan = 5, sticky = 'EW')

            greenLegend = Label(f1,width = 7, bg = 'green')
            greenLegend.grid(column = 0, row = 2, sticky = 'EW')
            greenText = Label(f1, text = 'In Range (0,2)',font = 2)
            greenText.grid(column = 2, row = 2, sticky = 'W')
            
            yellowLegend = Label(f1,width = 7, bg = 'yellow')
            yellowLegend.grid(column = 0, row = 3, sticky = 'EW')
            yellowText = Label(f1, text = 'Equal to 0',font = 2)
            yellowText.grid(column = 2, row = 3, sticky = 'W')
                           
            c = Canvas(f1,width=260, height=260)
            c.grid(column = 0,row = 4,columnspan = 4, sticky = 'W')
            c.create_arc((40,40,200,200),fill="green", start=self.frac(0),extent = self.frac(948))
            Inrange = 948/1000 * 100
            c.create_text(120,88,fill="black", text = '(0, 1): '+str(Inrange)+'%', font = 2)
            c.create_arc((40,40,200,200), fill="yellow", start=self.frac(948), extent = self.frac(52))
            Outrange = 52/1000 *100
            c.create_text(200,128,fill="black", text = 'Equal to 0: '+str(Outrange)+'%', font = 2)
            #c.create_arc((2,2,98,98), fill="green", start=self.frac(400), extent = self.frac(100))

            equal0 = 52
            rangeMin = 0
            rangeMax = 0.001482
            #data = [52,900,48,0]
            #data = [20, 15, 10, 7, 5, 4, 3, 2, 1, 1, 0]
            data = [5.2, 7.3,15.2,23.5, 28.7, 20.1, 0]
            dataRange = ['       0','(0-0.0003)','(0.0003-0.0006)','(0.0006-0.0009)','(0.0009-0.0012)','(0.0012-0.0015)','(0.0015-1.0)']

            c_width = 590
            c_height = 400/2
            c2 = Canvas(f1,width=c_width, height=c_height, bg = 'white')
            c2.grid(column = 6,row = 4,columnspan = 5, sticky = 'W')
            y_stretch = 15/3
            y_gap = 20/2
            x_stretch = 70/2
            x_width = 100/2
            x_gap = 2/2
            for x, y in enumerate(data):
                # calculate reactangle coordinates (integers) for each bar
                x0 = x * x_stretch + x * x_width + x_gap
                y0 = c_height - (y * y_stretch + y_gap)
                x1 = x * x_stretch + x * x_width + x_width + x_gap
                y1 = c_height - y_gap
                # draw the bar
                c2.create_rectangle(x0, y0, x1, y1, fill="blue")
                # put the y value above each bar
                c2.create_text(x0+10, y0, anchor=SW, text=str(y*10))
                c2.create_text(x0-5, c_height+5, anchor=SW, text=str(dataRange[x]))

            piechartTitle = Label(f1,text = 'Pie Chart Results Distribution',font = 2)
            piechartTitle.grid(column = 0,row = 5,rowspan = 2, columnspan = 4, sticky = 'EW')

            histogramTitle = Label(f1, text = 'Histogram of Results Distribution', font = 2)
            histogramTitle.grid(column = 6, row = 5, rowspan = 2, columnspan = 5, sticky = 'EW')

            blank = Label(f1)
            blank.grid(column = 0, row = 7, columnspan = 10, sticky = 'EW')

            self.clickNumber = 1
            TestUndisiredInput = Button(f1, text = 'Undesired Input Test', font = 36, activebackground = 'blue', command = self.inputTest2)
            TestUndisiredInput.grid(column = 10,row = 8,columnspan=1,sticky = 'E')


        nb.add(f3, text='Constraint')
        Results = Text(f3,height = 35,width = 130,font = 30)
        Results.pack()
        procedureName = self.procedure.split('.')[0]
        procedureName = procedureName.split('-')[1]
        Results.tag_config("Err",foreground="red")
        Results.tag_config("Chg",foreground="yellow")
        if (procedureName == 'Procedure1'):
            Results.insert(INSERT,'No Constraint Specification For This Procedure')
        if (procedureName == 'Procedure2'):
            Results.insert(INSERT,'No Constraint Specification For This Procedure')

        nb.add(f4, text='Manual Error')
        Results = Text(f4,height = 50,width = 130,font = 30)
        Results.pack()
        Results.tag_config("Hypo",foreground="blue")
        procedureName = self.procedure.split('.')[0]
        procedureName = procedureName.split('-')[1]
        if (procedureName == 'Procedure1'):
            Results.insert(INSERT,'No Manual Mistake Found For this Procedure')
        if (procedureName == 'Procedure2'):
            Results.insert(INSERT,'No Manual Mistake Found For this Procedure')


    def inputTest1(self):
        if self.clickNumber == 1:
            f1 = tkinter.Toplevel(height = 200, width = 600)
            f1.title('Input-a')
            Results2 = Text(f1,height = 1,width = 35,font = 120)
            Results2.grid(column = 0,row = 0,columnspan=2,sticky = 'W')

            Results2.tag_config("Emphasize",background = 'yellow')
            Results2.tag_config("Err",foreground="red")
            Results2.insert(INSERT,'a(5,10):\n')

            blank = Label(f1)
            blank.grid(column = 0, row = 1, columnspan = 5, sticky = 'EW')

            greenLegend = Label(f1,width = 9, bg = 'green')
            greenLegend.grid(column = 0, row = 2, sticky = 'E')
            greenText = Label(f1, text = 'In Range (0,1)',font = 2)
            greenText.grid(column = 1, row = 2, sticky = 'W')


            yellowLegend = Label(f1,width = 9, bg = 'yellow')
            yellowLegend.grid(column = 0, row = 3, sticky = 'E')
            yellowText = Label(f1, text = 'Equal to 0',font = 2)
            yellowText.grid(column = 1, row = 3, sticky = 'W')

            blank = Label(f1)
            blank.grid(column = 0, row = 4, columnspan = 5, sticky = 'EW')

            c3 = Canvas(f1,width=260, height=200)
            c3.grid(column = 0,row = 5,columnspan=2, sticky = 'EW')
            c3.create_arc((2,2,150,150),fill="green", start=self.frac(0),extent = self.frac(18))
            Inrange = 18/1000 * 100
            c3.create_text(180,75,fill="black", text = '(0, 1): '+'1.8%')
            c3.create_arc((2,2,150,150), fill="yellow", start=self.frac(18), extent = self.frac(982))
            Outrange = 982/1000 *100
            c3.create_text(80,48,fill="black", text = 'Equal to 0: '+str(Outrange)+'%')

            data = [2,5,6, 4, 1, 0]
            dataRange = ['  (0,   0.0003)','(0.0003,0.0006)','(0.0006,0.0009)','(0.0009,0.0012)','(0.0012,0.0015)','(0.0015,1)']


            Results3 = Text(f1,height = 1,width = 35,font = 120)
            Results3.grid(column = 3,row = 0,columnspan=2,sticky = 'EW')
            Results3.tag_config("Err",foreground="red")
            Results3.tag_config("Emphasize",background = 'yellow')
            Results3.insert(INSERT,'a(-10,0):\n')

            c5 = Canvas(f1,width=260, height=200)
            c5.grid(column = 3,row = 5,columnspan=2, sticky = 'W')
            c5.create_arc((2,2,150,150),fill="green", start=self.frac(0),extent = self.frac(9))
            Inrange = 9/1000 * 100
            c5.create_text(180,68,fill="black", text = '(0, 1): '+ '0.9%')
            c5.create_arc((2,2,150,150), fill="yellow", start=self.frac(9), extent = self.frac(991))
            Outrange = 991/1000 *100
            c5.create_text(80,48,fill="black", text = 'Equal to 0: '+str(Outrange)+'%')

            
            self.clickNumber = self.clickNumber+1
            return
        if self.clickNumber == 2:
            f1 = tkinter.Toplevel(height = 200, width = 600)
            f1.title('Input-b')
            Results4 = Text(f1,height = 1,width = 35, font = 120)
            Results4.grid(column = 0,row = 0,columnspan=2,sticky = 'W')
            Results4.insert(INSERT,'b(90,500):\n')

            blank = Label(f1)
            blank.grid(column = 0, row = 1, columnspan = 5, sticky = 'EW')

            greenLegend = Label(f1,width = 9, bg = 'green')
            greenLegend.grid(column = 0, row = 2, sticky = 'E')
            greenText = Label(f1, text = 'In Range (0,1)',font = 2)
            greenText.grid(column = 1, row = 2, sticky = 'W')


            yellowLegend = Label(f1,width = 9, bg = 'yellow')
            yellowLegend.grid(column = 0, row = 3, sticky = 'E')
            yellowText = Label(f1, text = 'Equal to 0',font = 2)
            yellowText.grid(column = 1, row = 3, sticky = 'W')

            orangeLegend = Label(f1, width = 9, bg = 'orange')
            orangeLegend.grid(column = 0, row = 4, sticky = 'E')
            orangeText = Label(f1, text = 'Out-of Range [1,10)', font = 2)
            orangeText.grid(column = 1, row = 4, sticky = 'W')


            blackLegend = Label(f1, width = 9, bg = 'black')
            blackLegend.grid(column = 3, row = 2, sticky = 'E')
            blackText = Label(f1, text = 'Runtime Error',font = 2)
            blackText.grid(column = 4, row = 2, sticky = 'W')

            redLegend = Label(f1, width = 9, bg = 'red')
            redLegend.grid(column = 3, row = 3, sticky = 'E')
            redText = Label(f1, text = 'Out-of Range(-10,0)',font = 2)
            redText.grid(column = 4, row = 3, sticky = 'W')

            blank = Label(f1)
            blank.grid(column = 0, row = 5, columnspan = 5, sticky = 'EW')
            
            c6 = Canvas(f1,width=260, height=200)
            c6.grid(column = 0,row = 6,columnspan = 2, sticky = 'EW')
            c6.create_arc((2,2,150,150),fill="green", start=self.frac(0),extent = self.frac(84))
            Inrange = 9/1000 * 100
            c6.create_text(180,68,fill="black", text = '(0, 1): '+ '8.4%')
            c6.create_arc((2,2,150,150), fill="yellow", start=self.frac(84), extent = self.frac(45))
            Equal0 = 45/1000 *100
            c6.create_text(175,28,fill="black", text = 'Equal to 0: '+str(Equal0)+'%')
            c6.create_arc((2,2,150,150), fill="orange", start=self.frac(129), extent = self.frac(871))
            MoreThan1 = 871/1000 *100
            c6.create_text(80,98,fill="white", text = '[1,9.785770]: '+str(MoreThan1)+'%')

            Results5 = Text(f1,height = 1,width = 35, font = 120)
            Results5.grid(column = 3,row = 0,columnspan=2,sticky = 'W')
            Results5.tag_config("Err",foreground="red")
            Results5.insert(INSERT,'b(-500,0):\n')

            c7 = Canvas(f1,width=260, height=200)
            c7.grid(column = 3,row = 6,columnspan = 2, sticky = 'EW')
            c7.create_arc((2,2,150,150),fill="red", start=self.frac(0),extent = self.frac(173))
            Nomorethan0 = 173/1000 * 100
            c7.create_text(200,48,fill="black", text = '[-9.999536,0]: '+ '17.3%')
            c7.create_arc((2,2,150,150), fill="black", start=self.frac(173), extent = self.frac(823))
            Error = 823/1000 *100
            c7.create_text(105,88,fill="red", text = 'Error: Segmentation Fault: '+str(Error)+'%')
            
            self.clickNumber = self.clickNumber+1
            return
        
        if self.clickNumber == 3:
            tkinter.messagebox.showinfo('Message','No More Input')
            self.clickNumber = self.clickNumber+1
            return
        if self.clickNumber == 4:
            return

    #Test the procedure robustness if input is out of the expected range. 
    def inputTest2(self):
        if self.clickNumber == 1:
            f1 = tkinter.Toplevel(height = 200, width = 600)
            f1.title('Input-a')
            Results2 = Text(f1,height = 1,width = 35,font = 120)
            Results2.grid(column = 0,row = 0,columnspan=2,sticky = 'W')

            Results2.tag_config("Emphasize",background = 'yellow')
            Results2.tag_config("Err",foreground="red")
            Results2.insert(INSERT,'a(5,10):\n')

            blank = Label(f1)
            blank.grid(column = 0, row = 1, columnspan = 5, sticky = 'EW')

            greenLegend = Label(f1,width = 9, bg = 'green')
            greenLegend.grid(column = 0, row = 2, sticky = 'E')
            greenText = Label(f1, text = 'In Range (0,1)',font = 2)
            greenText.grid(column = 1, row = 2, sticky = 'W')


            yellowLegend = Label(f1,width = 9, bg = 'yellow')
            yellowLegend.grid(column = 0, row = 3, sticky = 'E')
            yellowText = Label(f1, text = 'Equal to 0',font = 2)
            yellowText.grid(column = 1, row = 3, sticky = 'W')

            blank = Label(f1)
            blank.grid(column = 0, row = 4, columnspan = 5, sticky = 'EW')

            c3 = Canvas(f1,width=260, height=200)
            c3.grid(column = 0,row = 5,columnspan=2, sticky = 'EW')
            c3.create_arc((2,2,150,150),fill="green", start=self.frac(0),extent = self.frac(18))
            Inrange = 18/1000 * 100
            c3.create_text(180,75,fill="black", text = '(0, 1): '+'1.8%')
            c3.create_arc((2,2,150,150), fill="yellow", start=self.frac(18), extent = self.frac(982))
            Outrange = 982/1000 *100
            c3.create_text(80,48,fill="black", text = 'Equal to 0: '+str(Outrange)+'%')

            data = [2,5,6, 4, 1, 0]
            dataRange = ['  (0,   0.0003)','(0.0003,0.0006)','(0.0006,0.0009)','(0.0009,0.0012)','(0.0012,0.0015)','(0.0015,1)']


            Results3 = Text(f1,height = 1,width = 35,font = 120)
            Results3.grid(column = 3,row = 0,columnspan=2,sticky = 'EW')
            Results3.tag_config("Err",foreground="red")
            Results3.tag_config("Emphasize",background = 'yellow')
            Results3.insert(INSERT,'a(-10,0):\n')

            c5 = Canvas(f1,width=260, height=200)
            c5.grid(column = 3,row = 5,columnspan=2, sticky = 'W')
            c5.create_arc((2,2,150,150),fill="green", start=self.frac(0),extent = self.frac(9))
            Inrange = 9/1000 * 100
            c5.create_text(180,68,fill="black", text = '(0, 1): '+ '0.9%')
            c5.create_arc((2,2,150,150), fill="yellow", start=self.frac(9), extent = self.frac(991))
            Outrange = 991/1000 *100
            c5.create_text(80,48,fill="black", text = 'Equal to 0: '+str(Outrange)+'%')

            
            self.clickNumber = self.clickNumber+1
            return
        if self.clickNumber == 2:
            f1 = tkinter.Toplevel(height = 200, width = 600)
            f1.title('Input-b')
            Results4 = Text(f1,height = 1,width = 35, font = 120)
            Results4.grid(column = 0,row = 0,columnspan=2,sticky = 'W')
            Results4.insert(INSERT,'b(90,500):\n')

            blank = Label(f1)
            blank.grid(column = 0, row = 1, columnspan = 5, sticky = 'EW')

            greenLegend = Label(f1,width = 9, bg = 'green')
            greenLegend.grid(column = 0, row = 2, sticky = 'E')
            greenText = Label(f1, text = 'In Range (0,1)',font = 2)
            greenText.grid(column = 1, row = 2, sticky = 'W')


            yellowLegend = Label(f1,width = 9, bg = 'yellow')
            yellowLegend.grid(column = 0, row = 3, sticky = 'E')
            yellowText = Label(f1, text = 'Equal to 0',font = 2)
            yellowText.grid(column = 1, row = 3, sticky = 'W')

            orangeLegend = Label(f1, width = 9, bg = 'orange')
            orangeLegend.grid(column = 0, row = 4, sticky = 'E')
            orangeText = Label(f1, text = 'Out-of Range [1,10)', font = 2)
            orangeText.grid(column = 1, row = 4, sticky = 'W')


            blackLegend = Label(f1, width = 9, bg = 'black')
            blackLegend.grid(column = 3, row = 2, sticky = 'E')
            blackText = Label(f1, text = 'Runtime Error',font = 2)
            blackText.grid(column = 4, row = 2, sticky = 'W')

            redLegend = Label(f1, width = 9, bg = 'red')
            redLegend.grid(column = 3, row = 3, sticky = 'E')
            redText = Label(f1, text = 'Out-of Range(-10,0)',font = 2)
            redText.grid(column = 4, row = 3, sticky = 'W')

            blank = Label(f1)
            blank.grid(column = 0, row = 5, columnspan = 5, sticky = 'EW')
            
            c6 = Canvas(f1,width=260, height=200)
            c6.grid(column = 0,row = 6,columnspan = 2, sticky = 'EW')
            c6.create_arc((2,2,150,150),fill="green", start=self.frac(0),extent = self.frac(84))
            Inrange = 9/1000 * 100
            c6.create_text(180,68,fill="black", text = '(0, 1): '+ '8.4%')
            c6.create_arc((2,2,150,150), fill="yellow", start=self.frac(84), extent = self.frac(45))
            Equal0 = 45/1000 *100
            c6.create_text(175,28,fill="black", text = 'Equal to 0: '+str(Equal0)+'%')
            c6.create_arc((2,2,150,150), fill="orange", start=self.frac(129), extent = self.frac(871))
            MoreThan1 = 871/1000 *100
            c6.create_text(80,98,fill="white", text = '[1,9.785770]: '+str(MoreThan1)+'%')

            Results5 = Text(f1,height = 1,width = 35, font = 120)
            Results5.grid(column = 3,row = 0,columnspan=2,sticky = 'W')
            Results5.tag_config("Err",foreground="red")
            Results5.insert(INSERT,'b(-500,0):\n')

            c7 = Canvas(f1,width=260, height=200)
            c7.grid(column = 3,row = 6,columnspan = 2, sticky = 'EW')
            c7.create_arc((2,2,150,150),fill="red", start=self.frac(0),extent = self.frac(173))
            Nomorethan0 = 173/1000 * 100
            c7.create_text(200,48,fill="black", text = '[-9.999536,0]: '+ '17.3%')
            c7.create_arc((2,2,150,150), fill="black", start=self.frac(173), extent = self.frac(823))
            Error = 823/1000 *100
            c7.create_text(105,88,fill="red", text = 'Error: Segmentation Fault: '+str(Error)+'%')
            
            self.clickNumber = self.clickNumber+1
            return
        
        if self.clickNumber == 3:
            f1 = tkinter.Toplevel(height = 200, width = 600)
            f1.title('Input-c')
            Results6 = Text(f1,height = 1,width = 35,font = 120)
            Results6.grid(column = 0,row = 0,columnspan=2,sticky = 'W')
            Results6.insert(INSERT,'c(10,100):\n',)

            blank = Label(f1)
            blank.grid(column = 0, row = 1, columnspan = 5, sticky = 'EW')

            greenLegend = Label(f1,width = 9, bg = 'green')
            greenLegend.grid(column = 0, row = 2, sticky = 'E')
            greenText = Label(f1, text = 'In Range (0,1)',font = 2)
            greenText.grid(column = 1, row = 2, sticky = 'W')


            yellowLegend = Label(f1,width = 9, bg = 'yellow')
            yellowLegend.grid(column = 0, row = 3, sticky = 'E')
            yellowText = Label(f1, text = 'Equal to 0',font = 2)
            yellowText.grid(column = 1, row = 3, sticky = 'W')

            blank = Label(f1)
            blank.grid(column = 0, row = 4, columnspan = 5, sticky = 'EW')

            c8 = Canvas(f1,width=260, height=200)
            c8.grid(column = 0,row = 5,columnspan = 2,sticky = 'W')
            c8.create_arc((2,2,150,150),fill="yellow", start=self.frac(0),extent = self.frac(57))
            Nomorethan0 = 173/1000 * 100
            c8.create_text(200,60,fill="black", text = 'Equal to 0: '+ '5.7%')
            c8.create_arc((2,2,150,150), fill="green", start=self.frac(57), extent = self.frac(943))
            Inrange = 943/1000 *100
            c8.create_text(85,88,fill="black", text = '(0,0.001496]: '+str(Inrange)+'%')

            Results7 = Text(f1,height = 1,width = 35, font = 120)
            Results7.grid(column = 3,row = 0,columnspan=2,sticky = 'W')
            Results7.tag_config("Err",foreground="red")
            Results7.insert(INSERT,'bed_fraction(-100,0):\n')
            
            c9 = Canvas(f1,width=260, height=200)
            c9.grid(column = 3,row = 5,sticky = 'W')
            c9.create_arc((2,2,150,150),fill="green", start=self.frac(0),extent = self.frac(254))
            Nomorethan0 = 173/1000 * 100
            c9.create_text(195,40,fill="black", text = '(0,0.001498]: '+ '25.4%')
            c9.create_arc((2,2,150,150), fill="yellow", start=self.frac(254), extent = self.frac(746))
            Inrange = 746/1000 *100
            c9.create_text(85,88,fill="black", text = 'Equal to 0: '+str(Inrange)+'%')
            
            self.clickNumber = self.clickNumber+1
            return
        if self.clickNumber == 4:
            tkinter.messagebox.showinfo('Message','No More Input')
            self.clickNumber = self.clickNumber+1
            return
        if self.clickNumber == 5:
            return

    # open verification specification file
    def openfile(self):
        filepath = askopenfilename()
        specificationFile = os.path.basename(filepath)
        self.procedure = specificationFile
        self.SpecFileName.set(specificationFile)
        SourceCodePath = self.traceProcedure(specificationFile)
        self.SourceCodePath.set(SourceCodePath)

    # find related source code .c file from specification file 
    def traceProcedure(self,procedure):
        procedureName = procedure.split('.')[0]
        procedureName = procedureName.split('-')[1]
        found = False
        filenames = next(os.walk(os.getcwd()))[2]
        for file in filenames:
            fileName = file.split('.')[0]
            fileName = fileName.split('-')[1]
            suffix = file.split('.')[-1]
            if (procedureName == fileName and suffix == 'c'):
                found = True
                sourceFile = file 
                break
                
        return sourceFile

    def createSettingWindow(self):
        
        window = tkinter.Toplevel(height = 200, width = 300)
        window.title('Verification Settings')

if __name__ == "__main__":
    app = specToAssertion()
    app.title('AutoV2')
    app.mainloop()