gts-morpher / gts_morpher

Tool for building GTS Morphisms and Amalgamations
MIT License
4 stars 0 forks source link

rules mapped to multiple rules that get joined #26

Open narudocap opened 4 years ago

narudocap commented 4 years ago

The model is wrong, the counter should have a top element which get mapped to the top element of the target model. However, with this definition the completion takes the initialization rule to all remaining rules, which then get joined in one single rule.

pls_joined_rules_bug.zip

szschaler commented 4 years ago

The problem here is that the interface part of the rule is an empty rule. Auto-completion prefers mapping from an existing rule over creating a new virtual rule. It finds that it can map the (empty) interface part of Initialize to any of the rules for which no completion has been produced and generates that completion despite the fact that it's not a monomorphism over the rule names.

The weaver treats rule composition different from other kinds of composition. There is, I believe, an implicit assumption in that code (or possibly in the code extracting the rule mappings in the first place) that rule name mappings will always be monomorphisms. As a result, the weave actually picks a random existing rule and doesn't copy across any of the other rules.

There are different options for fixing this:

  1. Force auto-completion to only generate monomorphisms.
  2. Continue to allow auto-completion to generate non-monomorphisms, but provide an additional flag that allows users to specify that they don't want such completions.
  3. Fix weaving / conversion so that non-monomorphisms are handled correctly.