Clock names error

[Louis-Marie Traonouez]

when checking refinement between a component and itself,
or between a conjunction and one of the specifications
(e.g. T = Machine & MachineImpl; T >= MachineImpl)
pyecdar reports a bug

---------------------------------------------------------------------------
AssertionError Traceback (most recent call last)
/local/ltraonou/Developpement/python/pyecdar/<ipython-input-23-44613d658ce5> in <module>()
----> 1 T <= MachineImpl

/local/ltraonou/Developpement/python/pyecdar/pyecdar.pyc in __le__(self, big_spec)
    404
    405 def __le__(self,big_spec):
--> 406 return self.refine(big_spec)
    407
    408 def __ge__(self,small_spec):

/local/ltraonou/Developpement/python/pyecdar/pyecdar.pyc in refine(self, big_spec)
    352
    353 dbmpyuppaal.parse_nta_dbm(self.workspace.nta)
--> 354 dbmpyuppaal.parse_templates_dbm(self.workspace.nta,[model_template])
    355
    356 refCheck = pyreachability.ReachabilityAnalysis(self.workspace.nta,model_template,"UNSAFE",True)

/home/ltraonou/.local/lib/python2.7/site-packages/dbmpyuppaal/dbmpyuppaal.pyc in parse_templates_dbm(nta, template_list)
    318 """
    319 for template in template_list:
--> 320 nta.context = parse_local_clocks(template,nta.context)
    321 template.clocks = {}
    322 channels = {}

/home/ltraonou/.local/lib/python2.7/site-packages/dbmpyuppaal/dbmpyuppaal.pyc in parse_local_clocks(template, context)
    294 if declaration.type == 'clock':
    295 clock_name = template.name + '.' + declaration.name
--> 296 context.addClockByName(clock_name)
    297 return context
    298

/home/ltraonou/.local/lib/python2.7/site-packages/pydbm/udbm.pyc in addClockByName(self, clock_name)
    383 clock = _Clock(self, clock_name, len(self.clocks))
    384 self.clocks.append(clock)
--> 385 assert(not (hasattr(self, clock_name)))
    386 setattr(self, clock_name, clock)
    387 def hasClockByName(self, clock_name):

AssertionError:
-------------------------------------------------------------------------------

So pyecdar does not support checking refinement with itself because the two models have the same clock names.
Maybe due to the technique for refinement based on computed the product with the small spec and the reverse big spec,
since in that case small_spec and big_spec have clocks with the same name.

Solutions:
 1 temporarily change the name of the clocks when checking refinement
2 change the name of the clocks when computing a product, either with a prefix or suffix