fn parse_initial_loc_constr(
pair: Pair<'_, Rule>,
builder: &InitializedGeneralThresholdAutomatonBuilder,
ctx: &mut TLAParsingContext<'_>,
) -> Result<Vec<BooleanExpression<Location>>, Error>Expand description
Parse a constraint over ProcessesLocations into the set of initial
locations
This function is meant to parse a constraint of the form
ProcessesLocations \in [Processes -> {"loc0", "loc1"}]
appearing in the initial constraints and derive the boolean expressions that
are necessary to represent the initial constraints.