#################################################################################
##################################PREAMBLE#######################################
##“Copyright 2014 Rémy Chrétien”
##This file is part of Cpp2auto.
##
## Cpp2auto 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 3 of the License, or
## (at your option) any later version.
##
## Cpp2auto 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 Cpp2auto. If not, see .
#################################################################################
#################################################################################
import sys
#Please update the path to your compatible version of LALBLC:
sys.path.append("../LALBLC/")
from grammars import *
from strategies import *
from tactics import *
from parseGrammars import *
sys.path.append("Examples/")
from RunningExample import *
from Passport import *
from WMF import *
from DenningSacco import *
from PrivateAuth import *
#Select the protocols to test:
proto = [#(wmf1, wmf2, 'WMF1'),
#(wmf3, wmf4, 'WMF2'),
#(ds1, ds2, 'DenningSacco1'),
#(ds3, ds4, 'DenningSacco2'),
(passport1, passport2, 'Passport1'),
#(passport3, passport4, 'Passport2'),
#(pa1, pa2, 'PrivateAuth1'),
#(pa3, pa4, 'PrivateAuth2'),
#(ex1, ex2, 'RunningExample1'),
#(ex3, ex4, 'RunningExample2'),
]
def axioms(G, dic):
"""
Given a Greibach grammar from a renamed automaton G and list of 2 dictionnaries
mapping former states names (resp. stack symbols) to the new numeric ones,
computes the two renamed axioms and and returns their
corresponding matrices (to be used with strategies).
"""
newstate = dic[0]
newssymbol = dic[1]
startp = '<'+str(newstate['p0'])+'-'+str(newssymbol['O'])+'-'+str(newstate['pf'])+'>'
startq = '<'+str(newstate['q0'])+'-'+str(newssymbol['O'])+'-'+str(newstate['qf'])+'>'
#print(startp, startq)
S=word_to_mat([startp],G)
T=word_to_mat([startq],G)
return S, T
def prove(G, dic):
"""
Given a Greibach grammar from a renamed automaton G and list of 2 dictionnaries
mapping former states names (resp. stack symbols) to the new numeric ones,
try to prove the equivalence of the two grammars (with axioms axioms(G, dic)),
prints and returns the result of the lAlBlC tool on them.
"""
S, T = axioms(G, dic)
res = strategy_DCSRqmgudynA(G, S, T)
print("################################")
print("Result:")
print(res)
print("################################")
return res
for p, q, name in proto:
#Reach grammar
reach1 = auto_reach(p,q)
reach2, newstate, newssymbol = renameaut(reach1)
GQ = autotogram_quick(reach2)
GG = greibach(GQ)
#You can save the grammar in a file. Here is a sample line to do so:
#writeGrammar(GG, 'YourFileName', [newstate, newssymbol])
#In order to retrieve the grammar:
#G, dic = readGrammar('YourFileName')
s = name + ' reach grammar successfully computed.'
print(s)
prove(GG, [newstate, newssymbol])
#prove(GG, dic) #If you wrote the grammar in a file
#Const grammar
const1 = auto_const(p,q)
const2, newstate, newssymbol = renameaut(const1)
GQ = autotogram_quick(const2)
GG = greibach(GQ)
s = name + ' const grammar successfully computed.'
print(s)
prove(GG, [newstate, newssymbol])
#Fork grammar
fork1 = auto_fork(p,q)
fork2, newstate, newssymbol = renameaut(fork1)
GQ = autotogram_quick(fork2)
GG = greibach(GQ)
s = name + ' fork grammar successfully computed.'
print(s)
prove(GG, [newstate, newssymbol])