create_coverability_expression

Function create_coverability_expression 

Source
pub fn create_coverability_expression(loc_name: String) -> ELTLExpression
Expand 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