create_reachability_expression

taco_cli::cli

Function create_reachability_expression 

Source 
pub fn create_reachability_expression(
    populated_locs: Vec<String>,
    unpopulated_locs: Vec<String>,
) -> ELTLExpression
Expand description

The reachability specification looks as follows: We want to find a path from an initial configuration to a specific configuration Thus the specification looks as follows: (expression_initial) => []((pop_loc_1 = 0) || … || (pop_loc_p = 0) || (unpop_loc_1 > 0) || … || (unpop_loc_u > 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