diff --git a/n-vivace-satreach-cyber/b-satkubernetes.py b/n-vivace-satreach-cyber/b-satkubernetes.py index bf3c6b773a1adc3b01e43783432d63338e964712..328eb63903ec6600e3bd2126e0547d668a31a6ec 100644 --- a/n-vivace-satreach-cyber/b-satkubernetes.py +++ b/n-vivace-satreach-cyber/b-satkubernetes.py @@ -3,11 +3,12 @@ import sys, yNaming as naming RADIUS=1 CONTROLSHIFT=1 # shift for reading the initial and final configurations NTRANS=8 -T=20 # number of time steps -# transition table -TABTRANS="" + +# GLOABAL VARS +T=0 # number of time steps +TABTRANS="" # transition table #sx="*1111101*" # initial configuration #sy="*0111001*" # final configuration @@ -75,10 +76,11 @@ def genSpaceTime(T): #%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% def run(): - global N,TABTRANS + global N, T, TABTRANS ECA=int ( sys.argv[1] ) TABTRANS='{0:08b}'.format(ECA)[::-1] - x,y=sys.argv[2],sys.argv[3] + T=int ( sys.argv[2] ) + x,y=sys.argv[3],sys.argv[4] assert len(x) == len(y) sx,sy="*%s*"%x,"*%s*"%y N=len(sx) diff --git a/n-vivace-satreach-cyber/c-ECApaths.py b/n-vivace-satreach-cyber/c-ECApaths.py index 7b5dd1d72e8cfeddfc7441d4303a85ddff7f6832..d01e5f55d889afb4baebda921f2a5706d83ee37e 100644 --- a/n-vivace-satreach-cyber/c-ECApaths.py +++ b/n-vivace-satreach-cyber/c-ECApaths.py @@ -1,4 +1,28 @@ -import os +import os, sys + +ECA=110 +TSTEPS=70 +x, y = "0101010011010011011101", "1011101101110110111001" + +EXCEPTIONMINISAT=2560 + +def runcmd(cmd): + cmdresult= os.system(cmd) + print("cmd:%s"%(cmd)) + if cmdresult!=0 and cmdresult!=EXCEPTIONMINISAT: + sys.exit("\nFATAL ERROR code:%d raised by script command:\n[%s"%(cmdresult,cmd)) + def run(): - os.system("python3 b-satkubernetes.py 90 01001 11000 > ztst.dat") \ No newline at end of file + basename="ECA%d-%s-%s"%(ECA,x,y) + cmd1="python3 b-satkubernetes.py %d %d %s %s > %s.dat"%(ECA, TSTEPS, x, y, basename) + cmd2="python3 x2-convertToSat.py %s.dat "%basename + cmd3="minisat %s.cnf Zsol-%s.cnf"%(basename,basename) + ncells=len(x)+2 + cmd4="python3 w-prnCNFsolution.py %d Zsol-%s.cnf"%(ncells, basename) + cmdseq=[cmd1,cmd2,cmd3,cmd4] + for cmd in cmdseq: + #print(cmd) + runcmd(cmd) + +run() \ No newline at end of file diff --git a/n-vivace-satreach-cyber/w-prnCNFsolution.py b/n-vivace-satreach-cyber/w-prnCNFsolution.py index 007223c6244762ca1985653a5c36586484bc1957..a17b375c22a1f9824cb1fe66c42c96a7657fcf8f 100644 --- a/n-vivace-satreach-cyber/w-prnCNFsolution.py +++ b/n-vivace-satreach-cyber/w-prnCNFsolution.py @@ -16,9 +16,9 @@ def processFile(filename, ncell): endstr='\n' if count%ncell==0 else ' ' print(stoken,end=endstr) -def run(): - filename=sys.argv[1] - ncell=int(sys.argv[2]) +def run(): + ncell=int(sys.argv[1]) + filename=sys.argv[2] print("solution of :%s size:%d" % (filename,ncell)) print("-"*(2*ncell-1)) processFile(filename, ncell) diff --git a/n-vivace-satreach-cyber/x2-convertToSat.py b/n-vivace-satreach-cyber/x2-convertToSat.py index ebfd9db7737853143cf34983aa1ccd33b9ce622f..772e823f734a558891b368a84edc9f3969b8bfbf 100644 --- a/n-vivace-satreach-cyber/x2-convertToSat.py +++ b/n-vivace-satreach-cyber/x2-convertToSat.py @@ -26,27 +26,41 @@ def processDIC(line): output+="0" # end of line if tokenarray[len(tokenarray)-1].startswith("KOMM"): # comment should be the last element output+= " c "+ token[5:] - print(output) + return output def readval(strval): return int(strval[2:]) -def processFile(filename): - f = open(filename, "r") - head= f.readline() - headtokenarray= head.split() - T=readval(headtokenarray[1]) # extract what is after "T=" - N=readval(headtokenarray[2]) # extract what is after "N=" - #print(" read info T:%d N:%d" %(T,N)) - genDIC(T,N) - lines = f.readlines() - for line in lines: - #print("reading line:" + line) - processDIC(line) +def processFile(filename,fileoutput): + f = open(filename, "r") + head= f.readline() + lines = f.readlines() + + headtokenarray= head.split() + T=readval(headtokenarray[1]) # extract what is after "T=" + N=readval(headtokenarray[2]) # extract what is after "N=" + print(" converting to CNF ; read info T:%d N:%d" %(T,N)) + genDIC(T,N) + + fileout=open(fileoutput,"w") + # header + nbvars= N * (T+1) + nbclauses= len(lines) + header="p cnf %d %d"%(nbvars,nbclauses) + fileout.write(header+"\n") + # body + for line in lines: + #print("reading line:" + line) + lineout=processDIC(line) + fileout.write(lineout+"\n") + fileout.close() + f.close() + def run(): - filename=sys.argv[1] - #print("converting:%s"%filename) - processFile(filename) + filesrc=sys.argv[1] + fileoutput=filesrc.rstrip(".dat")+".cnf" + print("converting:%s to %s"%(filesrc,fileoutput)) + processFile(filesrc,fileoutput) run()