a4/code/sut/learnlib_dot2jtorx_aut.py

   1 #!/usr/bin/env python
   2 """
   3 generates aut for jtorx from dot file learned with learnlib
   4   '?COIN_1_1'
   5   '!TEA_0_1'
   6
   7 note: dot file uses I for input instead of ? and O for output instead of !
   8 """
   9 # Author: Harco Kuppens
  10
  11
  12 import sys, re, pprint  # modules from standard lib (python 2.6 and later)
  13
  14
  15
  16 def get_lts_from_dotfile(dot_file):
  17     """ Get labeled transition system from graphviz dot file
  18
  19         The dot file:
  20            - describes a digraph with labels
  21            - encodes the start state with the color='red' attribute
  22              note: this corresponds with the highlighted state in learnlib API
  23
  24         Returns: [start_state,transions]
  25         Where :
  26            - start_state: start state label
  27            - transitions: list of transitions
  28
  29     """
  30
  31     start_state='unknown'
  32     f=file(dot_file)
  33     lines=f.readlines()
  34
  35
  36
  37     # find start state
  38     #  line in dot: __start0 -> s0;
  39     for line in lines:
  40         if line.find('->') != -1:
  41             if line.find('__start') != -1:
  42                start_state=line[line.find('->')+2:].strip(" ;\t\n")
  43                break
  44
  45
  46     # get transitions
  47     #   line in dot:  s5 -> s5 [label="ARTREG 20013226 / 531"];
  48     transitions=[]
  49     for line in lines:
  50         if line.find('__start') != -1:
  51             continue
  52         if line.find('->') != -1:
  53             transitions.append(line)
  54
  55     # throw away transitions with the keywords : quiescence or inconsistency or undefined
  56     #transitions = [ t for t in transitions if ( 'quiescence' not in t ) and ( 'inconsistency' not in t  )  and ( 'undefined' not in t  )]
  57
  58     trans_out=[]
  59     regexpr_transition=re.compile(r'\s*(\w*)\s*-\>\s*(\w*)\s*\[label=\"(.*)\"\]')
  60     regexpr_tag=re.compile(r'<[^>]+>')
  61     for transition in transitions:
  62         match=regexpr_transition.match(transition)
  63         if match:
  64             match=match.groups()
  65             label=regexpr_tag.sub('',match[2])
  66             trans_out.append({
  67               'source' : match[0],
  68               'target' : match[1],
  69               'label': label
  70             })
  71
  72     states=set()
  73     for t in trans_out:
  74         states.add(t['source'])
  75         states.add(t['target'])
  76
  77
  78     return [start_state,states,trans_out]
  79
  80
  81 def parse_labels_of_mealy_lts(transitions):
  82     """Parse labels of labeled transition system
  83     """
  84     trans_out=[]
  85     for t in transitions:
  86         label=t['label']
  87         [inputstr,outputstr]=label.split('/')
  88         trans_out.append({
  89           'source' : t['source'],
  90           'target' : t['target'],
  91           'input':  inputstr,
  92           'output':  outputstr,
  93         })
  94     return trans_out
  95
  96 def split_io_transitions_in_separate_input_and_output_transition(io_transitions,nr_states):
  97     """Split transitions with both an input and output event into two transitions
  98
  99        Makes two sequential transitions with a dummy state in between:
 100         - dummy state <midstate> is labeled :
 101              m_<counter>
 102         - first transition :
 103              <source> -> <midstate>  for  <input>
 104         - second transition :
 105              <midstate> -> <target>  for <output>
 106     """
 107     trans_out=[]
 108     id=nr_states
 109     for t in io_transitions:
 110         midstate= 'm' + str(id)
 111         trans_out.append({
 112             'source': t['source'],
 113             'target': midstate,
 114             'label' : "?" + t['input'].strip(),
 115         })
 116         trans_out.append({
 117             'source': midstate,
 118             'target': t['target'],
 119             'label' : "!" + t['output'].strip(),
 120         })
 121         id=id+1
 122
 123     states=set()
 124     for t in trans_out:
 125         states.add(t['source'])
 126         states.add(t['target'])
 127
 128     return [states,trans_out]
 129
 130
 131 def transitions2aut(transitions,first_state,nr_of_states):
 132     nr_of_transitions=len(transitions)
 133     strings=[ "des(" + first_state[1:] + ","  + str(nr_of_transitions) + "," + str(nr_of_states) +")"]
 134     for t in transitions:
 135        #aut_edge ::= "(" start_state "," label "," end_state ")"
 136        strings.append("("+t['source'][1:] + "," + '"' + t['label'] + '"' + "," + t['target'][1:] + ")" )
 137
 138     return "\n".join(strings)
 139
 140
 141 def dot2aut(dot_filename_in):
 142     """
 143        from mealy machine in a .dot file written by DotUtil.write of learnlib
 144        we create an .aut file containing an lts where input and output each
 145        have its own labeled transition. An input transition has a
 146        label starting with '?' and an output transition has a label
 147        starting with '!'
 148
 149     """
 150
 151     if  dot_filename_in[-4:].lower() != '.dot':
 152        print "Problem: file '"+ dot_filename_in + "' is not a dot file!!"
 153        print "Exit!"
 154        sys.exit(1)
 155
 156
 157     [start_state,states,transitions]=get_lts_from_dotfile(dot_filename_in)
 158
 159
 160
 161     io_transitions=parse_labels_of_mealy_lts(transitions) # each transition has input and output
 162     [states,transitions]=split_io_transitions_in_separate_input_and_output_transition(io_transitions,len(states)) # each transition only has label again
 163
 164     #pprint.pprint(start_state)
 165     #pprint.pprint(states)
 166     #pprint.pprint(transitions)
 167
 168     result=transitions2aut(transitions,start_state,len(states))
 169
 170     aut_filename=dot_filename_in[:-4] + ".aut"
 171
 172     f=open(aut_filename ,'w')
 173     f.write(result)
 174     f.close()
 175
 176     print "written file : " +  aut_filename
 177
 178
 179 if __name__ == "__main__":
 180     dot2aut(*sys.argv[1:])
 181