parse_initial_loc_constr

Function parse_initial_loc_constr 

Source
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.