Class AbstractModelExporter

java.lang.Object
ca.mcscert.jpipe.visitor.AbstractModelExporter
All Implemented Interfaces:
JustificationVisitor<Void>
Direct Known Subclasses:
DotExporter, JsonExporter, PythonExporter
public abstract class AbstractModelExporter extends Object implements JustificationVisitor<Void>
Abstract base for exporters that serialise a single JustificationModel to text. Provides the common infrastructure shared by all single-model exporters:

Subclasses implement exportModel(JustificationModel) to perform the actual serialisation, setting currentModelName as their first action. Element visit methods (visit(Conclusion), etc.) are left abstract so each exporter controls its own output format.

  • Field Details

    • builder

      protected final StringBuilder builder
      Accumulates the serialised output. Reset at the start of each export.

    • currentModelName

      protected String currentModelName
      Name of the model currently being exported. Set by exportModel(JustificationModel) before any element visit methods are called.

  • Constructor Details

    • AbstractModelExporter

      public AbstractModelExporter()

  • Method Details

    • qualify

      protected final String qualify(String elementId)
      Qualifies elementId with the current model name: "currentModelName:elementId".

    • initAliases

      protected final void initAliases(JustificationModel<?> model)
      Builds the inverted alias lookup and the link index for model. Subclasses that surface aliases must call this at the start of exportModel(JustificationModel), after setting currentModelName.

    • qualifiedAliasesOf

      protected final List<String> qualifiedAliasesOf(String plainElementId)
      Returns the qualified original ids that were merged into plainElementId, or an empty list when the element is not the target of any alias. Requires initAliases(JustificationModel) to have been called first.

    • qualifiedOriginalsOf

      protected final List<String> qualifiedOriginalsOf(String plainElementId)
      Returns every qualified id plainElementId was merged from, following alias chains transitively.

      A composition applied to the result of another composition records a chain (a -> merged -> unified_0) rather than a flat mapping, so a one-hop lookup (qualifiedAliasesOf(String)) stops at the intermediate and loses the id the user actually wrote. The returned list holds both the intermediates and the leaves, nearest first.

    • qualifiedAuthoredOriginalsOf

      protected final List<String> qualifiedAuthoredOriginalsOf(String plainElementId)
      Returns the qualified ids plainElementId was merged from that an author actually wrote: the ids as they stood in the source models. Empty when the element is not a merge product.

      Two kinds of id are passed over. One that was merged from further ids is skipped in favour of those, which stand closer to the source. One that unification minted (unified_0) is skipped outright: it names a merged group by a counter and appears in no source file. The latter is not always the former, since composing the result of a composition can leave a minted id recorded as a sibling of the ids it stood for rather than as their parent, so being childless does not make an id authored.

    • minimalLink

      protected final String minimalLink(String qualifiedKey)
      Shortens qualifiedKey to the shortest trailing run of colon-separated segments that still designates the same element, never going below container:id.

      Consumers resolve a link by exact match against the link index first, then by strict segment-suffix match; a suffix designating two different elements is ambiguous and is not a valid link. Candidates are therefore checked against the very index a consumer builds from the exported model, shortest first, and qualifiedKey itself is returned when no shorter form is unambiguous, because a full id always resolves exactly.

      The 2-segment floor is a readability requirement rather than a resolution one: a bare id would often resolve, but a reader of the exported artefact has no way to tell what it belongs to. Keeping the owning model or source justification in front of it, as a_claim:s1 rather than s1, makes the reference legible on its own. Every key starts qualified with the model name, so the floor is always reachable.

    • visit

      public final Void visit(Unit unit)
      Rejects Unit — single-model exporters require a specific model. Use SelectModel in the compilation pipeline to extract one first.
      Specified by:
      visit in interface JustificationVisitor<Void>

    • visit

      public final Void visit(Justification justification)
      Delegates to exportModel(JustificationModel).
      Specified by:
      visit in interface JustificationVisitor<Void>

    • visit

      public final Void visit(Template template)
      Delegates to exportModel(JustificationModel).
      Specified by:
      visit in interface JustificationVisitor<Void>

    • exportModel

      protected abstract void exportModel(JustificationModel<?> model)
      Performs the actual serialisation of model. Implementations must set currentModelName= model.getName() before calling any element visit methods.