Module spec

Defines the interface of the JSON Specification for various versions. The versions are gated using features.

The interfaces are implemented as serde-structs, which can be serialized to- and deserialized from specification-compliant JSON.

Modules

• appendix
• auxillary
  Defines practical structs that are extremely convenient and spec-compliant, but not necessary mentioned in it.
• errors
  Defines Rust errors, which are not part of the spec but generated by it.

Structs

• DomainRange
  Defines how to give a range of values as a domain for an atomic fact.
• DomainSet
  Defines how to give a set of values as a domain for an atomic fact.
• DutyDefinitionCommon
  Represents common fields for all duty-like definition phrases.
• Error
  Represents an error returned by the server.
• EventDefinitionCommon
  Represents common fields for all event-like definition phrases.
• ExpressionConstructorApp
  Defines a constructor application in eFLINT.
• ExpressionIterator
  Defines an iterator expression in eFLINT.
• ExpressionOperator
  Defines an operator application in eFLINT.
• ExpressionProjection
  Defines a type projection in eFLINT.
• ExpressionVarRef
  Represents a variable reference in eFLINT.
• PhraseAct
  Defines an automatic transition between Facts instantiated by a particular actor, e.g.,
• PhraseAtomicFact
  Represents the definition of an atomic Fact, e.g.,
• PhraseBooleanQuery
  Represents a boolean query within eFLINT, e.g.,
• PhraseCompositeFact
  Represents the definition of a composite Fact, e.g.,
• PhraseCreate
  Represents a true-postulation within eFLINT, e.g.,
• PhraseDuty
  Defines an obligation that two actors have, e.g.,
• PhraseEvent
  Defines an automatic transition between Facts, e.g.,
• PhraseExtendAct
  Defines an extension to an existing Act, e.g.,
• PhraseExtendDuty
  Defines an extension to an existing Act, e.g.,
• PhraseExtendEvent
  Defines an extension to an existing Event, e.g.,
• PhraseExtendFact
  Defines an extension to an existing Fact, e.g.,
• PhraseInstanceQuery
  Represents an instance query within eFLINT, e.g.,
• PhraseObfuscate
  Represents the removal of postulation within eFLINT, e.g.,
• PhrasePlaceholder
  Represents a Placeholder definition for Fact for e.g.,
• PhrasePredicate
  Represents a predicate that can be queried but not instantiated, e.g.,
• PhraseResultBooleanQuery
  Defines the result given by the server when a boolean query is processed.
• PhraseResultCommon
  Defines the fields common to all PhraseResult variants.
• PhraseResultInstanceQuery
  Defines the result given by the server when an instance query is processed.
• PhraseResultStateChange
  Defines state changes that are induced after executing a Phrase.
• PhraseTerminate
  Represents a false-postulation within eFLINT, e.g.,
• PhraseTrigger
  Represents the execution of an Event or Act, e.g.,
• RequestCommon
  Determines the common fields for all requests.
• RequestHandshake
  Represents a Handshake-request.
• RequestInspect
  Represents an Inspect-request.
• RequestPhrases
  Represents a Phrases-request.
• RequestPing
  Represents a Ping-request.
• ResponseCommon
  Determines the common fields for all responses.
• ResponseHandshake
  Represents the reply to a Handshake-request.
• ResponseInspect
  Represents the reply to an Inspect-request.
• ResponsePhrases
  Represents the reply to a Phrases-request.
• ResponsePing
  Represents the reply to a Ping-request.
• Trigger
  Encodes the trigger of an Event or Act that occurs when running an eFLINT spec.
• TypeDefinitionCommon
  Represents common fields for all type definition phrases.
• Violation
  Encodes a violation that occurs when running an eFLINT spec.

Enums

• ConstructorInput
  Defines the input to a constructor application.
• Domain
  Defines how to specify a closed domain of an atomic eFLINT Fact when we declare it.
• Expression
  Defines an eFLINT expression that evaluates to a value.
• ExpressionPrimitive
  Represents a primitive eFLINT type.
• Phrase
  Represents an eFLINT statement, essentially.
• PhraseExtend
  Defines an extension to an existing type, e.g.,
• PhraseResult
  Defines the execution result of a particular Phrase.
• Request
  The toplevel request of the JSON specification.