Small improvements to the .dot output #561
Conversation
- shorter SAPiC rulenames in .dot output - empty action lists are not displayed - shortened/rewrote duplicate code that resulted from the new changes
| showRuleName (StandRule rn) = | ||
| case rn of | ||
| NonSAPiCRuleName s -> 'r' : s | ||
| SAPiCRuleName s -> 'r' : s |
There was a problem hiding this comment.
This looks functionally the same to the old code. Possible typo?
| unNull s = if null s then "p" else s | ||
| stripSemicolon = filter (/= ';') |
There was a problem hiding this comment.
How sure are you that this filters everything dot does not want. As we do not have the dot output in the regression tests, we may want to just filter for everything that we know dot does not except, not just the intersection with what we currently think occurs in SAPIC.
| @@ -142,7 +142,7 @@ fromRuleRestriction rname f = | |||
| -- creates restriction with f quantified over free variables | |||
| -- and varnow | |||
| mkRestriction f' = Restriction | |||
| (restrPrefix ++ rname) | |||
| (restrPrefix ++ filter (/= '#') rname) | |||
There was a problem hiding this comment.
Here and and line 157: probably you found this bug by testing. To make the code a little more solid: can you define a function that (positively) defines what may occur in a rule? Having this in the smart constructor is good practice, well done.
There was a problem hiding this comment.
We make a lot of code inside the main parts of tamarin more complicated just because of a simple readability change for SAPIC. I have two ideas how to make this better.
- Create a smart constructor for standard rules
- Instead of a constructor to differentiate rules produces by SAPIC, let it be a Tag
The second can be useful if we think of other things that we want different for SAPIC in the future. We can also combine the two ideas, having one or two smart constructors (e.g., one for Rules and one for Standard Rules) for the Tamarin cases. Note that SAPIC rules are only generated by our translation and (edge case) from parsing downloaded theories with SAPIC output. (Here, we could encode the tag in an attribute. Actually, why not just have it as an attribute?)
Hi,
This PR adds some small improvements to the .dot output (as requested by @rkunnema).
In the .dot output, SAPiC rule names are "shortened": "rule_001000_1" becomes just "rule" in the .dot nodes.
All other rule names are not affected in any way.
Additionally, when we have an empty actions list ("[]"), the list ("[]") not displayed at all in the .dot nodes.