pub fn create_coverability_expression(loc_name: String) -> ELTLExpressionExpand description
The coverability specification looks as follows: We want to find a path from an initial configuration to a configuration where the location is covered Thus the specification looks as follows: (expression_initial) => [](to_be_covered_loc = 0) Since the initial configuration is coded into the ta, there is no need for the implication. A counter example to this specification is exactly the path we are looking for