search

luisandresilva / reprotool

Automatically exported from code.google.com/p/reprotool
0 stars 0 forks source link

NuSMV code generator should add comments to formulae #85

Open GoogleCodeExporter opened 8 years ago

GoogleCodeExporter commented 8 years ago 
When a LTL/CTL formula is generated as LTLSPEC/CTLSPEC fragment in the NuSMV 
code there should be a comment generated after the formula which contains the 
"Description" field of the formula in the reprotool model.

For example:
  CTLSPEC AG(open_file -> AF(close_file)) -- After 'open' there should always be 'close'

or:
  -- After 'open' there should always be 'close'
  CTLSPEC AG(open_file -> AF(close_file))

Original issue reported on code.google.com by viliam.s...@gmail.com on 6 Mar 2012 at 12:26

GoogleCodeExporter commented 8 years ago 
ahoj, to uz nebudem riesit. Preto lebo komentare nie su sucastou AST ktory 
staviam pred tym ako ho poslem serializatoru. To by som musel upravit tu 
gramatiku a do toho by som sa nerad teraz pustal lebo by sa mohlo stat ze tam 
nieco rozbijem co si nevsimnem.

Original comment by rud...@gmail.com on 7 Mar 2012 at 5:41