Skip to content
Snippets Groups Projects
generate_ref_clk_state_machine.py 13.08 KiB
import os
import sys as ss
import ConfigParser
import ast
import pickle
import networkx as nx
from matplotlib import pyplot as plt
import pydot as pd
from generate_lockstep_state_machine import *

os.system('cls' if os.name == 'nt' else 'clear')

config_clock = ConfigParser.RawConfigParser()
config_proto = ConfigParser.RawConfigParser()

config_clock.read('clock_config.cfg')
config_proto.read('config_mclock.cfg')

# Getting clock details from the configuration file
clock_nodes = []
clock_tran_rel = []
clock_init_state = []

clock_nodes.append(ast.literal_eval(config_clock.get('clock_state_machine', 'protocolnodes')))
clock_tran_rel.append(ast.literal_eval(config_clock.get('clock_state_machine', 'protocol')))
clock_init_state.append(ast.literal_eval(config_clock.get('clock_state_machine', 'initstate')))

# proto nodes will get the state nodes of the protocol and the proto_tran_rel will get
# the transition relation of the protocol from the configuration file. 
# proto_nodes will be list of lists and proto_tran_rel wil be list of dictionaries. 
proto_nodes = {}
proto_tran_rel = {}
proto_init_state = {}
proto_broadcast_msg = {}

Protocols = ast.literal_eval(config_proto.get('Configuration', 'Protocols'))
#print Protocols.keys()

for key in Protocols.keys():
    for comp in Protocols[key]:
        protocol_name = key + ':' + comp
        proto_nodes[protocol_name] = ast.literal_eval(config_proto.get(protocol_name, 'protocolnodes'))
        proto_tran_rel[protocol_name] = ast.literal_eval(config_proto.get(protocol_name, 'protocol'))
        proto_init_state[protocol_name] = ast.literal_eval(config_proto.get(protocol_name, 'initstate'))
        try:
            proto_broadcast_msg[protocol_name] = ast.literal_eval(config_proto.get(protocol_name, 'broadcast'))
        except ConfigParser.NoOptionError, err:
            pass
            #print str(err)

#print proto_broadcast_msg

#ss.exit(0)

#print proto_nodes
#print proto_init_state

Xtended_proto_cfg_file = open('./cfg/Xtended_proto.cfg', 'w')
Xtended_proto_cfg_file.write('[Configuration]\n')
#Xtended_proto_cfg_file.write('Protocols: ' + str(Protocols) + '\n')
Xtended_proto_cfg_file.write('Protocols: [' + ", ".join('\'' + key + '\'' for key in Protocols.keys()) + ']\n')
Xtended_proto_cfg_file.write('Clock_Nodes: ' + str(len(clock_nodes[0])) + '\n\n')

for key in Protocols.keys():

    Xtended_proto_cfg_file.write('[' + key + ']\n')

    Intermediate_proto_cfg_file = open('./cfg/Intermediate_proto.cfg', 'w')
    Intermediate_proto_cfg_file.write('[Configuration]\n')
    Intermediate_proto_cfg_file.write('Protocols:['  + ", ".join('\'' + key + ':' + ele + '\'' for ele in Protocols[key]) + ']\n')
    Intermediate_proto_cfg_file.write('Clock_Nodes: ' + str(len(clock_nodes[0])) + '\n\n')

    for comp in Protocols[key]:
        protocol_name = key + ':' + comp
        print "Enhancing protocol state machine:", protocol_name
        Intermediate_proto_state_machine = {}
        Intermediate_proto_cfg_file.write('[' + protocol_name + ']\n')
        ListStateMachineNodes = []
        for j in range(len(clock_nodes[0])):
            for k in range(len(proto_nodes[protocol_name])):
                state_name = proto_nodes[protocol_name][k][0] + ':' + clock_nodes[0][j][0]
                ListStateMachineNodes.append(state_name)
        print "Possible States of the enhanced state protocol state machine are:", ListStateMachineNodes
        InitState = tuple([proto_init_state[protocol_name][0][0] + ':' + clock_init_state[0][0][0]])
    
        StatesExplored = []
        StatesYetToExplore = []
        StatesYetToExplore.append(InitState)
        print "Init State Queued:", InitState, "\n"
        
        # Extending one protocol with the reference clock state machine
        while StatesYetToExplore:
            #print "States Yet to Explore: ", StatesYetToExplore
            StateNowExploring = StatesYetToExplore.pop()
            print "Current State being Explored: ", StateNowExploring
            StatesExplored.append(StateNowExploring)
            try:
                assert (len(StatesYetToExplore) + len(StatesExplored)) <= len(ListStateMachineNodes)
            except AssertionError:
                print "Number of States Yet to Explore: ", len(StatesYetToExplore)
                print "Number of States Explored: ", len(StatesExplored)
                print "Number of total States in the new state machine: ", len(ListStateMachineNodes)
                ss.exit(1)

            EdgeOfProto = proto_tran_rel[protocol_name].get(tuple([StateNowExploring[0][:StateNowExploring[0].find(':')]]))
            # print "Edge of Proto State:", StateNowExploring[0][:StateNowExploring[0].find(':')], EdgeOfProto
            EdgeOfClk = clock_tran_rel[0].get(tuple([StateNowExploring[0][StateNowExploring[0].find(':')+1:]]))
            # print "Edge of Clock State:", StateNowExploring[0][StateNowExploring[0].find(':')+1:], EdgeOfClk

            # Case 1: The edge of the clock state machine is marked with 'True' only and no clock.
            # Then (w, ca) --> (w, ca'). There will be NO change in the state of the protocol state
            if len(EdgeOfClk) == 1 and EdgeOfClk.keys()[0] == 'True':
                tempdict = {}
                NextClockState = EdgeOfClk['True'][0][0]
                QStateToExplore = tuple([StateNowExploring[0][:StateNowExploring[0].find(':')] + ':' + NextClockState])
                tempdict['True'] = QStateToExplore
                # Reconstructing the transition relation in the extended transition system
                if StateNowExploring in Intermediate_proto_state_machine.keys():
                    Intermediate_proto_state_machine[StateNowExploring].update(tempdict)
                else:
                    Intermediate_proto_state_machine[StateNowExploring] = tempdict
                # A state just created can be in either of StatesExplored or in StatesYetToExplore but cannot be in both. If its not in both,
                # then it needs to be explored to find out reachable states and should be pushed in the StatesYetToExplore queue
                if QStateToExplore not in StatesExplored and QStateToExplore not in StatesYetToExplore:
                    StatesYetToExplore.append(QStateToExplore)
                    #print "Ref 1: New State Queued:", QStateToExplore, "\n\n"
                    # Case 2: The edge of the clock has more than one clock labeling with atleast one label being other than 'True'
                    # its time to move to next state of the protocol state machine
            else:
                CurrentClocks = EdgeOfClk.keys()
                CurrentProtoMsgs = EdgeOfProto.keys()
                NextClockState = EdgeOfClk[CurrentClocks[0]][0][0]
                for msg in CurrentProtoMsgs:
                    #print "Proto Message is:", msg[:msg.find(':')], " and clock is:", msg[msg.find(':') + 1:]
                    msgclk = msg[msg.find(':') + 1:]
                    #print "NextClockState is:", NextClockState
                    # Case 2.1: If the clock labeling of the protocol state machine and the clock
                    # state machine matches, then advance the protocol state machine and the clock 
                    # state machine
                    #print "msgclk:", msgclk
                    if msgclk in CurrentClocks:
                        tempdict = {}
                        #print "Solving: Case 2a.1\n"
                        NxtProtoState = EdgeOfProto[msg][0][0]
                        #print "NxtProtoState:", NxtProtoState, " and NextClockState:", NextClockState
                        QStateToExplore = tuple([NxtProtoState + ':' + NextClockState])
                        tempdict[msg[:msg.find(':')]] = QStateToExplore
                        #print "QStateToExplore:", QStateToExplore
                        #print "tempdict:", tempdict
                        # Reconstructing the transition relation in the extended transition system
                        if StateNowExploring in Intermediate_proto_state_machine.keys():
                            Intermediate_proto_state_machine[StateNowExploring].update(tempdict)
                        else:
                            Intermediate_proto_state_machine[StateNowExploring] = tempdict

                        if QStateToExplore not in StatesExplored and QStateToExplore not in StatesYetToExplore:
                            StatesYetToExplore.append(QStateToExplore)
                            #print "Ref 2: State Queued:", QStateToExplore, "\n\n"
                    # Case 2.2: If the clock labeling og the protocol state machine and the clock
                    # state machine does not match, then advance the clock state machine state but 
                    # not the state of the protocol state machine
                    else:
                        tempdict = {}
                        #print "Solving: Case 2a.2\n"
                        QStateToExplore = tuple([StateNowExploring[0][:StateNowExploring[0].find(':')] + ':' + NextClockState])
                        tempdict['True'] = QStateToExplore
                        #print "Case 2a.2 QStateToExplore:", QStateToExplore
                        # Reconstructing the transition relation in the extended transition system
                        if StateNowExploring in Intermediate_proto_state_machine.keys():
                            Intermediate_proto_state_machine[StateNowExploring].update(tempdict)
                        else:
                            Intermediate_proto_state_machine[StateNowExploring] = tempdict

                        if QStateToExplore not in StatesExplored and QStateToExplore not in StatesYetToExplore:
                            StatesYetToExplore.append(QStateToExplore)
                            #print "Ref 3: State Queued:", QStateToExplore, "\n\n"

        protocol_states = ", ".join(str(tuple([i])) for i in ListStateMachineNodes) 
        Intermediate_proto_cfg_file.write('protocolnodes: [' + protocol_states + ']\n')
        Intermediate_proto_cfg_file.write('protocol:' + str(Intermediate_proto_state_machine) + '\n')
        Intermediate_proto_cfg_file.write('initstate: [' + str(tuple([InitState[0]])) + ']\n')
        try:
            Intermediate_proto_cfg_file.write('broadcast: ' + str(proto_broadcast_msg[protocol_name])) 
        except KeyError:
            pass
        Intermediate_proto_cfg_file.write("\n\n")
    
        #print Xtended_proto_state_machine.keys()

        Intermediate_state_machine_states = Intermediate_proto_state_machine.keys()
        extended_state_machine_graph = pd.Dot(graph_type = 'digraph')
        NodeDict = {}
        for i in ListStateMachineNodes:
            if i == InitState[0]:
                NodeDict[i] = pd.Node(i.replace(':', '_'), style="filled", fillcolor="green")
            else:
                if tuple([i]) in Intermediate_state_machine_states:
                    NodeDict[i] = pd.Node(i.replace(':', '_'), style="filled", fillcolor="gray")
                else:
                    NodeDict[i] = pd.Node(i.replace(':', '_'), style="filled", fillcolor="red")
                    extended_state_machine_graph.add_node(NodeDict[i])
        #print NodeDict
        TotalNoEdges = 0 
        for i in ListStateMachineNodes:
            if tuple([i]) in Intermediate_state_machine_states:
                #print "i:", i
                for j in Intermediate_proto_state_machine[tuple([i])]:
                    #print "j:", j
                    for k in Intermediate_proto_state_machine[tuple([i])][j]:
                        #print "k:", k
                        TotalNoEdges = TotalNoEdges + 1
                        extended_state_machine_graph.add_edge(pd.Edge(NodeDict[i], NodeDict[k], label = j))

        extended_state_machine_graph.write_pdf("./pdf/" + protocol_name.replace(':', '_')+".pdf")
    
        print "\n"
        print '#' * 20
        print "Total Number of Possible States in the Enhanced State Machine of Protocol ", protocol_name, ": ",len(ListStateMachineNodes)
        print "Total Number of States in Enhanced State Machine of Protocol ", protocol_name, ": ", len(Intermediate_state_machine_states)
        print "Total Number of Edges  in Enhanced State Machine of Protocol ", protocol_name, ": ", TotalNoEdges
        print "Total Number of Unreachable states in the Enhanced State Machine of Protocol ", protocol_name, ": ", len(ListStateMachineNodes) - len(Intermediate_state_machine_states)
        print '#' * 20
        print "\n"
    
    Intermediate_proto_cfg_file.close() 
    print "Calling protocol construction routine...\n"
    Xtended_lts_machine, Initstate = construct_protocol('./cfg/Intermediate_proto.cfg', key)
    #os.system("rm -rfv ./cfg/Intermediate_proto.cfg")
    Xtended_lts_states = Xtended_lts_machine.keys()
   
    Xtended_lts_machine_init = []
    Xtended_lts_machine_init.append(tuple([Initstate[0].replace(':', '_', 1)]))
    draw_dot(Xtended_lts_machine, Xtended_lts_machine_init, 100, key)
    print "\n\n"
    
    Xtended_proto_cfg_file.write('protocolnodes: ' + str(Xtended_lts_states) + '\n')
    Xtended_proto_cfg_file.write('protocol: ' + str(Xtended_lts_machine) + '\n')
    Xtended_proto_cfg_file.write('initstate: ' + str([Initstate[0].replace(':', '_', 1)]) + '\n\n')

Xtended_proto_cfg_file.close()