mcmas.fmtk

  1"""
  2mcmas.fmtk:
  3
  4A growing formal methods toolkit. This is focused on abstract base classes
  5(pydantic models) that are intended to be useful for describing things like
  6"specifications" and "simulations" in general. Classes like ispl.Specification
  7and ispl.Simulation extend these, but the hopefully the base classes are more
  8reusable.
  9
 10This might be reused to wrap other kinds of formalisms like:
 11
 12* Other model-checkers (.. Alloy lang?)
 13* SAT & SMT Provers (.. Z3?)
 14* Constraints, Discrete-events, Systems Simulations (.. SimPy / CPMpy?)
 15* Games & Protocols, etc (.. py-mfglib?)
 16"""
 17
 18import typing
 19
 20import pydantic
 21from pydantic import Field
 22
 23from mcmas import util
 24from mcmas.typing import PathType
 25
 26LOGGER = util.get_logger(__name__)
 27
 28
 29class SpecificationMetadata(pydantic.BaseModel):
 30    """
 31    Metadata for this Specification.
 32    """
 33
 34    file: PathType = Field(
 35        description="File associated with this specification", default=None
 36    )
 37    engine: str = Field(
 38        description="The engine that will be used for this specification",
 39        default="mcmas",
 40    )
 41    parser: str = Field(
 42        description="The parser that will be used for this specification",
 43        default="mcmas.parser",
 44    )
 45
 46
 47SpecificationMetadataType = typing.Union[SpecificationMetadata, None]
 48
 49
 50class SpecificationFragment(pydantic.BaseModel):
 51    """
 52    A Fragment of a Specification.
 53
 54    NB: Fragments are incomplete by definition.
 55    """
 56
 57    logger: typing.ClassVar = LOGGER
 58    Metadata: typing.ClassVar = SpecificationMetadata
 59    metadata: SpecificationMetadata = Field(
 60        description=(
 61            "Known metadata about this Specification.\n\n"
 62            "(Updated if/when the specification is analyzed or simulated)"
 63        ),
 64        default=SpecificationMetadata(),
 65        exclude=True,
 66    )
 67
 68    @classmethod
 69    def get_trivial(kls, **kwargs):
 70        """
 71        Subclassers must implement this.
 72
 73        Returns the trivial fragment for this type.
 74        """
 75        raise NotImplementedError(f"{kls}")
 76
 77    @classmethod
 78    def load_from_source(kls, txt) -> typing.Self:
 79        """
 80        Subclassers must implement this.
 81
 82        Creates spec-fragment from raw source-code.
 83        """
 84        raise NotImplementedError(f"{kls}")
 85
 86    def model_dump_source(self) -> str:
 87        """
 88        Subclassers must implement this.
 89
 90        Dumps raw source-code for this fragment.
 91        """
 92        raise NotImplementedError(f"{self}")
 93
 94    @property
 95    def valid(self):
 96        """
 97        True if this agent is valid, i.e. ready to run and not a
 98        fragment.
 99        """
100        return not any(
101            [self.__class__.__name__ == "SpecificationFragment", self.advice]
102        )
103
104    concrete = valid
105
106    @property
107    def advice(self) -> list:
108        """
109        Returns a list of any problems with this object.
110
111        See also `valid` property
112        """
113        required = getattr(self.__class__, "REQUIRED", [])
114        if not required:
115            LOGGER.warning(
116                f"no attrs listed as required for {self}; advice unavailable"
117            )
118        return [
119            f"MISSING-REQUIRED {f} from {self.__class__.__name__}"
120            for f in required
121            if not bool(getattr(self, f))
122        ] + self.local_advice
123
124    @property
125    def local_advice(self) -> list:
126        """
127        Subclassers must implement this.
128        """
129        return []
130
131    def __add__(self, other):
132        """
133        Subclassers must implement this.
134        """
135        raise TypeError(f"Cannot add {self} and {other}")
136
137    def __and__(self, other):
138        """
139        Subclassers must implement this.
140        """
141        raise TypeError(f"Cannot `and` {self} and {other}")
142
143    def __or__(self, other):
144        """
145        Subclassers must implement this.
146        """
147        raise TypeError(f"Cannot `or` {self} and {other}")
148
149
150Fragment = SpecificationFragment
151
152
153class Specification(SpecificationFragment):
154    """
155    Pydantic models for a Specification.
156    """
157
158
159#####################
160from mcmas import typing
161
162
163class AnalysisMeta(pydantic.BaseModel):
164    """
165    Metadata for a Specification Analysis.
166    """
167
168    formula_index: int = Field(default=-1)
169    base_complexity: float = Field(default=0.0)
170    nesting_coefficient: int = Field(default=1)
171    raw_score: float = Field(default=0.0)
172
173
174class SymbolMetadata(pydantic.BaseModel):
175    """
176    Result of running ISPL Analysis.
177
178    This extracts details about symbols, namespaces, etc.
179    """
180
181    actions: typing.SymbolList2 = Field(
182        default=[],
183        description="Actions list",
184    )
185    agents: typing.SymbolList2 = Field(
186        default=[],
187        description="Agents list",
188    )
189    vars: typing.SymbolList2 = Field(
190        default=[],
191        description="Var list",
192    )
193
194
195#########################
196
197
198class SpecificationAnalysis(pydantic.BaseModel):
199    """
200    Base class for all Analysis results.
201    """