Enum Model 

pub enum Model {
    Discrete(Box<DiscreteDblModel>),
    Modal(Box<ModalDblModel>),
}

A model generated by DoubleTT.

Similarly to TheoryDef, this enum boxes the different types of models that can be generated by DoubleTT.

Variants

Discrete(Box<DiscreteDblModel>)

A model of a discrete double theory.

Modal(Box<ModalDblModel>)

A model of a modal double theory.

Implementations

impl Model

pub fn new(theory: &TheoryDef) -> Self

Constructs an empty model of a theory.

pub fn from_text(th: &TheoryDef, s: &str) -> Option<Self>

Parses and generates a model from plain text.

pub fn from_ty( toplevel: &Toplevel, th: &TheoryDef, ty: &TyV, ) -> (Self, Namespace)

Generates a model from a type.

Precondition: ty must be valid in the empty context.

pub fn as_discrete(self) -> Option<DiscreteDblModel>

Tries to extract a model of a discrete theory.

pub fn as_modal(self) -> Option<ModalDblModel>

Tries to extract a model of a modal theory.

pub fn summary(&self, printer: &DblModelPrinter) -> String

Pretty prints a summary of the model.

pub fn to_doc<'a>(&self, printer: &DblModelPrinter, ns: &Namespace) -> D<'a>

Pretty prints the model in the given namespace.