'''This file is part of AToMPM - A Tool for Multi-Paradigm Modelling
Copyright 2011 by the AToMPM team and licensed under the LGPL
See COPYING.lesser and README.md in the root of this project for full details'''
#from numpy import *
import igraph as ig
import datetime
#import pydot
from threading import *
from random import choice
from .barrier import *
import sys
if sys.version_info[0] < 3:
from Queue import *
from sets import *
else:
from queue import *
class PnModule(Thread):
def __init__(self, pnet, que, bar, full=False):
Thread.__init__(self)
'''Our graph'''
self.pngraph = pnet;
P = self.pngraph.vs.select(type_eq = 'P')
key = P[0]['name'][:1]
self.key = key
#index in matrix to graph id
self.mx_to_gr_indexT = {}
self.mx_to_gr_indexP = {}
self.mx_to_gr_indexTn = {}
self.mx_to_gr_indexPn = {}
self.que = que
self.barrier = bar
self.TFtoRun = {}
self.ssc = 0
self.full = full
self.result={}
self.xxx = 0
def repstr(self,string, length):
return (string * length)[0:length]
def printMatrix(self,M):
lenr = len(M[0])
lenc = len(M)
first = True
i = 0
j = 0
text = ''
colwidth = []
for x in range(lenr):
text+=self.pngraph.vs[self.mx_to_gr_indexT[x]]['name']+' '
colwidth.append(len(self.pngraph.vs[self.mx_to_gr_indexT[x]]['name'])+1)
text+='\n'
for row in M:
for el in row:
text += '%d'%el+self.repstr(' ', colwidth[j]-len(str(int(el))))
j+=1
text += self.pngraph.vs[self.mx_to_gr_indexP[i]]['name']
text+='\n'
j=0
i+=1
print(text)
def summary(self):
ig.summary(self.reachability)
def getKey(self):
return self.key
def next(self):
self.ssc += 1
return self.ssc
def DminPlusMatrix(self):
i = 0
j = 0
self.incidence = zeros((self.numP,self.numT,))
for p in self.P:
self.mx_to_gr_indexP[i]=p.index
self.mx_to_gr_indexPn[p['name']]=i
self.M0[i]=p['nbTokens']
totrans = self.pngraph.successors(p.index)
fromtrans = self.pngraph.predecessors(p.index)
toweight = 0
fromweight = 0
for t in self.T:
if t.index in totrans:
self.dminus[i][j] = 1
toweight = int(self.pngraph.es[self.pngraph.get_eid(p.index,t.index)]['weight'])
self.dminus[i][j] = toweight
if t.index in fromtrans:
self.dplus[i][j] = 1
fromweight = int(self.pngraph.es[self.pngraph.get_eid(t.index,p.index)]['weight'])
self.dplus[i][j] = fromweight
#print t['name']
# if t.index in totrans:
# self.dminus[i][j] = 1
# elif t.index in fromtrans:
# self.dplus[i][j] = 1
# else:
# pass#row.append(0)
self.mx_to_gr_indexTn[t['name']] = j
self.mx_to_gr_indexT[j] = t.index
j+=1
i+=1
j = 0
# self.printMatrix(self.dminus)
# self.printMatrix(self.incidence)
# self.printMatrix(self.dplus)
#get Strongly connected components, used in modular analysis
def getSCC(self,M):
vindex = statePresent(M)
if not vindex == -1:
return self.reachability.vs[vindex]['SCC']
else:
return -1
def getSCCvid(self,id):
P = self.reachability.vs[int(id)]
return self.reachability.vs[int(id)]['SCC']
def statePresent(self, M):
for v in self.reachability.vs:
if all(v['M'] == M):
return v.index
return -1
#get all enabled transitions for state exploration
def enabledT(self,M):
enabled=[]
for j in range(self.numT):
good = True
tcol = self.dminus[0:self.numP,j] #Ti column over P as rows
for i in range(self.numP):
if tcol[i] > 0:
t = self.mx_to_gr_indexT[j]
p = self.mx_to_gr_indexP[i]
weight = int(self.pngraph.es[self.pngraph.get_eid(p,t)]['weight'])
if not M[i] >= weight :
good = False
break
if good:
# print 'Enabled trans %s'%self.pngraph.vs[self.mx_to_gr_indexT[j]]['name']
enabled.append(j)
return enabled
#produce new marking
def fire(self,j,M,fusion=False):
if fusion:
empty = []
empty.append(j)
return empty
else:
i = 0
marking = ''
for value in M:
marking+=' %s-%d'%(self.pngraph.vs[self.mx_to_gr_indexP[i]]['name'],value)
i+=1
#print 'Old marking %s'%marking
ts = zeros(self.numT) #array of Ts to fire, fire one transition indexed by j
ts[j] = 1
Mnew = M + dot(self.incidence,ts)
#print 'Fire %s'%self.pngraph.vs[self.mx_to_gr_indexT[j]]['name']
marking = ''
i=0
for value in Mnew:
marking+=' %s-%d'%(self.pngraph.vs[self.mx_to_gr_indexP[i]]['name'],value)
i+=1
#print 'New marking %s'%marking
return Mnew
#create reachability graph
def reachabilityG(self):
work=[]
work.append(self.M0)
self.reachability.add_vertices(1)
self.reachability.vs[0]['M'] = self.M0
while work:
M = work.pop()
#del(work[-1])
fromID = self.statePresent(M)
enabledTs = self.enabledT(M)
for i in enabledTs:
Mnew = self.fire(i,M)
idFound = self.statePresent(Mnew)
if idFound == -1:
self.reachability.add_vertices(1)
newID = self.reachability.vcount()-1
self.reachability.vs[newID]['M'] = Mnew
#print fromID
self.reachability.add_edges([(fromID,newID)])
self.reachability.es[self.reachability.get_eid(fromID, newID)]['T'] = self.pngraph.vs[self.mx_to_gr_indexT[i]]['name']
work.append(Mnew)
else:
self.reachability.add_edges([(fromID,idFound)])
self.reachability.es[self.reachability.get_eid(fromID, idFound)]['T'] = self.pngraph.vs[self.mx_to_gr_indexT[i]]['name']
self.barrier.wait() #several modules can run in parallel (comes from modular analysis) wait for all to finish.
#mark strong components of a graph
def SC(self):
if not 'SCC' in self.reachability.vs.attribute_names():
self.reachability.vs[0]['SCC'] = self.next()
components = self.reachability.clusters(mode=ig.STRONG)
for i in range(len(components)):
ssc = self.next()
changed = False
partial = False
for s in components[i]:
if self.reachability.vs[s]['SCC']>=0:
pass
else:
self.reachability.vs[s]['SCC'] = ssc
changed = True
if not changed:
self.ssc -= 1
#Transition fusion sets, modular analysys
def addToEnabledTF(self,TF,M):
if not TF in self.TFtoRun:
self.TFtoRun[TF]=[]
for m in self.TFtoRun[TF]:
if all(m==M) :
#print' duplicate'
return
self.TFtoRun[TF].append(M)
# vattr = ''
# j =0
# for id in M:
# vattr += '%s-%s,'%(self.pngraph.vs[self.mx_to_gr_indexP[j]]['name'],int(id))
# j+=1
#print 'adding %s to enabled Fusion transitions'%vattr
#for modular analysis
def explore(self,id):
work = []
work.append(id)
while work:
vid = work.pop()
#print 'explore name %s'%self.reachability.vs[vid]['M']
M = self.reachability.vs[vid]['M']
enabledTs = self.enabledT(M)
for i in enabledTs:
if self.pngraph.vs[self.mx_to_gr_indexT[i]]['fusion'] == True: #new
self.addToEnabledTF(self.pngraph.vs[self.mx_to_gr_indexT[i]]['name'],M) #new
continue #noted the shared transition continue exploring.
self.reachability.vs[vid]['visited'] = True
succ = self.reachability.successors(vid)
for i in succ:
if not self.reachability.vs[i]['visited']:
work.append(i)
self.reset()
def reset(self):
for p in self.reachability.vs:
p['visited']= False
def reachabilityModular(self):
work=[]
sgwork=[]
work.append(self.M0)
self.reachability.add_vertices(1)
self.reachability.vs[0]['M'] = self.M0
xxx = 0;
exp = False
while self.run:
while work:
M = work.pop()
fromID = self.statePresent(M)
enabledTs = self.enabledT(M)
from_M = []
for i in enabledTs:
if self.pngraph.vs[self.mx_to_gr_indexT[i]]['fusion'] == True: #new
self.addToEnabledTF(self.pngraph.vs[self.mx_to_gr_indexT[i]]['name'],M) #new
continue #noted the shared transition continue exploring.
else:
Mnew = self.fire(i,M)
idFound = self.statePresent(Mnew)
if idFound == -1:
self.reachability.add_vertices(1)
newID = self.reachability.vcount()-1
self.reachability.vs[newID]['M'] = Mnew
#print 'add edge src %d-dest %d name %s'%(fromID,newID,self.pngraph.vs[self.mx_to_gr_indexT[i]]['name'])
self.reachability.add_edges([(fromID,newID)])
self.reachability.es[self.reachability.get_eid(fromID, newID)]['T'] = self.pngraph.vs[self.mx_to_gr_indexT[i]]['name']
#if not self.pngraph.vs[self.mx_to_gr_indexT[i]]['fusion'] == True:
work.append(Mnew)
#if self.pngraph.vs[self.mx_to_gr_indexT[i]]['fusion'] == True:
#self.reachability.es[self.reachability.get_eid(fromID, newID)]['fusion'] = True
else:
if exp:
pass
#BACKWARDS
#self.explore(idFound)
self.reachability.add_edges([(fromID,idFound)])
self.reachability.es[self.reachability.get_eid(fromID, idFound)]['T'] = self.pngraph.vs[self.mx_to_gr_indexT[i]]['name']
if self.pngraph.vs[self.mx_to_gr_indexT[i]]['fusion'] == True:
self.reachability.es[self.reachability.get_eid(fromID, idFound)]['fusion'] = True
self.barrier.wait()
exp = False
self.graph(xxx);
xxx+=1;
ts = self.que.get(block=True,timeout=None)
self.result={}
res = {}
if '@exit' in ts:
self.run = False
break
for t in ts:
self.result[t]=[]
j = self.mx_to_gr_indexTn[t]
# Mse = self.reachability.es.select(T_eq=t)
from_M = []
to_M = []
for M in self.TFtoRun[t]: #loop over synchtransition edges
exp = True
Mnew = self.fire(j, M) #use marking at the source of the edge
if self.statePresent(Mnew) == -1:
self.reachability.add_vertices(1) #add this new marking
newID = self.reachability.vcount()-1 # to the reachability
self.reachability.vs[newID]['M'] = Mnew
work.append(Mnew)
from_M.append(self.statePresent(M))
to_M.append(self.statePresent(Mnew))
self.result[t].append(from_M)
self.result[t].append(to_M)
for ftlists in self.result:
for from_to in self.result[ftlists]:
for i in range(len(from_to)):
from_to[i] = '%s-%d'%(self.key,from_to[i])
for t in ts:
del self.TFtoRun[t] #remove processed maybe not yet?
def rnode(self,id,state):
vattr = ""
j=0
i = len(state)
for value in state:
vattr += '%s-%s'%(self.pngraph.vs[self.mx_to_gr_indexP[j]]['name'],int(value))
if not i-1 == 0:
vattr+=','
i -=1
j+=1
return "%s"%(id,vattr)+"\n"
#export reachability graph to xml
def reachtoxml(self,fname='',key=''):
header = "\n"
end = ""
for v in self.reachability.vs:
header+=self.rnode(v.index,v['M'])
for e in self.reachability.es:
header+="%s\n"%(e.source,e.target,e['T'])
dateTag = datetime.datetime.now().strftime("%Y-%b-%d_%H-%M-%S")
f = open('%s.%s.reachability.xml'%(fname,key),'w')
header+=end
f.write(header)
f.close()
def graph(self,key,fname='',id=None):
vattr=''
eattr = ''
nodes = {}
graph = pydot.Dot(self.key, graph_type='digraph')
dateTag = datetime.datetime.now().strftime("%Y-%b-%d_%H-%M-%S")
for v in self.reachability.vs:
i = len(v['M'])
leng = i
j=0
if 'SCC' in self.reachability.vs.attribute_names():
vattr +='SCC-%s\n'%v['SCC']
for value in v['M']:
if leng == 1:
vattr = 'fstate%d'%choice(list(range(100)))
else:
if int(value) > 0:
vattr += '%s-%s '%(self.pngraph.vs[self.mx_to_gr_indexP[j]]['name'],int(value))
if not i-1 == 0:
pass#vattr+=','
i -=1
j+=1
#vattr+='\nid-%d'%v.index;
#vattr +=')'
nodes[v.index] = pydot.Node(vattr)
graph.add_node(nodes[v.index])
vattr = ''
for e in self.reachability.es:
graph.add_edge(pydot.Edge(nodes[e.source],nodes[e.target],label=e['T']))
#graph.write_svg('graphs/STATE%s%d%s.svg'%(self.key,choice(range(100)),dateTag))
if not fname:
graph.write_svg('graphs/STATE%s%d%s.svg'%(self.key,choice(list(range(100))),dateTag))
else:
graph.write_svg('%s.%s.reachability.svg'%(fname,key))
#the thread per module
def run(self):
self.reachability = ig.Graph(0,directed=True)
TF = self.pngraph.vs.select(fusion_eq = True)
self.TFS = []
for tf in TF:
self.TFS.append(tf['name'])
self.P = self.pngraph.vs.select(type_eq = 'P')
self.key = self.P[0]['name'][:1]
self.T = self.pngraph.vs.select(type_eq = 'T')
self.numP = len(self.P.indices)
self.numT = len(self.T.indices)
#Get places and transitions
self.M0 = zeros(self.numP)
self.dminus = zeros((self.numP,self.numT,))
self.dplus = zeros((self.numP,self.numT,))
self.DminPlusMatrix()
self.incidence = self.dplus - self.dminus
self.printMatrix(self.incidence)
if self.full:
self.reachabilityG()
else:
self.reachabilityModular()
def reachable(self, state):
P = zeros(self.numP)
for ps in state:
for key,value in list(ps.items()):
index = self.mx_to_gr_indexPn[key]
P[index] = value
id = self.statePresent(P)
if not id==-1:
return True
else:
return False
def reachableMod(self,state):
P = zeros(self.numP)
for ps in state:
for key,value in list(ps.items()):
index = self.mx_to_gr_indexPn[key]
P[index] = value
id = self.statePresent(P)
components = self.markAncestors(id)
return Set(components)
def markAncestors(self,id):
work = []
result = []
work.append(id)
while work:
vid = work.pop()
result.append(self.reachability.vs[vid]['SCC'])
self.reachability.vs[vid]['visitedd'] = True
ancestors = self.reachability.predecessors(vid)
for i in ancestors:
if not self.reachability.vs[i]['visitedd']:
work.append(i)
#self.reset()
return result
def getEnabledTFs(self):
return list(self.TFtoRun.keys())