From 0d4ede499babe9fab32313c0466dc3bf1e0390eb Mon Sep 17 00:00:00 2001 From: Siddhartha Prasad Date: Mon, 8 Dec 2025 14:36:14 -0500 Subject: [PATCH 1/2] More changes --- experiments/benchmark_builder.py | 2 + experiments/exclusive_u_experiment.py | 111 -------------------------- src/codebook.py | 102 +++++++++++------------ src/spotutils.py | 57 +++++++++++++ 4 files changed, 107 insertions(+), 165 deletions(-) delete mode 100644 experiments/exclusive_u_experiment.py diff --git a/experiments/benchmark_builder.py b/experiments/benchmark_builder.py index bb92146..d8ad035 100644 --- a/experiments/benchmark_builder.py +++ b/experiments/benchmark_builder.py @@ -686,6 +686,7 @@ def main(): parser.add_argument("--max-candidates", type=int, default=5000, help="Max candidates to try") parser.add_argument("--output-prefix", default="ltl_benchmark", help="Output file prefix") parser.add_argument("--quiet", action="store_true", help="Suppress progress output") + parser.add_argument("--max-atomic-props", type=int, default=3, help="Maximum number of atomic propositions") args = parser.parse_args() @@ -695,6 +696,7 @@ def main(): far_eng_threshold=args.far_eng_threshold, min_similarity_threshold=args.min_similarity_threshold, seed=args.seed, + max_atomic_props=args.max_atomic_props, max_candidates=args.max_candidates, verbose=not args.quiet, misconception_weights=DEFAULT_MISCONCEPTION_WEIGHTS diff --git a/experiments/exclusive_u_experiment.py b/experiments/exclusive_u_experiment.py deleted file mode 100644 index 124defa..0000000 --- a/experiments/exclusive_u_experiment.py +++ /dev/null @@ -1,111 +0,0 @@ -"""Simple experiment to estimate how often random seed formulas contain -ExclusiveU or WeakU misconceptions. - -The generator intentionally keeps the grammar lightweight: literals plus a -mix of unary and binary temporal operators. We rely on the existing -`codebook.getAllApplicableMisconceptions` helper to detect whether a formula -contains a site where the ExclusiveU or WeakU mutations can apply. -""" -from __future__ import annotations - - -import sys -import os -import re -import pandas as pd -import numpy as np -from pathlib import Path -from collections import Counter -from random import randint -import random - -# Add src to path for LTL Tutor imports -sys.path.insert(0, str(Path(__file__).parent.parent / 'src')) - -from ltlnode import parse_ltl_string - - -import os -import random -import sys -from typing import List -import spot - - -# Local imports -from ltlnode import ( - LiteralNode, - NotNode, - FinallyNode, - GloballyNode, - NextNode, - UntilNode, - AndNode, - OrNode, - ImpliesNode, - LTLNode, -) -import codebook - -ATOMS = ["a", "b", "c", "p", "q", "r", "x", "y", "z"] - - -def random_literal() -> LiteralNode: - return LiteralNode(random.choice(ATOMS)) - - -def random_formula(depth: int, max_depth: int) -> LTLNode: - """Generate a random LTL formula as an AST. - - The generator balances literals, unary operators, and binary operators. - Depth is capped to avoid runaway recursion. - """ - if depth >= max_depth: - return random_literal() - - roll = random.random() - if roll < 0.25: - return random_literal() - if roll < 0.50: - op = random.choice([NotNode, FinallyNode, GloballyNode, NextNode]) - return op(random_formula(depth + 1, max_depth)) - - op = random.choice([AndNode, OrNode, ImpliesNode, UntilNode]) - return op(random_formula(depth + 1, max_depth), random_formula(depth + 1, max_depth)) - - -def has_misconception(node: LTLNode, code: codebook.MisconceptionCode) -> bool: - mutations = codebook.getAllApplicableMisconceptions(node) - return any(m.misconception == code for m in mutations) - - -def run_experiment(num_formulas: int = 100, seed: int = 42, max_depth: int = 3) -> None: - random.seed(seed) - formulas: List[LTLNode] = [random_formula(0, max_depth) for _ in range(num_formulas)] - - exclusive_hits = [] - weak_hits = [] - - for formula in formulas: - - formula = parse_ltl_string("x U (!x & y)") - - if has_misconception(formula, codebook.MisconceptionCode.ExclusiveU): - exclusive_hits.append(str(formula)) - if has_misconception(formula, codebook.MisconceptionCode.WeakU): - weak_hits.append(str(formula)) - - - - print(f"Generated {num_formulas} formulas (seed={seed}, max_depth={max_depth})") - print(f"ExclusiveU-applicable: {len(exclusive_hits)}") - for i, formula in enumerate(exclusive_hits, 1): - print(f" Exclusive example {i}: {formula}") - - print(f"WeakU-applicable: {len(weak_hits)}") - for i, formula in enumerate(weak_hits, 1): - print(f" WeakU example {i}: {formula}") - - -if __name__ == "__main__": - run_experiment() diff --git a/src/codebook.py b/src/codebook.py index 207eaac..7e40be9 100644 --- a/src/codebook.py +++ b/src/codebook.py @@ -2,6 +2,7 @@ import random from ltlnode import * import copy +import spotutils class MisconceptionCode(Enum): Precedence = "Precedence" @@ -43,75 +44,68 @@ def needsTemplateGeneration(self): def generateTemplateFormula(self, atomic_props=None): """ Generate a formula from a template that guarantees this misconception can be applied. + Uses SPOT's randltl for subformulae to avoid trivial tautologies/contradictions. Returns an LTLNode, or None if template generation is not applicable. Args: - atomic_props: List of atomic proposition strings to use. If None, uses ['p', 'q', 'r'] + atomic_props: List of atomic proposition strings to use. If None, uses ['p0', 'p1', 'p2'] """ if atomic_props is None: - atomic_props = ['p', 'q', 'r'] + atomic_props = ['p0', 'p1', 'p2'] if not self.needsTemplateGeneration(): return None - # Helper to get random distinct props - def get_props(n): - return random.sample(atomic_props, min(n, len(atomic_props))) - - def build_subformula(): + def build_subformula(tree_size=3): """ - Build a small subformula to increase structural variety beyond literals. - Combines a randomly chosen atom with a light unary or binary decoration. + Build a non-trivial subformula using SPOT's randltl via spotutils. + Returns an LTLNode. """ - chosen = get_props(2) - base = parse_ltl_string(chosen[0]) - - if random.random() < 0.55: - unary_ctor = random.choice([NotNode, FinallyNode, GloballyNode, NextNode]) - base = unary_ctor(base) - - if len(chosen) > 1 and random.random() < 0.55: - rhs = parse_ltl_string(chosen[1]) - bin_ctor = random.choice([AndNode, OrNode, ImpliesNode]) - base = bin_ctor(base, rhs) + formula_str = spotutils.gen_small_rand_ltl(atomic_props, tree_size=tree_size) + return parse_ltl_string(formula_str) - return base - - if self == MisconceptionCode.ExclusiveU: - # Generate patterns that ExclusiveU can mutate - x = build_subformula() - y = build_subformula() + # Generate template and verify it's non-trivial + max_attempts = 20 + for attempt in range(max_attempts): + template = None - patterns = [ - # x U (!x & y) - explicit disjointness - UntilNode(x, AndNode(NotNode(x), y)), - # x U (x -> y) - implication pattern - UntilNode(x, ImpliesNode(x, y)), - # x U (!x | y) - or pattern with negation - UntilNode(x, OrNode(NotNode(x), y)), - # (x U y) & G(x -> !y) - global exclusivity constraint - AndNode(UntilNode(x, y), GloballyNode(ImpliesNode(x, NotNode(y)))), - # (x U y) & G!(x & y) - globally not both - AndNode(UntilNode(x, y), GloballyNode(NotNode(AndNode(x, y)))), - ] - return random.choice(patterns) - - elif self == MisconceptionCode.BadStateIndex: - # Generate Until/Next patterns with complex RHS - x = build_subformula() - y = build_subformula() - z = build_subformula() + if self == MisconceptionCode.ExclusiveU: + # Generate patterns that ExclusiveU can mutate + x = build_subformula(tree_size=2) + y = build_subformula(tree_size=3) + + patterns = [ + # x U (!x & y) - explicit disjointness + UntilNode(x, AndNode(NotNode(x), y)), + # x U (x -> y) - implication pattern + UntilNode(x, ImpliesNode(x, y)), + # x U (!x | y) - or pattern with negation + UntilNode(x, OrNode(NotNode(x), y)), + ] + template = random.choice(patterns) + + elif self == MisconceptionCode.BadStateIndex: + # Generate Until/Next patterns with complex RHS + x = build_subformula(tree_size=2) + y = build_subformula(tree_size=2) + z = build_subformula(tree_size=2) + + patterns = [ + # x U (y & Fz) - Until with conjunction including Finally + UntilNode(x, AndNode(y, FinallyNode(z))), + # x U (y & Gz) - Until with conjunction including Globally + UntilNode(x, AndNode(y, GloballyNode(z))), + # x U X(y & z) - Until with Next of conjunction + UntilNode(x, NextNode(AndNode(y, z))), + # X(y & z) - Next with conjunction + NextNode(AndNode(y, z)), + ] + template = random.choice(patterns) - patterns = [ - # x U (y & Fz) - Until with conjunction including Finally - UntilNode(x, AndNode(y, FinallyNode(z))), - # x U (y & Gz) - Until with conjunction including Globally - UntilNode(x, AndNode(y, GloballyNode(z))), - # X(y & z) - Next with conjunction - NextNode(AndNode(y, z)), - ] - return random.choice(patterns) + if template is not None and not spotutils.is_trivial(str(template)): + return template + # If all attempts failed, return None return None def associatedOperators(self): diff --git a/src/spotutils.py b/src/spotutils.py index 1857d09..5a98eed 100644 --- a/src/spotutils.py +++ b/src/spotutils.py @@ -182,6 +182,63 @@ def to_priority_string(d): return [str(next(f)) for _ in range(num_formulae)] +def is_trivial(formula_str): + """ + Check if a formula is a tautology or contradiction using SPOT. + + Args: + formula_str: String representation of an LTL formula + + Returns: + True if the formula simplifies to constant true (1) or false (0) + """ + try: + f = spot.formula(formula_str) + # Simplify and check if it's constant true (1) or false (0) + simplified = spot.simplify(f) + simplified_str = str(simplified) + return simplified_str in ['1', '0', 'true', 'false'] + except: + return False + + +def gen_small_rand_ltl(atoms, tree_size=3, max_attempts=10): + """ + Generate a single small non-trivial random LTL formula using SPOT. + Prioritizes atomic propositions and simple operators to avoid complexity. + + Args: + atoms: List of atomic proposition strings + tree_size: Maximum tree size for the formula (default 3) + max_attempts: Maximum number of attempts to find a non-trivial formula + + Returns: + String representation of a non-trivial LTL formula, or a random atom as fallback + """ + # Prioritize simple operators, keep tree size small + priorities = { + 'ap': 5, + 'G': 2, 'F': 2, 'X': 2, 'U': 3, + 'and': 4, 'or': 4, 'implies': 3, 'not': 3, + 'equiv': 1, 'xor': 0, 'R': 0, 'W': 0, 'M': 0, + 'true': 0, 'false': 0 + } + + for _ in range(max_attempts): + try: + formulas = gen_rand_ltl(atoms, tree_size, priorities, num_formulae=1) + formula_str = formulas[0] + + # Reject trivial formulas + if not is_trivial(formula_str): + return formula_str + except: + continue + + # Fallback to a simple literal if all attempts fail + return random.choice(atoms) + + ## Returns the Mana Pneulli classification of the formula def get_mana_pneulli_class(formula): From 5179852f5e916c7d3c14e69f96adb7cfc6636ada Mon Sep 17 00:00:00 2001 From: Siddhartha Prasad Date: Mon, 8 Dec 2025 14:52:21 -0500 Subject: [PATCH 2/2] Modified benchmark and v --- semantic_benchmark_far_eng.csv | 137 +++++++++------------- semantic_benchmark_near_eng.csv | 198 ++++++++++++++++---------------- src/templates/version.html | 2 +- 3 files changed, 152 insertions(+), 185 deletions(-) diff --git a/semantic_benchmark_far_eng.csv b/semantic_benchmark_far_eng.csv index c6092f8..e9f91b9 100644 --- a/semantic_benchmark_far_eng.csv +++ b/semantic_benchmark_far_eng.csv @@ -1,101 +1,68 @@ ltl_formula,english_translation,closest_mutant_formula,closest_mutant_english,closest_mutant_misconception,closest_distance,max_distance,avg_distance,num_mutants -p3 | Gp1,Either 'p3' or 'p1' must always hold,(p3 | (F p1)),"Either 'p3' or at some point, 'p1' will hold",BadStateQuantification,0.45043107867240906,0.5518139600753784,0.4953062931696574,3 -(p0 U ((! p0) | (! p3))),'p0' until not both 'p0' and 'p3',((p0 U ((! p0) | (! p3))) | (G p0)),Either 'p0' until not both 'p0' and 'p3' or 'p0' must always hold,WeakU,0.45751529932022095,0.781352698802948,0.5453808307647705,4 -!p3 | Xp0,"Either 'p3' is false or in the next step, 'p0'",((! p3) | (F p0)),"Either 'p3' is false or at some point, 'p0' will hold",OtherImplicit,0.46314603090286255,0.46314603090286255,0.46314603090286255,1 -(p2 U ((! p2) | p2)),'p2' until either 'p2' is false or 'p2',(p2 U p2),'p2' until 'p2',ExclusiveU,0.46673595905303955,0.46673595905303955,0.46673595905303955,1 -X(p3 & FGp2),"In the next step, both 'p3' and eventually, 'p2' will always be true",(X (p3 & (F p2))),"In the next step, both 'p3' and at some point, 'p2' will hold",ImplicitG,0.46724972128868103,0.5417690873146057,0.487897090613842,4 -X((p1 & p2) | (!p1 & !p2)),"In the next step, either both 'p1' and 'p2' or neither 'p1' nor 'p2'",(X (((p1 & p2) | (! p1)) & (! p2))),"In the next step, both either both 'p1' and 'p2' or 'p1' is false and 'p2' is false",Precedence,0.49869200587272644,0.5975241661071777,0.5481080859899521,2 -F(p2 & p3),"Eventually, both 'p2' and 'p3' will be true simultaneously",(p2 & p3),Both 'p2' and 'p3',ImplicitF,0.6440837979316711,0.7360519766807556,0.6747398575146993,3 +p0 | !p1 | Xp0,"Either 'p0' or 'p1' is false or in the next step, 'p0'",((p0 | (! p1)) | (F p0)),"Either 'p0' or 'p1' is false or at some point, 'p0' will hold",OtherImplicit,0.4505925178527832,0.4505925178527832,0.4505925178527832,1 p1 | G!p0,Either 'p1' or 'p0' will never occur,(p1 | (F (! p0))),"Either 'p1' or eventually, not 'p0'",BadStateQuantification,0.4521879255771637,0.7287090420722961,0.6086266140143076,3 -p3 U p2,'p3' until 'p2',((p3 U p2) | (G p3)),Either 'p3' until 'p2' or 'p3' must always hold,WeakU,0.4602723717689514,0.616101861000061,0.5230183998743693,3 -((G p2) U ((G p2) -> (F p2))),"'p2' must always hold until if 'p2' must always hold, then at some point, 'p2' will hold",(G p2),'p2' must always hold,OtherImplicit,0.46611276268959045,0.6317513585090637,0.5489320605993271,2 -XG(p0 & p3),"In the next step, at all times, both 'p0' and 'p3' hold",(X (p0 & p3)),"In the next step, both 'p0' and 'p3'",ImplicitG,0.49857398867607117,0.5757542252540588,0.5293595294157664,3 -(p3 U (p3 -> p3)),"'p3' until if 'p3' holds, then 'p3' holds",(p3 U p3),'p3' until 'p3',ExclusiveU,0.5209833383560181,0.5209833383560181,0.5209833383560181,1 -F(p0 & p3),"Eventually, both 'p0' and 'p3' will be true simultaneously",(p0 & p3),Both 'p0' and 'p3',ImplicitF,0.6623632311820984,0.7488532662391663,0.6911932428677877,3 -p2 | Gp3,Either 'p2' or 'p3' must always hold,(p2 | (F p3)),"Either 'p2' or at some point, 'p3' will hold",BadStateQuantification,0.4526665508747101,0.741706132888794,0.588632196187973,3 -p1 U p0,'p1' until 'p0',((p1 U p0) | (G p1)),Either 'p1' until 'p0' or 'p1' must always hold,WeakU,0.46299681067466736,0.6431487202644348,0.5307719111442566,3 -!p0 & Xp3,"Both 'p0' is false and in the next step, 'p3'",((! p0) & (F p3)),"Both 'p0' is false and at some point, 'p3' will hold",OtherImplicit,0.4761523902416229,0.4761523902416229,0.4761523902416229,1 -XG(p2 & p3),"In the next step, at all times, both 'p2' and 'p3' hold",(X (p2 & p3)),"In the next step, both 'p2' and 'p3'",ImplicitG,0.5027826428413391,0.5630331635475159,0.533862849076589,3 -(p1 U (p1 -> p1)),"'p1' until if 'p1' holds, then 'p1' holds",(p1 U p1),'p1' until 'p1',ExclusiveU,0.5512495636940002,0.8403921127319336,0.6958208382129669,2 -FGp2,"Eventually, 'p2' will always be true",(G p2),'p2' must always hold,ImplicitF,0.6659942865371704,0.7746404409408569,0.6934536993503571,4 -p1 | (p1 U p2),Either 'p1' or 'p1' until 'p2',(p1 | (p1 U (F p2))),"Either 'p1' or 'p1' until at some point, 'p2' will hold",BadStateQuantification,0.4548565745353699,0.7249919772148132,0.5574564039707184,3 -!p3 | Xp3,"Either 'p3' is false or in the next step, 'p3'",((! p3) | (F p3)),"Either 'p3' is false or at some point, 'p3' will hold",OtherImplicit,0.47656193375587463,0.47656193375587463,0.47656193375587463,1 -p1 U p2,'p1' until 'p2',((p1 U p2) | (G p1)),Either 'p1' until 'p2' or 'p1' must always hold,WeakU,0.4799743890762329,0.7211152911186218,0.5797340075174967,3 -G(p1 | p2),Always have either 'p1' or 'p2',(p1 | p2),At least one of 'p1' or 'p2',ImplicitG,0.5046390295028687,0.6220009326934814,0.5437596638997396,3 -(p0 U (p0 -> p0)),"'p0' until if 'p0' holds, then 'p0' holds",(p0 U p0),'p0' until 'p0',ExclusiveU,0.5660205483436584,0.5660205483436584,0.5660205483436584,1 -F(p0 & p2),"Eventually, both 'p0' and 'p2' will be true simultaneously",(p0 & p2),Both 'p0' and 'p2',ImplicitF,0.6757736802101135,0.7607364654541016,0.7040946086247762,3 -!p2 | p3 | GFp1,Either 'p2' is false or 'p3' or 'p1' will happen infinitely often,(((! p2) | p3) | (F (F p1))),"Either 'p2' is false or 'p3' or eventually, 'p1'",BadStateQuantification,0.45498692989349365,0.5934218168258667,0.542361855506897,4 -!p1 | p3,Either 'p1' is false or 'p3',(! p1),'p1' is false,OtherImplicit,0.4804563522338867,0.4804563522338867,0.4804563522338867,1 -p0 U p1,'p0' until 'p1',((p0 U p1) | (G p0)),Either 'p0' until 'p1' or 'p0' must always hold,WeakU,0.49506258964538574,0.7117910385131836,0.5696965654691061,3 -XG(p1 & p2),"In the next step, at all times, both 'p1' and 'p2' hold",(X (p1 & p2)),"In the next step, both 'p1' and 'p2'",ImplicitG,0.5117736458778381,0.5819584727287292,0.5519059896469116,3 +(p0 & F!p0) U p1,"Both 'p0' and eventually, not 'p0' hold until 'p1'",((p0 & (! p0)) U p1),Both 'p0' and 'p0' is false hold until 'p1',ImplicitF,0.4571964144706726,0.5160290002822876,0.49541393915812176,3 +p1 U p0,'p1' until 'p0',((p1 U p0) | (G p1)),Either 'p1' until 'p0' or 'p1' must always hold,WeakU,0.46299681067466736,0.7936521172523499,0.5941601892312368,3 +X(p0 & FGp1),"In the next step, both 'p0' and eventually, 'p1' will always be true",(X (p0 & (F p1))),"In the next step, both 'p0' and at some point, 'p1' will hold",ImplicitG,0.4759460687637329,0.529869019985199,0.49311330169439316,4 +X((p0 & p1) | (!p0 & !p1)),"In the next step, either both 'p0' and 'p1' or neither 'p0' nor 'p1'",(X (((p0 & p1) | (! p0)) & (! p1))),"In the next step, both either both 'p0' and 'p1' or 'p0' is false and 'p1' is false",Precedence,0.48475202918052673,0.5904891490936279,0.5376205891370773,2 +p1 | F!p0,"Either 'p1' or eventually, not 'p0'",(p1 | (G (! p0))),Either 'p1' or 'p0' will never occur,BadStateQuantification,0.4521879255771637,0.6004613041877747,0.5159396231174469,3 +!p0 | Xp1,"Either 'p0' is false or in the next step, 'p1'",((! p0) | (F p1)),"Either 'p0' is false or at some point, 'p1' will hold",OtherImplicit,0.47501397132873535,0.47501397132873535,0.47501397132873535,1 +G(p0 | p1),Always have either 'p0' or 'p1',(p0 | p1),At least one of 'p0' or 'p1',ImplicitG,0.5075837969779968,0.6178237795829773,0.5443304578463236,3 +(!p0 & !p1) U p1,Neither 'p0' nor 'p1' hold until 'p1',((((! p0) & (! p1)) U p1) | (G ((! p0) & (! p1)))),Either neither 'p0' nor 'p1' hold until 'p1' or always maintain both 'p0' is false and 'p1' is false,WeakU,0.5151694416999817,0.7312856316566467,0.65437384446462,3 +F(p1 & Fp0),"Eventually, both 'p1' and at some point, 'p0' will hold will be true simultaneously",(p1 & (F p0)),"Both 'p1' and at some point, 'p0' will hold",ImplicitF,0.5874497890472412,0.5934363603591919,0.5894453128178915,3 +F!p0 & Xp0,"Both eventually, not 'p0' and in the next step, 'p0'",((G (! p0)) & (X p0)),"Both 'p0' will never occur and in the next step, 'p0'",BadStateQuantification,0.4558142423629761,0.5417894124984741,0.5099705457687378,3 +!p1 | Xp0,"Either 'p1' is false or in the next step, 'p0'",((! p1) | (F p0)),"Either 'p1' is false or at some point, 'p0' will hold",OtherImplicit,0.4832385778427124,0.4832385778427124,0.4832385778427124,1 +FG(p0 | p1),"Eventually, at least one of 'p0' or 'p1' will always be true",(F (p0 | p1)),"Eventually, at least one of 'p0' or 'p1'",ImplicitG,0.5241556763648987,0.7763866782188416,0.6962777078151703,4 +p1 | FGp1,"Either 'p1' or eventually, 'p1' will always be true",(p1 | (G p1)),Either 'p1' or 'p1' must always hold,ImplicitF,0.6364479660987854,0.7268989682197571,0.6647939532995224,4 +p1 | G!p1,Either 'p1' or 'p1' will never occur,(p1 | (F (! p1))),"Either 'p1' or eventually, not 'p1'",BadStateQuantification,0.46807342767715454,0.7174451947212219,0.6148241559664408,3 +(p0 & Xp1) U p1,"Both 'p0' and in the next step, 'p1' hold until 'p1'",((p0 & (F p1)) U p1),"Both 'p0' and at some point, 'p1' will hold until 'p1'",OtherImplicit,0.48519712686538696,0.5217308402061462,0.5034639835357666,2 +G(p0 & p1),"At all times, both 'p0' and 'p1' hold",(p0 & p1),Both 'p0' and 'p1',ImplicitG,0.6399862766265869,0.7655901908874512,0.681854248046875,3 F(p0 & p1),"Eventually, both 'p0' and 'p1' will be true simultaneously",(p0 & p1),Both 'p0' and 'p1',ImplicitF,0.6860395073890686,0.7655901908874512,0.7125564018885294,3 -p3 | G!p3,Either 'p3' or 'p3' will never occur,(p3 | (F (! p3))),"Either 'p3' or eventually, not 'p3'",BadStateQuantification,0.4570067822933197,0.6578147411346436,0.571741650501887,3 -X(p0 | !p1 | !p2 | p3),"In the next step, either either 'p0' or 'p1' is false or 'p2' is false or 'p3'",(F (((p0 | (! p1)) | (! p2)) | p3)),"Eventually, either either 'p0' or 'p1' is false or 'p2' is false or 'p3'",OtherImplicit,0.5055903196334839,0.5055903196334839,0.5055903196334839,1 -G(p1 & p3),"At all times, both 'p1' and 'p3' hold",(p1 & p3),Both 'p1' and 'p3',ImplicitG,0.6503925323486328,0.7537016868591309,0.6848289171854655,3 -p3 & G!p2,Both 'p3' and 'p2' will never occur,(p3 & (F (! p2))),"Both 'p3' and eventually, not 'p2'",BadStateQuantification,0.46759116649627686,0.5926995873451233,0.5327227910359701,3 -((G p3) U (p3 & (G ((! p3) -> p2)))),'p3' must always hold until both 'p3' and it is always the case that 'p2' unless 'p3',(G p3),'p3' must always hold,OtherImplicit,0.5538555383682251,0.5538555383682251,0.5538555383682251,1 +!p1 | Xp1,"Either 'p1' is false or in the next step, 'p1'",((! p1) | (F p1)),"Either 'p1' is false or at some point, 'p1' will hold",OtherImplicit,0.48659685254096985,0.48659685254096985,0.48659685254096985,1 +!p1 | GFp0,Either 'p1' is false or 'p0' will happen infinitely often,((! p1) | (F (F p0))),"Either 'p1' is false or eventually, 'p0'",BadStateQuantification,0.509462833404541,0.6672589182853699,0.608925998210907,4 FGp1,"Eventually, 'p1' will always be true",(F p1),"At some point, 'p1' will hold",ImplicitG,0.6717284917831421,0.8013848066329956,0.7046237289905548,4 -!p3 | GFp1,Either 'p3' is false or 'p1' will happen infinitely often,((! p3) | (F (F p1))),"Either 'p3' is false or eventually, 'p1'",BadStateQuantification,0.47198814153671265,0.632379949092865,0.5645895153284073,4 -p1 & p2,Both 'p1' and 'p2',p1,'p1',OtherImplicit,0.5831860303878784,0.5831860303878784,0.5831860303878784,1 -FGp3,"Eventually, 'p3' will always be true",(F p3),"At some point, 'p3' will hold",ImplicitG,0.6736251711845398,0.7966910004615784,0.7063409090042114,4 -p1 & F!p2,"Both 'p1' and eventually, not 'p2'",(p1 & (G (! p2))),Both 'p1' and 'p2' will never occur,BadStateQuantification,0.47616830468177795,0.685285747051239,0.6001089910666147,3 -X(p0 | !p1),"In the next step, either 'p0' or 'p1' is false",(F (p0 | (! p1))),"Eventually, either 'p0' or 'p1' is false",OtherImplicit,0.595894992351532,0.595894992351532,0.595894992351532,1 -G(p1 & p2),"At all times, both 'p1' and 'p2' hold",(p1 & p2),Both 'p1' and 'p2',ImplicitG,0.6804438829421997,0.7751515507698059,0.7120131055514017,3 -F!p3,"Eventually, not 'p3'",(G (! p3)),'p3' will never occur,BadStateQuantification,0.49604660272598267,0.6771801710128784,0.6168023149172465,3 -p0 & p3,Both 'p0' and 'p3',p3,'p3',OtherImplicit,0.5999793410301208,0.5999793410301208,0.5999793410301208,1 -G!p3,'p3' will never occur,(F (! p3)),"Eventually, not 'p3'",BadStateQuantification,0.49604660272598267,0.6052417159080505,0.5688433448473612,3 -FGp0,"Eventually, 'p0' will always be true",(F p0),"At some point, 'p0' will hold",ImplicitG,0.7481658458709717,0.8434385061264038,0.7759364545345306,4 -p2 & p3,Both 'p2' and 'p3',p2,'p2',OtherImplicit,0.6012242436408997,0.6012242436408997,0.6012242436408997,1 -p0 U p2,'p0' until 'p2',((F p0) U p2),"At some point, 'p0' will hold until 'p2'",BadStateQuantification,0.49832701683044434,0.746719241142273,0.5830078721046448,3 -p0 | p1,At least one of 'p0' or 'p1',p1,'p1',OtherImplicit,0.6131643652915955,0.6131643652915955,0.6131643652915955,1 -Fp3,"At some point, 'p3' will hold",(G p3),'p3' must always hold,BadStateQuantification,0.498857319355011,0.6736803650856018,0.6154060165087382,3 -p1 | p3 | Xp1,"Either at least one of 'p1' or 'p3' or in the next step, 'p1'",((p1 | p3) | (F p1)),"Either at least one of 'p1' or 'p3' or at some point, 'p1' will hold",OtherImplicit,0.6208100914955139,0.6208100914955139,0.6208100914955139,1 -Gp3,'p3' must always hold,(F p3),"At some point, 'p3' will hold",BadStateQuantification,0.498857319355011,0.5874304175376892,0.5579060514767965,3 -p0 | p3,At least one of 'p0' or 'p3',p3,'p3',OtherImplicit,0.6339837312698364,0.6339837312698364,0.6339837312698364,1 -Fp2,"At some point, 'p2' will hold",(G p2),'p2' must always hold,BadStateQuantification,0.5048030018806458,0.6781956553459167,0.6203981041908264,3 -!p2,'p2' is false,p2,'p2',OtherImplicit,0.6409874558448792,0.6409874558448792,0.6409874558448792,1 -Gp2,'p2' must always hold,(F p2),"At some point, 'p2' will hold",BadStateQuantification,0.5048030018806458,0.5831425189971924,0.5570293466250101,3 -!p3,'p3' is false,p3,'p3',OtherImplicit,0.6421687602996826,0.6421687602996826,0.6421687602996826,1 -G!p2,'p2' will never occur,(F (! p2)),"Eventually, not 'p2'",BadStateQuantification,0.5071642994880676,0.6483583450317383,0.601293663183848,3 -p0 | p2 | Xp2,"Either at least one of 'p0' or 'p2' or in the next step, 'p2'",((p0 | p2) | (F p2)),"Either at least one of 'p0' or 'p2' or at some point, 'p2' will hold",OtherImplicit,0.6449719667434692,0.6449719667434692,0.6449719667434692,1 -F!p2,"Eventually, not 'p2'",(G (! p2)),'p2' will never occur,BadStateQuantification,0.5071642994880676,0.6714813709259033,0.6167090137799581,3 -p3 | X!p3,"Either 'p3' or in the next step, 'p3' is false",(p3 | (F (! p3))),"Either 'p3' or eventually, not 'p3'",OtherImplicit,0.6540914177894592,0.6540914177894592,0.6540914177894592,1 +!p0 & Xp1,"Both 'p0' is false and in the next step, 'p1'",((! p0) & (F p1)),"Both 'p0' is false and at some point, 'p1' will hold",OtherImplicit,0.4875878095626831,0.4875878095626831,0.4875878095626831,1 F!p0,"Eventually, not 'p0'",(G (! p0)),'p0' will never occur,BadStateQuantification,0.5171661376953125,0.6988669633865356,0.6383000214894613,3 -!p1,'p1' is false,p1,'p1',OtherImplicit,0.6591484546661377,0.6591484546661377,0.6591484546661377,1 +FGp0,"Eventually, 'p0' will always be true",(F p0),"At some point, 'p0' will hold",ImplicitG,0.7481658458709717,0.8434385061264038,0.7759364545345306,4 +!p0 & X!p0,"Both 'p0' is false and in the next step, 'p0' is false",((! p0) & (F (! p0))),"Both 'p0' is false and eventually, not 'p0'",OtherImplicit,0.4930298924446106,0.4930298924446106,0.4930298924446106,1 G!p0,'p0' will never occur,(F (! p0)),"Eventually, not 'p0'",BadStateQuantification,0.5171661376953125,0.701252281665802,0.6398902336756388,3 -X(p0 | p2),"In the next step, at least one of 'p0' or 'p2'",(F (p0 | p2)),"Eventually, at least one of 'p0' or 'p2'",OtherImplicit,0.667004406452179,0.667004406452179,0.667004406452179,1 +!p0 | Xp0,"Either 'p0' is false or in the next step, 'p0'",((! p0) | (F p0)),"Either 'p0' is false or at some point, 'p0' will hold",OtherImplicit,0.5122258067131042,0.5122258067131042,0.5122258067131042,1 Fp1,"At some point, 'p1' will hold",(G p1),'p1' must always hold,BadStateQuantification,0.5173208117485046,0.6866223216056824,0.6301884849866232,3 Gp1,'p1' must always hold,(F p1),"At some point, 'p1' will hold",BadStateQuantification,0.5173208117485046,0.6117421984672546,0.580268402894338,3 -!p0,'p0' is false,p0,'p0',OtherImplicit,0.6832073926925659,0.6832073926925659,0.6832073926925659,1 -F!p1,"Eventually, not 'p1'",(G (! p1)),'p1' will never occur,BadStateQuantification,0.518254280090332,0.6831350326538086,0.6281747817993164,3 -p2 | X!p2,"Either 'p2' or in the next step, 'p2' is false",(p2 | (F (! p2))),"Either 'p2' or eventually, not 'p2'",OtherImplicit,0.6898571848869324,0.6898571848869324,0.6898571848869324,1 +p0 & p1,Both 'p0' and 'p1',p1,'p1',OtherImplicit,0.562502920627594,0.562502920627594,0.562502920627594,1 G!p1,'p1' will never occur,(F (! p1)),"Eventually, not 'p1'",BadStateQuantification,0.518254280090332,0.6784943342208862,0.6250809828440348,3 -p2 & Xp3,"Both 'p2' and in the next step, 'p3'",(p2 & (F p3)),"Both 'p2' and at some point, 'p3' will hold",OtherImplicit,0.6917235851287842,0.6917235851287842,0.6917235851287842,1 +X(!p0 | p1),"In the next step, either 'p0' is false or 'p1'",(F ((! p0) | p1)),"Eventually, either 'p0' is false or 'p1'",OtherImplicit,0.5777229070663452,0.5777229070663452,0.5777229070663452,1 +F!p1,"Eventually, not 'p1'",(G (! p1)),'p1' will never occur,BadStateQuantification,0.518254280090332,0.6831350326538086,0.6281747817993164,3 +X(p0 | !p1),"In the next step, either 'p0' or 'p1' is false",(F (p0 | (! p1))),"Eventually, either 'p0' or 'p1' is false",OtherImplicit,0.595894992351532,0.595894992351532,0.595894992351532,1 Fp0,"At some point, 'p0' will hold",(G p0),'p0' must always hold,BadStateQuantification,0.5208287835121155,0.7393346428871155,0.6664993564287821,3 -p1 | p2,At least one of 'p1' or 'p2',p2,'p2',OtherImplicit,0.7012022137641907,0.7012022137641907,0.7012022137641907,1 +p0 | p1 | Xp1,"Either at least one of 'p0' or 'p1' or in the next step, 'p1'",((p0 | p1) | (F p1)),"Either at least one of 'p0' or 'p1' or at some point, 'p1' will hold",OtherImplicit,0.6310442090034485,0.6310442090034485,0.6310442090034485,1 Gp0,'p0' must always hold,(F p0),"At some point, 'p0' will hold",BadStateQuantification,0.5208287835121155,0.6559706330299377,0.6109233498573303,3 -p3 | Xp3,"Either 'p3' or in the next step, 'p3'",(p3 | (F p3)),"Either 'p3' or at some point, 'p3' will hold",OtherImplicit,0.7160053849220276,0.7160053849220276,0.7160053849220276,1 -F(p3 & Fp1),"Eventually, both 'p3' and at some point, 'p1' will hold will be true simultaneously",(G (p3 & (F p1))),"At all times, both 'p3' and at some point, 'p1' will hold",BadStateQuantification,0.5369850397109985,0.5416533350944519,0.5400972366333008,3 +p0 | X!p1,"Either 'p0' or in the next step, 'p1' is false",(p0 | (F (! p1))),"Either 'p0' or eventually, not 'p1'",OtherImplicit,0.6349679231643677,0.6349679231643677,0.6349679231643677,1 +GFp0 U p0,'p0' will happen infinitely often until 'p0',((G (F p0)) U (F p0)),"At all times at some point, 'p0' will hold, and this continues until eventually 'p0' occurs",BadStateQuantification,0.5223342776298523,0.8279346823692322,0.6521279513835907,4 +p1 | X!p0,"Either 'p1' or in the next step, 'p0' is false",(p1 | (F (! p0))),"Either 'p1' or eventually, not 'p0'",OtherImplicit,0.6586194634437561,0.6586194634437561,0.6586194634437561,1 +F(p1 & ((!p0 & !p1) | (p0 & p1))),"Eventually, both 'p1' and either neither 'p0' nor 'p1' or both 'p0' and 'p1' will be true simultaneously",(G (p1 & (((! p0) & (! p1)) | (p0 & p1)))),Always maintain both 'p1' and either neither 'p0' nor 'p1' or both 'p0' and 'p1',BadStateQuantification,0.5612719058990479,0.5640279650688171,0.563109278678894,3 +!p1,'p1' is false,p1,'p1',OtherImplicit,0.6591484546661377,0.6591484546661377,0.6591484546661377,1 +p1 & FGp1,"Both 'p1' and eventually, 'p1' will always be true",(p1 & (G (G p1))),"Both 'p1' and at all times, 'p1'",BadStateQuantification,0.6257264018058777,0.7601434588432312,0.6638139933347702,4 +X(p0 | p1),"In the next step, at least one of 'p0' or 'p1'",(F (p0 | p1)),"Eventually, at least one of 'p0' or 'p1'",OtherImplicit,0.6717126965522766,0.6717126965522766,0.6717126965522766,1 +p0 | FGp1,"Either 'p0' or eventually, 'p1' will always be true",(p0 | (G (G p1))),"Either 'p0' or at all times, 'p1'",BadStateQuantification,0.6502596139907837,0.8300031423568726,0.6966247260570526,4 +p0 | X!p0,"Either 'p0' or in the next step, 'p0' is false",(p0 | (F (! p0))),"Either 'p0' or eventually, not 'p0'",OtherImplicit,0.6763193011283875,0.6763193011283875,0.6763193011283875,1 +p1 | FGp0,"Either 'p1' or eventually, 'p0' will always be true",(p1 | (G (G p0))),"Either 'p1' or at all times, 'p0'",BadStateQuantification,0.6502671837806702,0.7417636513710022,0.6838897317647934,4 +!p0,'p0' is false,p0,'p0',OtherImplicit,0.6832073926925659,0.6832073926925659,0.6832073926925659,1 +GFp1,'p1' will happen infinitely often,(F (F p1)),"Eventually, 'p1'",BadStateQuantification,0.695120632648468,0.7743967175483704,0.7534150779247284,4 +p0 | p1,At least one of 'p0' or 'p1',p0,'p0',OtherImplicit,0.701449990272522,0.701449990272522,0.701449990272522,1 +p0 | FGp0,"Either 'p0' or eventually, 'p0' will always be true",(p0 | (G (G p0))),"Either 'p0' or at all times, 'p0'",BadStateQuantification,0.6959380507469177,0.776573121547699,0.7269381731748581,4 p0 | Xp1,"Either 'p0' or in the next step, 'p1'",(p0 | (F p1)),"Either 'p0' or at some point, 'p1' will hold",OtherImplicit,0.716743528842926,0.716743528842926,0.716743528842926,1 -p0 | Xp2,"Either 'p0' or in the next step, 'p2'",(p0 | (F p2)),"Either 'p0' or at some point, 'p2' will hold",OtherImplicit,0.7250054478645325,0.7250054478645325,0.7250054478645325,1 -p2 & FGp3,"Both 'p2' and eventually, 'p3' will always be true",(p2 & (G (G p3))),"Both 'p2' and at all times, 'p3'",BadStateQuantification,0.5996398329734802,0.7897274494171143,0.6651566028594971,4 -!p0 | p3,Either 'p0' is false or 'p3',p3,'p3',OtherImplicit,0.7462073564529419,0.7462073564529419,0.7462073564529419,1 -p2 | FGp3,"Either 'p2' or eventually, 'p3' will always be true",(p2 | (G (G p3))),"Either 'p2' or at all times, 'p3'",BadStateQuantification,0.6310169696807861,0.7770109176635742,0.6712877005338669,4 +GFp0,'p0' will happen infinitely often,(F (F p0)),"Eventually, 'p0'",BadStateQuantification,0.6987221240997314,0.8137977123260498,0.775435209274292,4 +p1 & ((!p0 & !p1) | (p0 & p1)),Both 'p1' and either neither 'p0' nor 'p1' or both 'p0' and 'p1',p1,'p1',OtherImplicit,0.7177761793136597,0.7177761793136597,0.7177761793136597,1 +p0 & Xp0,"Both 'p0' and in the next step, 'p0'",(p0 & (F p0)),"Both 'p0' and at some point, 'p0' will hold",OtherImplicit,0.7273707389831543,0.7273707389831543,0.7273707389831543,1 +p1 & Xp0,"Both 'p1' and in the next step, 'p0'",(p1 & (F p0)),"Both 'p1' and at some point, 'p0' will hold",OtherImplicit,0.727513313293457,0.727513313293457,0.727513313293457,1 +p1 & Xp1,"Both 'p1' and in the next step, 'p1'",(p1 & (F p1)),"Both 'p1' and at some point, 'p1' will hold",OtherImplicit,0.7421839833259583,0.7421839833259583,0.7421839833259583,1 +!p0 | p1,Either 'p0' is false or 'p1',p1,'p1',OtherImplicit,0.7422010898590088,0.7422010898590088,0.7422010898590088,1 +p1 | Xp0,"Either 'p1' or in the next step, 'p0'",(p1 | (F p0)),"Either 'p1' or at some point, 'p0' will hold",OtherImplicit,0.7488872408866882,0.7488872408866882,0.7488872408866882,1 p0 | Xp0,"Either 'p0' or in the next step, 'p0'",(p0 | (F p0)),"Either 'p0' or at some point, 'p0' will hold",OtherImplicit,0.7491868138313293,0.7491868138313293,0.7491868138313293,1 -p0 | FGp2,"Either 'p0' or eventually, 'p2' will always be true",(p0 | (G (G p2))),"Either 'p0' or at all times, 'p2'",BadStateQuantification,0.6483875513076782,0.8493967056274414,0.7040949761867523,4 -X!p3,"In the next step, 'p3' is false",(F (! p3)),"Eventually, not 'p3'",OtherImplicit,0.7590113878250122,0.7590113878250122,0.7590113878250122,1 -GFp3,'p3' will happen infinitely often,(F (F p3)),"Eventually, 'p3'",BadStateQuantification,0.6577970385551453,0.738743245601654,0.7151447683572769,4 -p2 | Xp2,"Either 'p2' or in the next step, 'p2'",(p2 | (F p2)),"Either 'p2' or at some point, 'p2' will hold",OtherImplicit,0.7597582340240479,0.7597582340240479,0.7597582340240479,1 -GFp2,'p2' will happen infinitely often,(F (F p2)),"Eventually, 'p2'",BadStateQuantification,0.6619113683700562,0.7502215504646301,0.725648507475853,4 p1 | Xp1,"Either 'p1' or in the next step, 'p1'",(p1 | (F p1)),"Either 'p1' or at some point, 'p1' will hold",OtherImplicit,0.7647441029548645,0.7647441029548645,0.7647441029548645,1 -GFp1,'p1' will happen infinitely often,(F (F p1)),"Eventually, 'p1'",BadStateQuantification,0.695120632648468,0.7743967175483704,0.7534150779247284,4 -p1 | !p2,Either 'p1' or 'p2' is false,p1,'p1',OtherImplicit,0.7699452042579651,0.7699452042579651,0.7699452042579651,1 -GFp0,'p0' will happen infinitely often,(F (F p0)),"Eventually, 'p0'",BadStateQuantification,0.6987221240997314,0.8137977123260498,0.775435209274292,4 -p1 | !p3,Either 'p1' or 'p3' is false,p1,'p1',OtherImplicit,0.7796639800071716,0.7796639800071716,0.7796639800071716,1 -X!p2,"In the next step, 'p2' is false",(F (! p2)),"Eventually, not 'p2'",OtherImplicit,0.7816904783248901,0.7816904783248901,0.7816904783248901,1 -!p0 & p3,Both 'p0' is false and 'p3',p3,'p3',OtherImplicit,0.7827446460723877,0.7827446460723877,0.7827446460723877,1 X!p1,"In the next step, 'p1' is false",(F (! p1)),"Eventually, not 'p1'",OtherImplicit,0.7882987260818481,0.7882987260818481,0.7882987260818481,1 X!p0,"In the next step, 'p0' is false",(F (! p0)),"Eventually, not 'p0'",OtherImplicit,0.8068245053291321,0.8068245053291321,0.8068245053291321,1 -Xp3,"In the next step, 'p3'",(F p3),"At some point, 'p3' will hold",OtherImplicit,0.8077911734580994,0.8077911734580994,0.8077911734580994,1 -Xp2,"In the next step, 'p2'",(F p2),"At some point, 'p2' will hold",OtherImplicit,0.8097606897354126,0.8097606897354126,0.8097606897354126,1 -p0 | !p2,Either 'p0' or 'p2' is false,p0,'p0',OtherImplicit,0.8130448460578918,0.8130448460578918,0.8130448460578918,1 +p0 | !p1,Either 'p0' or 'p1' is false,p0,'p0',OtherImplicit,0.816491425037384,0.816491425037384,0.816491425037384,1 +Xp1,"In the next step, 'p1'",(F p1),"At some point, 'p1' will hold",OtherImplicit,0.8330647945404053,0.8330647945404053,0.8330647945404053,1 +Xp0,"In the next step, 'p0'",(F p0),"At some point, 'p0' will hold",OtherImplicit,0.8539109230041504,0.8539109230041504,0.8539109230041504,1 diff --git a/semantic_benchmark_near_eng.csv b/semantic_benchmark_near_eng.csv index e54a594..bab9856 100644 --- a/semantic_benchmark_near_eng.csv +++ b/semantic_benchmark_near_eng.csv @@ -1,101 +1,101 @@ ltl_formula,english_translation,closest_mutant_formula,closest_mutant_english,closest_mutant_misconception,closest_distance,max_distance,avg_distance,num_mutants -(p0 U p1) & (p1 U p0),Both 'p0' until 'p1' and 'p1' until 'p0',((p0 U p1) & (p0 U p1)),Both 'p0' until 'p1' and 'p0' until 'p1',BadStateQuantification,0.023236310109496117,0.387821763753891,0.27713817497715354,4 -(Fp2 & X(p1 | !p3)) | (G!p2 & X(!p1 & p3)),"Either both at some point, 'p2' will hold and in the next step, either 'p1' or 'p3' is false or both 'p2' will never occur and in the next step, both 'p1' is false and 'p3'",(((F p2) & (X (p1 | (! p3)))) | ((G (! p2)) & ((X (! p1)) & p3))),"Either both at some point, 'p2' will hold and in the next step, either 'p1' or 'p3' is false or both 'p2' will never occur and both in the next step, 'p1' is false and 'p3'",BadStateIndex,0.02979588322341442,0.3414227068424225,0.19458286557346582,6 -(X (((G p2) & p0) & ((X p2) | p1))),"In the next step, both 'p2' must always hold and 'p0' and either in the next step, 'p2' or 'p1'",(X ((((G p2) & p0) & (X p2)) | p1)),"In the next step, either both 'p2' must always hold and 'p0' and in the next step, 'p2' or 'p1'",Precedence,0.033475689589977264,0.4500802159309387,0.296018673107028,4 -(((F p3) -> p2) U ((G p2) & (G ((G p1) | p0)))),"If at some point, 'p3' will hold, then 'p2' holds until both 'p2' must always hold and always have either 'p1' must always hold or 'p0'",(((F p3) -> p2) U ((G p2) & ((G p1) | p0))),"If at some point, 'p3' will hold, then 'p2' holds until both 'p2' must always hold and either 'p1' must always hold or 'p0'",ImplicitG,0.05513975769281387,0.4693278670310974,0.20608597621321678,6 -((((F p2) -> p3) U (p2 -> p1)) & (G (! (((F p2) -> p3) & (p2 -> p1))))),"Both if at some point, 'p2' will hold, then 'p3' until if 'p2' holds, then 'p1' holds and it is never the case that both if at some point, 'p2' will hold, then 'p3' and if 'p2', then 'p1' holds",((((F p2) -> p3) U (p2 -> p1)) & (G (! ((p2 -> p3) & (p2 -> p1))))),"Both if at some point, 'p2' will hold, then 'p3' until if 'p2' holds, then 'p1' holds and it is never the case that both if 'p2', then 'p3' and if 'p2' holds, then 'p1' holds",ImplicitF,0.077869713306427,0.2907422184944153,0.17991345801523753,7 -(((p2 | p3) U ((! p0) -> p1)) & (G ((p2 | p3) -> (! ((! p0) -> p1))))),"Both at least one of 'p2' or 'p3' hold until 'p1' unless 'p0' and if at least one of 'p2' or 'p3', then not 'p1' unless 'p0' is always true",((((p2 | p3) U ((! p0) -> p1)) | (G (p2 | p3))) & (G ((p2 | p3) -> (! ((! p0) -> p1))))),"Both either at least one of 'p2' or 'p3' hold until 'p1' unless 'p0' or always have either 'p2' or 'p3' and if at least one of 'p2' or 'p3', then not 'p1' unless 'p0' is always true",WeakU,0.10272090882062912,0.42701253294944763,0.2642976976931095,6 -G(FGp3 U p3),"Eventually, 'p3' will always be true until 'p3' is always true",((F (G p3)) U p3),"Eventually, 'p3' will always be true until 'p3'",OtherImplicit,0.11623762547969818,0.4842790961265564,0.27479931712150574,4 -((! p3) U ((! (! p3)) & (p2 | p3))),'p3' is false until both 'p3' and at least one of 'p2' or 'p3',((! p3) U (p2 | p3)),'p3' is false until at least one of 'p2' or 'p3',ExclusiveU,0.12543898820877075,0.46455007791519165,0.24368559196591377,4 -(p0 U p3) | (p1 U p3),Either 'p0' until 'p3' or 'p1' until 'p3',((p0 U p3) | (p3 U p1)),Either 'p0' until 'p3' or 'p3' until 'p1',BadStateQuantification,0.02593476139008999,0.4019530117511749,0.2798178284429014,4 -(Fp0 U p1) U (p2 U p0),"At some point, 'p0' will hold until 'p1', and this continues until 'p2' until 'p0'",((((F p0) U p1) U p2) U p0),"At some point, 'p0' will hold until 'p1' until 'p2', and this continues until 'p0'",Precedence,0.03628356382250786,0.3988723158836365,0.27059474512934684,5 -X(G!p3 | X(!p0 & G!p2)),"In the next step, either 'p3' will never occur or in the next step, both 'p0' is false and 'p2' will never occur",(X ((G (! p3)) | ((X (! p0)) & (G (! p2))))),"In the next step, either 'p3' will never occur or both in the next step, 'p0' is false and 'p2' will never occur",BadStateIndex,0.055499814450740814,0.28529950976371765,0.1977731455117464,4 -(((F p2) U (p1 -> p0)) & (G ((F p2) -> (! (p1 -> p0))))),"Both at some point, 'p2' will hold until if 'p1', then 'p0' holds and at all times, if at some point, 'p2' will hold, then not if 'p1', then 'p0'",(((F p2) U (p1 -> p0)) & ((F p2) -> (! (p1 -> p0)))),"Both at some point, 'p2' will hold until if 'p1', then 'p0' holds and if at some point, 'p2' will hold, then not if 'p1', then 'p0'",ImplicitG,0.06012389808893204,0.34225183725357056,0.18971148026841028,7 -(p2 U ((p0 -> p3) & (F ((F p0) -> p3)))),"'p2' until both if 'p0' holds, then 'p3' holds and eventually, if at some point, 'p0' will hold, then 'p3' holds",(p2 U ((p0 -> p3) & ((F p0) -> p3))),"'p2' until both if 'p0' holds, then 'p3' holds and if at some point, 'p0' will hold, then 'p3' holds",ImplicitF,0.08821691572666168,0.3291768729686737,0.2209063172340393,4 -((((F p3) | p1) U (F p3)) & (G (((F p3) | p1) -> (! (F p3))))),"Both either at some point, 'p3' will hold or 'p1' hold until at some point, 'p3' will hold and at all times, if either at some point, 'p3' will hold or 'p1', then not at some point, 'p3' will hold",(((((F p3) | p1) U (F p3)) | (G ((F p3) | p1))) & (G (((F p3) | p1) -> (! (F p3))))),"Both either at some point, 'p3' will hold or 'p1' hold until at some point, 'p3' will hold or always have either at some point, 'p3' will hold or 'p1' and at all times, if either at some point, 'p3' will hold or 'p1', then not at some point, 'p3' will hold",WeakU,0.10320486128330231,0.2763770818710327,0.21865300834178925,3 -G(FGp3 U p2),"Eventually, 'p3' will always be true until 'p2' is always true",((F (G p3)) U p2),"Eventually, 'p3' will always be true until 'p2'",OtherImplicit,0.11845925450325012,0.4850548803806305,0.3048924088478088,5 -((! p2) U ((! (! p2)) | (p0 -> p1))),"'p2' is false until either 'p2' or if 'p0' holds, then 'p1' holds",((! p2) U (p0 -> p1)),"'p2' is false until if 'p0' holds, then 'p1' holds",ExclusiveU,0.14683017134666443,0.47526925802230835,0.28169373273849485,5 -Xp0 & (p3 U p2),"Both in the next step, 'p0' and 'p3' until 'p2'",((X p0) & (p2 U p3)),"Both in the next step, 'p0' and 'p2' until 'p3'",BadStateQuantification,0.032083041965961456,0.5398684740066528,0.31490558572113514,4 -XX((!p0 & ((p0 & p3) | (!p0 & !p3))) | (p0 & ((p0 & !p3) | (!p0 & p3)))),"In 2 steps, either both 'p0' is false and either both 'p0' and 'p3' or neither 'p0' nor 'p3' or both 'p0' and either both 'p0' and 'p3' is false or both 'p0' is false and 'p3'",(X (X ((((! p0) & ((p0 & p3) | ((! p0) & (! p3)))) | p0) & ((p0 & (! p3)) | ((! p0) & p3))))),"In 2 steps, both either both 'p0' is false and either both 'p0' and 'p3' or neither 'p0' nor 'p3' or 'p0' and either both 'p0' and 'p3' is false or both 'p0' is false and 'p3'",Precedence,0.03734102472662926,0.2864071726799011,0.14032170797387758,3 -F((p1 & p2) | (!p1 & !p2)) | X(p2 & p3),"Either eventually, either both 'p1' and 'p2' or neither 'p1' nor 'p2' or in the next step, both 'p2' and 'p3'",((F ((p1 & p2) | ((! p1) & (! p2)))) | ((X p2) & p3)),"Either eventually, either both 'p1' and 'p2' or neither 'p1' nor 'p2' or both in the next step, 'p2' and 'p3'",BadStateIndex,0.06327647715806961,0.5925284028053284,0.32958004623651505,5 -(((F p1) U (G p3)) & (G ((F p1) -> (! (G p3))))),"Both at some point, 'p1' will hold until 'p3' must always hold and at all times, if at some point, 'p1' will hold, then not 'p3' must always hold",(((F p1) U (G p3)) & ((F p1) -> (! (G p3)))),"Both at some point, 'p1' will hold until 'p3' must always hold and if at some point, 'p1' will hold, then not 'p3' must always hold",ImplicitG,0.06466665118932724,0.4403659999370575,0.29131780937314034,6 -((p0 -> p3) U ((F p2) & (F p3))),"If 'p0' holds, then 'p3' holds until both at some point, 'p2' will hold and at some point, 'p3' will hold",((p0 -> p3) U ((F p2) & p3)),"If 'p0' holds, then 'p3' holds until both at some point, 'p2' will hold and 'p3'",ImplicitF,0.09620845317840576,0.37508946657180786,0.23864905908703804,4 -(((G p2) U ((! p2) | p1)) & (G ((G p2) -> (! ((! p2) | p1))))),"Both 'p2' must always hold until either 'p2' is false or 'p1' and if 'p2' must always hold, then not either 'p2' is false or 'p1' is always true",((((G p2) U ((! p2) | p1)) | (G (G p2))) & (G ((G p2) -> (! ((! p2) | p1))))),"Both either 'p2' must always hold until either 'p2' is false or 'p1' or at all times, 'p2' and if 'p2' must always hold, then not either 'p2' is false or 'p1' is always true",WeakU,0.10728871822357178,0.39227768778800964,0.2693173885345459,4 -G((!p1 & (!p3 | Fp0)) | (p1 & p3 & G!p0)),"Always have either both 'p1' is false and either 'p3' is false or at some point, 'p0' will hold or both 'p1' and 'p3' and 'p0' will never occur",(((! p1) & ((! p3) | (F p0))) | ((p1 & p3) & (G (! p0)))),"Either both 'p1' is false and either 'p3' is false or at some point, 'p0' will hold or both 'p1' and 'p3' and 'p0' will never occur",OtherImplicit,0.15162089467048645,0.2360028177499771,0.19255444705486296,5 -(((F p3) & p1) U ((! ((F p3) & p1)) | (p3 -> p1))),"Both at some point, 'p3' will hold and 'p1' hold until either not both at some point, 'p3' will hold and 'p1' or if 'p3', then 'p1' holds",(((F p3) & p1) U (p3 -> p1)),"Both at some point, 'p3' will hold and 'p1' hold until if 'p3', then 'p1' holds",ExclusiveU,0.16197362542152405,0.4915367066860199,0.326755166053772,2 -(((p0 & p1) | (!p0 & !p1)) & XXG!p0) | (((p0 & !p1) | (!p0 & p1)) & XXFp0),"Either both either both 'p0' and 'p1' or neither 'p0' nor 'p1' and in 2 steps, 'p0' will never occur or both either both 'p0' and 'p1' is false or both 'p0' is false and 'p1' and in 2 steps, at some point, 'p0' will hold",(((((p0 & p1) | ((! p0) & (! p1))) & (X (X (G (! p0))))) | ((p0 & (! p1)) | ((! p0) & p1))) & (X (X (F p0)))),"Both either both either both 'p0' and 'p1' or neither 'p0' nor 'p1' and in 2 steps, 'p0' will never occur or either both 'p0' and 'p1' is false or both 'p0' is false and 'p1' and in 2 steps, at some point, 'p0' will hold",Precedence,0.04049919173121452,0.2636733651161194,0.17311375650266805,6 -X(p3 | (p2 U p1)),"In the next step, either 'p3' or 'p2' until 'p1'",(X (p3 | (p1 U p2))),"In the next step, either 'p3' or 'p1' until 'p2'",BadStateQuantification,0.046349335461854935,0.5506623983383179,0.31848904956132174,4 -Fp0 U (p3 | X(p2 & p3)),"At some point, 'p0' will hold until either 'p3' or in the next step, both 'p2' and 'p3'",((F p0) U (p3 | ((X p2) & p3))),"At some point, 'p0' will hold until either 'p3' or both in the next step, 'p2' and 'p3'",BadStateIndex,0.06353627145290375,0.4033069312572479,0.24506637702385584,6 -(((p1 | p3) U (! p3)) & (G ((p1 | p3) -> (! (! p3))))),"Both at least one of 'p1' or 'p3' hold until 'p3' is false and at all times, if at least one of 'p1' or 'p3', then not 'p3' is false",(((p1 | p3) U (! p3)) & ((p1 | p3) -> (! (! p3)))),"Both at least one of 'p1' or 'p3' hold until 'p3' is false and if at least one of 'p1' or 'p3', then not 'p3' is false",ImplicitG,0.06696542352437973,0.38150396943092346,0.22889351099729538,5 -FG((p3 | G!p1 | Gp0) & (p3 | F(!p0 | p1))),"Eventually, always maintain both either 'p3' or 'p1' will never occur or 'p0' must always hold and either 'p3' or eventually, either 'p0' is false or 'p1'",(F (G (((p3 | (G (! p1))) | (G p0)) & (p3 | ((! p0) | p1))))),"Eventually, always maintain both either 'p3' or 'p1' will never occur or 'p0' must always hold and either 'p3' or either 'p0' is false or 'p1'",ImplicitF,0.10394419729709625,0.2454671561717987,0.1904296338558197,5 -((((X p3) | p1) U (! p1)) & (G (! (((X p3) | p1) & (! p1))))),"Both either in the next step, 'p3' or 'p1' hold until 'p1' is false and it is never the case that both either in the next step, 'p3' or 'p1' and 'p1' is false",(((((X p3) | p1) U (! p1)) | (G ((X p3) | p1))) & (G (! (((X p3) | p1) & (! p1))))),"Both either in the next step, 'p3' or 'p1' hold until 'p1' is false or always have either in the next step, 'p3' or 'p1' and it is never the case that both either in the next step, 'p3' or 'p1' and 'p1' is false",WeakU,0.11572763323783875,0.4223088324069977,0.2547943741083145,4 -((! p2) U ((! (! p2)) | (p0 & p2))),'p2' is false until either 'p2' or both 'p0' and 'p2',((! p2) U (p0 & p2)),'p2' is false until both 'p0' and 'p2',ExclusiveU,0.1634880155324936,0.2883411943912506,0.2259146049618721,2 -(p3 U Gp0) U X(p2 U Xp2),"'p3' until 'p0' must always hold, and this continues until in the next step, 'p2' until in the next step, 'p2'",((p3 U (G p0)) U (F (p2 U (X p2)))),"'p3' until 'p0' must always hold, and this continues until eventually, 'p2' until in the next step, 'p2'",OtherImplicit,0.1733333170413971,0.27758660912513733,0.21240630373358727,4 -(p3 U (p0 U p1)) U (p3 U p0),"'p3' until 'p0' until 'p1', and this continues until 'p3' until 'p0'",(((p3 U (p0 U p1)) U p3) U p0),"'p3' until 'p0' until 'p1' until 'p3', and this continues until 'p0'",Precedence,0.041355639696121216,0.31306329369544983,0.20924533531069756,4 -p2 | (p0 U p3),Either 'p2' or 'p0' until 'p3',(p2 | (p3 U p0)),Either 'p2' or 'p3' until 'p0',BadStateQuantification,0.04961862415075302,0.4655517041683197,0.3165608998388052,4 -((G p1) U (((G p0) -> p1) & (G ((G p0) -> p3)))),"'p1' must always hold until both if 'p0' must always hold, then 'p1' holds and at all times, if 'p0' must always hold, then 'p3' holds",((G p1) U ((p0 -> p1) & (G ((G p0) -> p3)))),"'p1' must always hold until both if 'p0' holds, then 'p1' holds and at all times, if 'p0' must always hold, then 'p3' holds",ImplicitG,0.07011505961418152,0.6801282167434692,0.25602786242961884,5 -(X (((X p3) | p2) & ((! p1) & p2))),"In the next step, both either in the next step, 'p3' or 'p2' and both 'p1' is false and 'p2'",((X ((X p3) | p2)) & ((! p1) & p2)),"Both in the next step, either in the next step, 'p3' or 'p2' and both 'p1' is false and 'p2'",BadStateIndex,0.08070292323827744,0.31975439190864563,0.20022865757346153,2 -((F p0) U (((X p2) & p0) & (F ((F p1) -> p3)))),"At some point, 'p0' will hold until both in the next step, 'p2' and 'p0' and eventually, if at some point, 'p1' will hold, then 'p3' holds",((F p0) U (((X p2) & p0) & ((F p1) -> p3))),"At some point, 'p0' will hold until both in the next step, 'p2' and 'p0' and if at some point, 'p1' will hold, then 'p3' holds",ImplicitF,0.10425001382827759,0.38347673416137695,0.23939508944749832,6 -((((X p2) | p1) U (! p3)) & (G (! (((X p2) | p1) & (! p3))))),"Both either in the next step, 'p2' or 'p1' hold until 'p3' is false and it is never the case that both either in the next step, 'p2' or 'p1' and 'p3' is false",(((((X p2) | p1) U (! p3)) | (G ((X p2) | p1))) & (G (! (((X p2) | p1) & (! p3))))),"Both either in the next step, 'p2' or 'p1' hold until 'p3' is false or always have either in the next step, 'p2' or 'p1' and it is never the case that both either in the next step, 'p2' or 'p1' and 'p3' is false",WeakU,0.11577607691287994,0.4322969913482666,0.24379653632640838,5 -(p2 U ((! p2) & ((! p1) | p2))),'p2' until both 'p2' is false and either 'p1' is false or 'p2',(p2 U ((! p1) | p2)),'p2' until either 'p1' is false or 'p2',ExclusiveU,0.16365621984004974,0.5095543265342712,0.2741558313369751,5 -(Fp0 & (p0 U p3)) U p1,"Both at some point, 'p0' will hold and 'p0' until 'p3' hold until 'p1'",((F p0) & (p0 U p3)),"Both at some point, 'p0' will hold and 'p0' until 'p3'",OtherImplicit,0.18703140318393707,0.36475157737731934,0.24695269763469696,5 -(Fp1 U p2) U (p3 U p1),"At some point, 'p1' will hold until 'p2', and this continues until 'p3' until 'p1'",((((F p1) U p2) U p3) U p1),"At some point, 'p1' will hold until 'p2' until 'p3', and this continues until 'p1'",Precedence,0.04229610413312912,0.5763116478919983,0.29718530774116514,5 -((p3 U p0) U (p1 U p2)) U p3,"'p3' until 'p0' until 'p1' until 'p2', and this continues until 'p3'",(p3 U ((p3 U p0) U (p1 U p2))),"'p3' until 'p3' until 'p0', and this continues until 'p1' until 'p2'",BadStateQuantification,0.049981262534856796,0.7916196584701538,0.3216691827401519,4 -((F p3) U (((! p3) & p2) & (G ((G p3) -> p2)))),"At some point, 'p3' will hold until both 'p3' is false and 'p2' and at all times, if 'p3' must always hold, then 'p2' holds",((F p3) U (((! p3) & p2) & ((G p3) -> p2))),"At some point, 'p3' will hold until both 'p3' is false and 'p2' and if 'p3' must always hold, then 'p2' holds",ImplicitG,0.07021810859441757,0.3413970470428467,0.22759981006383895,5 -(X (((! p3) | p0) & ((X p2) & p3))),"In the next step, both either 'p3' is false or 'p0' and both in the next step, 'p2' and 'p3'",((X ((! p3) | p0)) & ((X p2) & p3)),"Both in the next step, either 'p3' is false or 'p0' and both in the next step, 'p2' and 'p3'",BadStateIndex,0.08377265185117722,0.348086953163147,0.2159298025071621,2 -(((X p1) | p3) U ((F p0) & (F p1))),"Either in the next step, 'p1' or 'p3' hold until both at some point, 'p0' will hold and at some point, 'p1' will hold",(((X p1) | p3) U ((F p0) & p1)),"Either in the next step, 'p1' or 'p3' hold until both at some point, 'p0' will hold and 'p1'",ImplicitF,0.10776412487030029,0.22966280579566956,0.16871346533298492,2 -(((X p1) | p0) U (((X p1) | p0) -> (p1 | p3))),"Either in the next step, 'p1' or 'p0' hold until if either in the next step, 'p1' or 'p0', then at least one of 'p1' or 'p3'",((((X p1) | p0) U (((X p1) | p0) -> (p1 | p3))) | (G ((X p1) | p0))),"Either in the next step, 'p1' or 'p0' hold until if either in the next step, 'p1' or 'p0', then at least one of 'p1' or 'p3' or always have either in the next step, 'p1' or 'p0'",WeakU,0.11592033505439758,0.22778265178203583,0.1908400058746338,4 -((p2 -> p3) U ((p2 -> p3) -> (p2 -> p3))),"If 'p2' holds, then 'p3' holds until if 'p2' holds, then 'p3' holds, then if 'p2' holds, then 'p3' holds",((p2 -> p3) U (p2 -> p3)),"If 'p2' holds, then 'p3' holds until if 'p2' holds, then 'p3' holds",ExclusiveU,0.16937156021595,0.3729923367500305,0.27118194848299026,2 -GFp1 U p1,'p1' will happen infinitely often until 'p1',(G (F p1)),'p1' will happen infinitely often,OtherImplicit,0.19305652379989624,0.6683191061019897,0.49543946981430054,3 -(Gp2 U p1) U (p0 U Xp0),"'p2' must always hold until 'p1', and this continues until 'p0' until in the next step, 'p0'",((((G p2) U p1) U p0) U (X p0)),"'p2' must always hold until 'p1' until 'p0', and this continues until in the next step, 'p0'",Precedence,0.04280916601419449,0.3918285071849823,0.22731567472219466,5 -(((G p2) -> p3) U ((! ((G p2) -> p3)) | (p3 & p1))),"If 'p2' must always hold, then 'p3' holds until either 'p2' must always hold, but not 'p3' or both 'p3' and 'p1'",(((G p2) -> p3) U (G ((! ((G p2) -> p3)) | (p3 & p1)))),"If 'p2' must always hold, then 'p3' holds until always have either 'p2' must always hold, but not 'p3' or both 'p3' and 'p1'",BadStateQuantification,0.058982182294130325,0.3857884705066681,0.19858889964719614,6 -((((! p0) | p2) U (G p1)) & (G (((! p0) | p2) -> (! (G p1))))),"Both either 'p0' is false or 'p2' hold until 'p1' must always hold and at all times, if either 'p0' is false or 'p2', then not 'p1' must always hold",((((! p0) | p2) U (G p1)) & (((! p0) | p2) -> (! (G p1)))),"Both either 'p0' is false or 'p2' hold until 'p1' must always hold and if either 'p0' is false or 'p2', then not 'p1' must always hold",ImplicitG,0.0703347846865654,0.34491488337516785,0.2206909939646721,5 -(p3 U p2) U X(p0 & p2),"'p3' until 'p2', and this continues until in the next step, both 'p0' and 'p2'",((p3 U p2) U ((X p0) & p2)),"'p3' until 'p2', and this continues until both in the next step, 'p0' and 'p2'",BadStateIndex,0.08811672776937485,0.4199155271053314,0.24801081977784634,4 -(((F p1) & p0) U ((p3 -> p2) & (F ((G p1) -> p0)))),"Both at some point, 'p1' will hold and 'p0' hold until both if 'p3', then 'p2' holds and eventually, if 'p1' must always hold, then 'p0' holds",(((F p1) & p0) U ((p3 -> p2) & ((G p1) -> p0))),"Both at some point, 'p1' will hold and 'p0' hold until both if 'p3', then 'p2' holds and if 'p1' must always hold, then 'p0' holds",ImplicitF,0.10813377052545547,0.28540918231010437,0.17905174816648164,6 -((p3 | p1) U (((F p0) & p3) & (G ((! p1) -> p0)))),"At least one of 'p3' or 'p1' hold until both at some point, 'p0' will hold and 'p3' and it is always the case that 'p0' unless 'p1'",(((p3 | p1) U (((F p0) & p3) & (G ((! p1) -> p0)))) | (G (p3 | p1))),"Either at least one of 'p3' or 'p1' hold until both at some point, 'p0' will hold and 'p3' and it is always the case that 'p0' unless 'p1' or always have either 'p3' or 'p1'",WeakU,0.11668875068426132,0.42371803522109985,0.20582491053002222,7 -(((G p1) & p3) U (((G p1) & p3) -> ((G p3) -> p1))),"Both 'p1' must always hold and 'p3' hold until if both 'p1' must always hold and 'p3', then if 'p3' must always hold, then 'p1'",(((G p1) & p3) U ((G p3) -> p1)),"Both 'p1' must always hold and 'p3' hold until if 'p3' must always hold, then 'p1'",ExclusiveU,0.1726030558347702,0.1726030558347702,0.1726030558347702,1 -F(p0 & p1) U p1,"Eventually, both 'p0' and 'p1' will be true simultaneously until 'p1'",(F (p0 & p1)),"Eventually, both 'p0' and 'p1' will be true simultaneously",OtherImplicit,0.19820520281791687,0.6248161196708679,0.4115106612443924,2 -XX((p2 & X!p2) | (!p2 & Xp2)),"In 2 steps, either both 'p2' and in the next step, 'p2' is false or both 'p2' is false and in the next step, 'p2'",(X (X (((p2 & (X (! p2))) | (! p2)) & (X p2)))),"In 2 steps, both either both 'p2' and in the next step, 'p2' is false or 'p2' is false and in the next step, 'p2'",Precedence,0.042971137911081314,0.2920770049095154,0.16071786110599837,3 -p1 | (p3 U p2),Either 'p1' or 'p3' until 'p2',(p1 | (p2 U p3)),Either 'p1' or 'p2' until 'p3',BadStateQuantification,0.06289363652467728,0.7450254559516907,0.42813421972095966,4 -(((G p2) -> p1) U (((F p3) -> p1) & (G (p2 -> p3)))),"If 'p2' must always hold, then 'p1' holds until both if at some point, 'p3' will hold, then 'p1' holds and at all times, if 'p2' holds, then 'p3' holds",(((G p2) -> p1) U (((F p3) -> p1) & (p2 -> p3))),"If 'p2' must always hold, then 'p1' holds until both if at some point, 'p3' will hold, then 'p1' holds and if 'p2' holds, then 'p3' holds",ImplicitG,0.07125857472419739,0.28554272651672363,0.16359106451272964,7 -XX(Gp0 | F!p3),"In 2 steps, either 'p0' must always hold or eventually, not 'p3'",(X (X (X ((G p0) | (F (! p3)))))),"In 3 steps, either 'p0' must always hold or eventually, not 'p3'",BadStateIndex,0.09606853872537613,0.3544589877128601,0.2574476197361946,5 -(((F p0) U ((F p3) -> p1)) & (G (! ((F p0) & ((F p3) -> p1))))),"Both at some point, 'p0' will hold until if at some point, 'p3' will hold, then 'p1' and it is never the case that both at some point, 'p0' will hold and if at some point, 'p3' will hold, then 'p1'",(((F p0) U ((F p3) -> p1)) & (G (! ((F p0) & (p3 -> p1))))),"Both at some point, 'p0' will hold until if at some point, 'p3' will hold, then 'p1' and it is never the case that both at some point, 'p0' will hold and if 'p3', then 'p1'",ImplicitF,0.11162640154361725,0.31764358282089233,0.2133680209517479,6 -(((p1 | p2) U ((G p3) | p1)) & (G (! ((p1 | p2) & ((G p3) | p1))))),Both at least one of 'p1' or 'p2' hold until either 'p3' must always hold or 'p1' and it is never the case that both at least one of 'p1' or 'p2' and either 'p3' must always hold or 'p1',((((p1 | p2) U ((G p3) | p1)) | (G (p1 | p2))) & (G (! ((p1 | p2) & ((G p3) | p1))))),Both either at least one of 'p1' or 'p2' hold until either 'p3' must always hold or 'p1' or always have either 'p1' or 'p2' and it is never the case that both at least one of 'p1' or 'p2' and either 'p3' must always hold or 'p1',WeakU,0.12026950716972351,0.3468334674835205,0.19986751079559326,5 -((p1 -> p0) U ((! (p1 -> p0)) & ((! p0) | p1))),"If 'p1' holds, then 'p0' holds until both 'p1', but not 'p0' and either 'p0' is false or 'p1'",((p1 -> p0) U ((! p0) | p1)),"If 'p1' holds, then 'p0' holds until either 'p0' is false or 'p1'",ExclusiveU,0.1887683868408203,0.542787492275238,0.2860000729560852,5 -X((p1 & G!p0) | (!p1 & Fp0)),"In the next step, either both 'p1' and 'p0' will never occur or both 'p1' is false and at some point, 'p0' will hold",(X (((p1 & (G (! p0))) | (! p1)) & (F p0))),"In the next step, both either both 'p1' and 'p0' will never occur or 'p1' is false and at some point, 'p0' will hold",Precedence,0.04458479955792427,0.44826582074165344,0.2596312053501606,5 -XX(p0 U p1),"In 2 steps, 'p0' until 'p1'",(X (X (p1 U p0))),"In 2 steps, 'p1' until 'p0'",BadStateQuantification,0.07203678041696548,0.4469376802444458,0.2801337894052267,4 -(((! p3) & p2) U (p1 & (G ((! p2) | p3)))),Both 'p3' is false and 'p2' hold until both 'p1' and always have either 'p2' is false or 'p3',(((! p3) & p2) U (p1 & ((! p2) | p3))),Both 'p3' is false and 'p2' hold until both 'p1' and either 'p2' is false or 'p3',ImplicitG,0.07618267834186554,0.38971635699272156,0.19905509303013483,6 -Fp1 U XXp3,"At some point, 'p1' will hold until in 2 steps, 'p3'",((F p1) U (X (X (X p3)))),"At some point, 'p1' will hold until in 3 steps, 'p3'",BadStateIndex,0.09645338356494904,0.4187382757663727,0.3098797984421253,4 -(((X p1) -> p2) U (((G p0) -> p2) & (F ((G p2) | p1)))),"If in the next step, 'p1', then 'p2' holds until both if 'p0' must always hold, then 'p2' holds and eventually, either 'p2' must always hold or 'p1'",(((X p1) -> p2) U (((G p0) -> p2) & ((G p2) | p1))),"If in the next step, 'p1', then 'p2' holds until both if 'p0' must always hold, then 'p2' holds and either 'p2' must always hold or 'p1'",ImplicitF,0.11210452020168304,0.3786934018135071,0.1797017753124237,7 -Gp1 U (((p0 & Xp1) | (!p0 & X!p1)) U p3),"'p1' must always hold until either both 'p0' and in the next step, 'p1' or both 'p0' is false and in the next step, 'p1' is false hold until 'p3'",(((G p1) U (((p0 & (X p1)) | ((! p0) & (X (! p1)))) U p3)) | (G (G p1))),"Either 'p1' must always hold until either both 'p0' and in the next step, 'p1' or both 'p0' is false and in the next step, 'p1' is false hold until 'p3' or at all times, 'p1'",WeakU,0.123885877430439,0.38047879934310913,0.2639784500002861,5 -(p2 U Xp1) U (p2 U p1),"'p2' until in the next step, 'p1', and this continues until 'p2' until 'p1'",(((p2 U (X p1)) U p2) U p1),"'p2' until in the next step, 'p1' until 'p2', and this continues until 'p1'",Precedence,0.04481009766459465,0.4488793909549713,0.23276558394233385,3 -((p0 & p3) U ((! (p0 & p3)) | (p2 -> p3))),"Both 'p0' and 'p3' hold until either not both 'p0' and 'p3' or if 'p2', then 'p3' holds",((p0 & p3) U (p2 -> p3)),"Both 'p0' and 'p3' hold until if 'p2', then 'p3' holds",ExclusiveU,0.1904260814189911,0.6873605847358704,0.3713172674179077,3 +!p1 | X(p0 | X(p1 U p0)),"Either 'p1' is false or in the next step, either 'p0' or in the next step, 'p1' until 'p0'",((! p1) | (X (p0 | (X (p0 U p1))))),"Either 'p1' is false or in the next step, either 'p0' or in the next step, 'p0' until 'p1'",BadStateQuantification,0.02090841345489025,0.25413063168525696,0.16864335474868616,3 +X((p0 & GFp1) | (!p0 & FG!p1)),"In the next step, either both 'p0' and 'p1' will happen infinitely often or both 'p0' is false and eventually, 'p1' will never occur again",(X (((p0 & (G (F p1))) | (! p0)) & (F (G (! p1))))),"In the next step, both either both 'p0' and 'p1' will happen infinitely often or 'p0' is false and eventually, 'p1' will never occur again",Precedence,0.045182909816503525,0.5305582880973816,0.30174335166811944,5 +X(G!p1 | X(!p0 & G!p1)),"In the next step, either 'p1' will never occur or in the next step, both 'p0' is false and 'p1' will never occur",(X ((G (! p1)) | ((X (! p0)) & (G (! p1))))),"In the next step, either 'p1' will never occur or both in the next step, 'p0' is false and 'p1' will never occur",BadStateIndex,0.059158120304346085,0.34612396359443665,0.22324363235384226,4 +p1 U G((p0 & Fp1) | (!p0 & G!p1)),"'p1' until always have either both 'p0' and at some point, 'p1' will hold or both 'p0' is false and 'p1' will never occur",(p1 U ((p0 & (F p1)) | ((! p0) & (G (! p1))))),"'p1' until either both 'p0' and at some point, 'p1' will hold or both 'p0' is false and 'p1' will never occur",ImplicitG,0.1079774796962738,0.844491720199585,0.2757271081209183,6 +((Fp1 U p0) U p1) U p0,"At some point, 'p1' will hold until 'p0' until 'p1', and this continues until 'p0'",(((F p1) U p0) U p1),"At some point, 'p1' will hold until 'p0', and this continues until 'p1'",OtherImplicit,0.115268774330616,0.4414633512496948,0.26019457913935184,4 +Gp1 U ((p0 & p1) | (!p0 & !p1)),'p1' must always hold until either both 'p0' and 'p1' or neither 'p0' nor 'p1',(((G p1) U ((p0 & p1) | ((! p0) & (! p1)))) | (G (G p1))),"Either 'p1' must always hold until either both 'p0' and 'p1' or neither 'p0' nor 'p1' or at all times, 'p1'",WeakU,0.12020408362150192,0.5117376446723938,0.4031363185495138,4 +(Fp0 & GFp1) | (G!p0 & FG!p1),"Either both at some point, 'p0' will hold and 'p1' will happen infinitely often or both 'p0' will never occur and eventually, 'p1' will never occur again",(((F p0) & (G (F p1))) | ((G (! p0)) & (G (! p1)))),"Either both at some point, 'p0' will hold and 'p1' will happen infinitely often or both 'p0' will never occur and 'p1' will never occur",ImplicitF,0.12770883738994598,0.29934269189834595,0.2128097414970398,5 +XX((p0 U p1) | (p1 U p0)),"In 2 steps, either 'p0' until 'p1' or 'p1' until 'p0'",(X (X ((p0 U p1) | (p0 U p1)))),"In 2 steps, either 'p0' until 'p1' or 'p0' until 'p1'",BadStateQuantification,0.027434570714831352,0.36185869574546814,0.22340362844988704,4 +((((!p0 & !p1) | (p0 & p1)) & Xp0) | (((p0 & !p1) | (!p0 & p1)) & X!p0)) U p1,"Either both either neither 'p0' nor 'p1' or both 'p0' and 'p1' and in the next step, 'p0' or both either both 'p0' and 'p1' is false or both 'p0' is false and 'p1' and in the next step, 'p0' is false hold until 'p1'",(((((((! p0) & (! p1)) | (p0 & p1)) & (X p0)) | ((p0 & (! p1)) | ((! p0) & p1))) & (X (! p0))) U p1),"Both either both either neither 'p0' nor 'p1' or both 'p0' and 'p1' and in the next step, 'p0' or either both 'p0' and 'p1' is false or both 'p0' is false and 'p1' and in the next step, 'p0' is false hold until 'p1'",Precedence,0.04599108546972275,0.322109192609787,0.20826068706810474,4 +p0 & X(p0 & (!p0 | !p1)),"Both 'p0' and in the next step, both 'p0' and not both 'p0' and 'p1'",(p0 & ((X p0) & ((! p0) | (! p1)))),"Both 'p0' and both in the next step, 'p0' and not both 'p0' and 'p1'",BadStateIndex,0.09727948158979416,0.5866594314575195,0.379283107817173,3 +p1 & G(Fp0 U X!p1),"Both 'p1' and at all times, at some point, 'p0' will hold until in the next step, 'p1' is false",(p1 & ((F p0) U (X (! p1)))),"Both 'p1' and at some point, 'p0' will hold until in the next step, 'p1' is false",ImplicitG,0.12393192201852798,0.38923153281211853,0.2591519221663475,5 +Xp0 | (Gp1 U p0),"Either in the next step, 'p0' or 'p1' must always hold until 'p0'",((X p0) | (((G p1) U p0) | (G (G p1)))),"Either in the next step, 'p0' or either 'p1' must always hold until 'p0' or at all times, 'p1'",WeakU,0.13785259425640106,0.5273995399475098,0.32292982563376427,4 +F((p0 & XG!p1) | (!p0 & XFp1)),"Eventually, either both 'p0' and in the next step, 'p1' will never occur or both 'p0' is false and in the next step, at some point, 'p1' will hold",(F ((p0 & (X (G (! p1)))) | ((! p0) & (X p1)))),"Eventually, either both 'p0' and in the next step, 'p1' will never occur or both 'p0' is false and in the next step, 'p1'",ImplicitF,0.14683674275875092,0.3655470907688141,0.2277156174182892,5 +p1 | ((p0 U p1) U Gp1),"Either 'p1' or 'p0' until 'p1', and this continues until 'p1' must always hold",((p0 U p1) U (G p1)),"'p0' until 'p1', and this continues until 'p1' must always hold",OtherImplicit,0.16943766176700592,0.38276705145835876,0.2709676414728165,5 +Gp0 & (p0 U p1),Both 'p0' must always hold and 'p0' until 'p1',((G p0) & (p1 U p0)),Both 'p0' must always hold and 'p1' until 'p0',BadStateQuantification,0.03841831535100937,0.5032243728637695,0.26060532331466674,5 +XX((p1 & X!p1) | (!p1 & Xp1)),"In 2 steps, either both 'p1' and in the next step, 'p1' is false or both 'p1' is false and in the next step, 'p1'",(X (X (((p1 & (X (! p1))) | (! p1)) & (X p1)))),"In 2 steps, both either both 'p1' and in the next step, 'p1' is false or 'p1' is false and in the next step, 'p1'",Precedence,0.04637196660041809,0.312267005443573,0.17948032915592194,3 +Gp0 | XXp1,"Either 'p0' must always hold or in 2 steps, 'p1'",((G p0) | (X (X (X p1)))),"Either 'p0' must always hold or in 3 steps, 'p1'",BadStateIndex,0.12116672098636627,0.4119628369808197,0.3144327290356159,4 +G(FGp1 U p1),"Eventually, 'p1' will always be true until 'p1' is always true",((F (G p1)) U p1),"Eventually, 'p1' will always be true until 'p1'",ImplicitG,0.12456154823303223,0.48139849305152893,0.22403253987431526,4 +F(p1 | (p0 U Gp1)),"Eventually, either 'p1' or 'p0' until 'p1' must always hold",(F (p1 | ((p0 U (G p1)) | (G p0)))),"Eventually, either 'p1' or either 'p0' until 'p1' must always hold or 'p0' must always hold",WeakU,0.15552829205989838,0.28641483187675476,0.2560430258512497,5 +(Fp1 & Fp0) | G(!p0 & !p1),"Either both at some point, 'p1' will hold and at some point, 'p0' will hold or always maintain both 'p0' is false and 'p1' is false",(((F p1) & p0) | (G ((! p0) & (! p1)))),"Either both at some point, 'p1' will hold and 'p0' or always maintain both 'p0' is false and 'p1' is false",ImplicitF,0.17261190712451935,0.5596886277198792,0.3430473022162914,4 +G(p1 | (p0 U Gp1)),Always have either 'p1' or 'p0' until 'p1' must always hold,(p1 | (p0 U (G p1))),Either 'p1' or 'p0' until 'p1' must always hold,OtherImplicit,0.17848385870456696,0.3540279269218445,0.2671307325363159,5 +p1 & X(p0 U p1),"Both 'p1' and in the next step, 'p0' until 'p1'",(p1 & (X (p1 U p0))),"Both 'p1' and in the next step, 'p1' until 'p0'",BadStateQuantification,0.040850527584552765,0.45363736152648926,0.3011660898725192,3 +(p0 U Xp1) U (p0 U p1),"'p0' until in the next step, 'p1', and this continues until 'p0' until 'p1'",(((p0 U (X p1)) U p0) U p1),"'p0' until in the next step, 'p1' until 'p0', and this continues until 'p1'",Precedence,0.04673055186867714,0.4582228362560272,0.20609123135606447,3 +Fp0 U X(p1 & Xp1),"At some point, 'p0' will hold until in the next step, both 'p1' and in the next step, 'p1'",((F p0) U ((X p1) & (X p1))),"At some point, 'p0' will hold until in the next step, both 'p1' and 'p1'",BadStateIndex,0.12152942270040512,0.39818066358566284,0.2809077754616737,5 +(Xp0 U Gp0) U Gp1,"In the next step, 'p0' until 'p0' must always hold, and this continues until 'p1' must always hold",(((X p0) U (G p0)) U p1),"In the next step, 'p0' until 'p0' must always hold, and this continues until 'p1'",ImplicitG,0.13521887362003326,0.41934463381767273,0.26437321305274963,3 +(p0 | Xp0) U (p1 U Xp1),"Either 'p0' or in the next step, 'p0' hold until 'p1' until in the next step, 'p1'",(((p0 | (X p0)) U (p1 U (X p1))) | (G (p0 | (X p0)))),"Either 'p0' or in the next step, 'p0' hold until 'p1' until in the next step, 'p1' or always have either 'p0' or in the next step, 'p0'",WeakU,0.17003490030765533,0.5788944363594055,0.33460013195872307,4 +XF(p1 | X!p0),"In the next step, eventually, either 'p1' or in the next step, 'p0' is false",(X (p1 | (X (! p0)))),"In the next step, either 'p1' or in the next step, 'p0' is false",ImplicitF,0.17506812512874603,0.2623584568500519,0.2232353240251541,3 +(p1 U Gp0) U X(p1 U Xp1),"'p1' until 'p0' must always hold, and this continues until in the next step, 'p1' until in the next step, 'p1'",((p1 U (G p0)) U (F (p1 U (X p1)))),"'p1' until 'p0' must always hold, and this continues until eventually, 'p1' until in the next step, 'p1'",OtherImplicit,0.18497410416603088,0.2863331139087677,0.22774365171790123,4 +p1 | (p1 U p0),Either 'p1' or 'p1' until 'p0',(p1 | (p0 U p1)),Either 'p1' or 'p0' until 'p1',BadStateQuantification,0.04335223510861397,0.6946157217025757,0.4112886053820451,3 +X((p1 & GFp0) | (!p1 & FG!p0)),"In the next step, either both 'p1' and 'p0' will happen infinitely often or both 'p1' is false and eventually, 'p0' will never occur again",(X (((p1 & (G (F p0))) | (! p1)) & (F (G (! p0))))),"In the next step, both either both 'p1' and 'p0' will happen infinitely often or 'p1' is false and eventually, 'p0' will never occur again",Precedence,0.046836189925670624,0.5405901670455933,0.3066252514719963,5 +(Fp0 & XXp1) | (G!p0 & XX!p1),"Either both at some point, 'p0' will hold and in 2 steps, 'p1' or both 'p0' will never occur and in 2 steps, 'p1' is false",(((F p0) & (X (X (X (X p1))))) | ((G (! p0)) & (X (X (X (X (! p1))))))),"Either both at some point, 'p0' will hold and in 4 steps, 'p1' or both 'p0' will never occur and in 4 steps, 'p1' is false",BadStateIndex,0.12312055379152298,0.2814328074455261,0.21634528413414955,6 +X(p1 U G(!p1 U p0)),"In the next step, 'p1' until 'p1' is false until 'p0' is always true",(X (p1 U ((! p1) U p0))),"In the next step, 'p1' until 'p1' is false until 'p0'",ImplicitG,0.13618993759155273,0.47957679629325867,0.28618506093819934,3 +F(p1 | ((Fp1 U p0) U Gp1)),"Eventually, either 'p1' or at some point, 'p1' will hold until 'p0', and this continues until 'p1' must always hold",(p1 | (((F p1) U p0) U (G p1))),"Either 'p1' or at some point, 'p1' will hold until 'p0', and this continues until 'p1' must always hold",ImplicitF,0.17938795685768127,0.27393218874931335,0.21014483273029327,5 +G(!p0 | G(!p0 | G!p1)),Always have either 'p0' is false or always have either 'p0' is false or 'p1' will never occur,((! p0) | (G ((! p0) | (G (! p1))))),Either 'p0' is false or always have either 'p0' is false or 'p1' will never occur,OtherImplicit,0.18578794598579407,0.27207452058792114,0.2289312332868576,2 +p0 | (p1 U Gp0),Either 'p0' or 'p1' until 'p0' must always hold,(p0 | ((p1 U (G p0)) | (G p1))),Either 'p0' or either 'p1' until 'p0' must always hold or 'p1' must always hold,WeakU,0.19263558089733124,0.4078819453716278,0.3085450269281864,4 +p0 & X(p0 U p1),"Both 'p0' and in the next step, 'p0' until 'p1'",(p0 & (X (p1 U p0))),"Both 'p0' and in the next step, 'p1' until 'p0'",BadStateQuantification,0.04538380727171898,0.4391469657421112,0.2959597098330657,3 +X(p0 U ((p0 & Gp1) | (!p0 & F!p1))),"In the next step, 'p0' until either both 'p0' and 'p1' must always hold or both 'p0' is false and eventually, not 'p1'",(X ((p0 U (p0 & (G p1))) | ((! p0) & (F (! p1))))),"In the next step, either 'p0' until both 'p0' and 'p1' must always hold or both 'p0' is false and eventually, not 'p1'",Precedence,0.04822469875216484,0.4035189151763916,0.2145196342219909,6 +!p1 | XXp0,"Either 'p1' is false or in 2 steps, 'p0'",((! p1) | (X (X (X p0)))),"Either 'p1' is false or in 3 steps, 'p0'",BadStateIndex,0.12743887305259705,0.3204624354839325,0.22395065426826477,2 +XF!p0 | (Fp1 & F!p0) | G(p0 & !p1),"Either in the next step, eventually, not 'p0' or both at some point, 'p1' will hold and eventually, not 'p0' or always maintain both 'p0' and 'p1' is false",(((X (F (! p0))) | ((F p1) & (F (! p0)))) | (p0 & (! p1))),"Either in the next step, eventually, not 'p0' or both at some point, 'p1' will hold and eventually, not 'p0' or both 'p0' and 'p1' is false",ImplicitG,0.1418096125125885,0.3046281039714813,0.24160577356815338,4 +XXXF(p1 | Xp1),"In 3 steps, eventually, either 'p1' or in the next step, 'p1'",(X (X (X (p1 | (X p1))))),"In 3 steps, either 'p1' or in the next step, 'p1'",ImplicitF,0.18874132633209229,0.2871764004230499,0.2559613659977913,4 +p0 & ((p1 U p0) U Gp1),"Both 'p0' and 'p1' until 'p0', and this continues until 'p1' must always hold",((p1 U p0) U (G p1)),"'p1' until 'p0', and this continues until 'p1' must always hold",OtherImplicit,0.1899251937866211,0.31264349818229675,0.2603229105472565,5 +Gp1 U (p0 | Xp0),"'p1' must always hold until either 'p0' or in the next step, 'p0'",(((G p1) U (p0 | (X p0))) | (G (G p1))),"Either 'p1' must always hold until either 'p0' or in the next step, 'p0' or at all times, 'p1'",WeakU,0.19389545917510986,0.4915340542793274,0.35983437299728394,3 +(p1 & F(p1 & X!p1)) | (!p1 & G(!p1 | Xp1)),"Either both 'p1' and eventually, both 'p1' and in the next step, 'p1' is false will be true simultaneously or both 'p1' is false and always have either 'p1' is false or in the next step, 'p1'",(((p1 & (F (p1 & (X (! p1))))) | (! p1)) & (G ((! p1) | (X p1)))),"Both either both 'p1' and eventually, both 'p1' and in the next step, 'p1' is false will be true simultaneously or 'p1' is false and always have either 'p1' is false or in the next step, 'p1'",Precedence,0.048868048936128616,0.33146679401397705,0.18673827424645423,5 +(p0 U p1) | (!p0 U p1),Either 'p0' until 'p1' or 'p0' is false until 'p1',((p1 U p0) | ((! p0) U p1)),Either 'p1' until 'p0' or 'p0' is false until 'p1',BadStateQuantification,0.05337568745017052,0.4504449963569641,0.2755219517275691,4 +X(Fp0 & Fp1),"In the next step, both at some point, 'p0' will hold and at some point, 'p1' will hold",((X (F p0)) & (F p1)),"Both in the next step, at some point, 'p0' will hold and at some point, 'p1' will hold",BadStateIndex,0.13900725543498993,0.5019745826721191,0.2730279341340065,4 +Fp0 U G(p1 | Xp1),"At some point, 'p0' will hold until always have either 'p1' or in the next step, 'p1'",((F p0) U (p1 | (X p1))),"At some point, 'p0' will hold until either 'p1' or in the next step, 'p1'",ImplicitG,0.14705687761306763,0.38945603370666504,0.3048351779580116,4 +XF(p0 | G!p1),"In the next step, eventually, either 'p0' or 'p1' will never occur",(X (p0 | (G (! p1)))),"In the next step, either 'p0' or 'p1' will never occur",ImplicitF,0.18988725543022156,0.4686608612537384,0.33729253709316254,4 +FG(Fp0 U p1),"Eventually, at some point, 'p0' will hold until 'p1' will always be true",(G ((F p0) U p1)),"At some point, 'p0' will hold until 'p1' is always true",OtherImplicit,0.1922300159931183,0.46150508522987366,0.3206024348735809,5 +(p1 | Xp1) U XGp1,"Either 'p1' or in the next step, 'p1' hold until in the next step, 'p1' must always hold",(((p1 | (X p1)) U (X (G p1))) | (G (p1 | (X p1)))),"Either 'p1' or in the next step, 'p1' hold until in the next step, 'p1' must always hold or always have either 'p1' or in the next step, 'p1'",WeakU,0.19762663543224335,0.34478357434272766,0.2679729796946049,4 +(p1 U Xp1) U (p0 U Xp0),"'p1' until in the next step, 'p1', and this continues until 'p0' until in the next step, 'p0'",(((p1 U (X p1)) U p0) U (X p0)),"'p1' until in the next step, 'p1' until 'p0', and this continues until in the next step, 'p0'",Precedence,0.048961423337459564,0.5553374290466309,0.32314873300492764,4 +((p1 U Xp0) U p0) U p1,"'p1' until in the next step, 'p0' until 'p0', and this continues until 'p1'",(p1 U ((p1 U (X p0)) U p0)),"'p1' until 'p1' until in the next step, 'p0', and this continues until 'p0'",BadStateQuantification,0.0630161464214325,0.4495844542980194,0.2675465444723765,3 +X((!p0 | p1) & Fp0),"In the next step, both either 'p0' is false or 'p1' and at some point, 'p0' will hold",((X ((! p0) | p1)) & (F p0)),"Both in the next step, either 'p0' is false or 'p1' and at some point, 'p0' will hold",BadStateIndex,0.14134325087070465,0.5133114457130432,0.2891026921570301,4 +(!p1 | X!p0) U Gp0,"Either 'p1' is false or in the next step, 'p0' is false hold until 'p0' must always hold",(((! p1) | (X (! p0))) U p0),"Either 'p1' is false or in the next step, 'p0' is false hold until 'p0'",ImplicitG,0.15286137163639069,0.3739868104457855,0.2799713462591171,3 +F((Fp0 & Xp1) | (X!p1 & G!p0)),"Eventually, either both at some point, 'p0' will hold and in the next step, 'p1' or both in the next step, 'p1' is false and 'p0' will never occur",(((F p0) & (X p1)) | ((X (! p1)) & (G (! p0)))),"Either both at some point, 'p0' will hold and in the next step, 'p1' or both in the next step, 'p1' is false and 'p0' will never occur",ImplicitF,0.19006946682929993,0.425050288438797,0.25383188426494596,5 +GFp1 U p1,'p1' will happen infinitely often until 'p1',(G (F p1)),'p1' will happen infinitely often,OtherImplicit,0.19305652379989624,0.6683191061019897,0.43526366353034973,4 +p1 | (p0 U Gp1),Either 'p1' or 'p0' until 'p1' must always hold,(p1 | ((p0 U (G p1)) | (G p0))),Either 'p1' or either 'p0' until 'p1' must always hold or 'p0' must always hold,WeakU,0.19808413088321686,0.39679455757141113,0.3015170067548752,5 +((!p0 | p1) & XXp0) | (p0 & !p1 & XX!p0),"Either both either 'p0' is false or 'p1' and in 2 steps, 'p0' or both 'p0' and 'p1' is false and in 2 steps, 'p0' is false",(((((! p0) | p1) & (X (X p0))) | (p0 & (! p1))) & (X (X (! p0)))),"Both either both either 'p0' is false or 'p1' and in 2 steps, 'p0' or both 'p0' and 'p1' is false and in 2 steps, 'p0' is false",Precedence,0.04942091181874275,0.31029564142227173,0.1746941270927588,3 +(p0 U p1) | XX!p0,"Either 'p0' until 'p1' or in 2 steps, 'p0' is false",((p1 U p0) | (X (X (! p0)))),"Either 'p1' until 'p0' or in 2 steps, 'p0' is false",BadStateQuantification,0.06357156485319138,0.27493199706077576,0.19406952895224094,4 +X(Fp1 U XXp0),"In the next step, at some point, 'p1' will hold until in 2 steps, 'p0'",(X ((F p1) U (X (X (X (X p0)))))),"In the next step, at some point, 'p1' will hold until in 4 steps, 'p0'",BadStateIndex,0.14459311962127686,0.4106765687465668,0.30060043931007385,4 +(p0 U Gp1) U Gp0,"'p0' until 'p1' must always hold, and this continues until 'p0' must always hold",((p0 U p1) U (G p0)),"'p0' until 'p1', and this continues until 'p0' must always hold",ImplicitG,0.1534748375415802,0.5967190861701965,0.32907889783382416,3 +p1 | XF(!p0 | p1),"Either 'p1' or in the next step, eventually, either 'p0' is false or 'p1'",(p1 | (X ((! p0) | p1))),"Either 'p1' or in the next step, either 'p0' is false or 'p1'",ImplicitF,0.1909075677394867,0.3919055163860321,0.2721031705538432,3 +(p1 U Xp0) U (p0 U Xp1),"'p1' until in the next step, 'p0', and this continues until 'p0' until in the next step, 'p1'",(((p1 U (X p0)) U p0) U (X p1)),"'p1' until in the next step, 'p0' until 'p0', and this continues until in the next step, 'p1'",Precedence,0.0513981431722641,0.552997887134552,0.2510302569717169,4 +(p1 | Xp1) U (p0 | Xp0),"Either 'p1' or in the next step, 'p1' hold until either 'p0' or in the next step, 'p0'",((p0 | (X p0)) U (p1 | (X p1))),"Either 'p0' or in the next step, 'p0' hold until either 'p1' or in the next step, 'p1'",BadStateQuantification,0.06600576639175415,0.606672465801239,0.2298018615692854,4 +XXXXF!p1,"In 4 steps, eventually, not 'p1'",(X (X (X (F (! p1))))),"In 3 steps, eventually, not 'p1'",BadStateIndex,0.14881731569766998,0.5548974871635437,0.34653211757540703,4 +XG(p1 | XGp1),"In the next step, always have either 'p1' or in the next step, 'p1' must always hold",(X (p1 | (X (G p1)))),"In the next step, either 'p1' or in the next step, 'p1' must always hold",ImplicitG,0.15448234975337982,0.5102343559265137,0.2897236148516337,3 +XF(p0 | Xp0),"In the next step, eventually, either 'p0' or in the next step, 'p0'",(X (p0 | (X p0))),"In the next step, either 'p0' or in the next step, 'p0'",ImplicitF,0.1949276626110077,0.27872219681739807,0.2486893037954966,3 +X(((p1 & Xp1) | (!p1 & X!p1)) U p0),"In the next step, either both 'p1' and in the next step, 'p1' or both 'p1' is false and in the next step, 'p1' is false until 'p0'",(X ((((p1 & (X p1)) | (! p1)) & (X (! p1))) U p0)),"In the next step, both either both 'p1' and in the next step, 'p1' or 'p1' is false and in the next step, 'p1' is false until 'p0'",Precedence,0.05285680294036865,0.3495334982872009,0.19633755460381508,4 +(p0 U p1) | XXp0,"Either 'p0' until 'p1' or in 2 steps, 'p0'",((p1 U p0) | (X (X p0))),"Either 'p1' until 'p0' or in 2 steps, 'p0'",BadStateQuantification,0.07112549245357513,0.2916434705257416,0.1955446849266688,3 +XX(p0 & !p1),"In 2 steps, both 'p0' and 'p1' is false",(X (X (X (X (p0 & (! p1)))))),"In 4 steps, both 'p0' and 'p1' is false",BadStateIndex,0.15534093976020813,0.4203168451786041,0.28782889246940613,2 +F!p0 U G(p1 | Xp1),"Eventually, not 'p0' until always have either 'p1' or in the next step, 'p1'",((F (! p0)) U (p1 | (X p1))),"Eventually, not 'p0' until either 'p1' or in the next step, 'p1'",ImplicitG,0.15620921552181244,0.48227840662002563,0.363957729190588,4 +FG(Fp1 U p0),"Eventually, at some point, 'p1' will hold until 'p0' will always be true",(G ((F p1) U p0)),"At some point, 'p1' will hold until 'p0' is always true",ImplicitF,0.1951882690191269,0.45801669359207153,0.3073694944381714,5 +(p0 & ((p0 & p1) | (!p0 & !p1))) | (!p0 & ((p0 & !p1) | (!p0 & p1))),Either both 'p0' and either both 'p0' and 'p1' or neither 'p0' nor 'p1' or both 'p0' is false and either both 'p0' and 'p1' is false or both 'p0' is false and 'p1',(((p0 & ((p0 & p1) | ((! p0) & (! p1)))) | (! p0)) & ((p0 & (! p1)) | ((! p0) & p1))),Both either both 'p0' and either both 'p0' and 'p1' or neither 'p0' nor 'p1' or 'p0' is false and either both 'p0' and 'p1' is false or both 'p0' is false and 'p1',Precedence,0.05554335564374924,0.3098038136959076,0.18267358466982841,2 +XX(p1 U p0),"In 2 steps, 'p1' until 'p0'",(X (X (p0 U p1))),"In 2 steps, 'p0' until 'p1'",BadStateQuantification,0.07203678041696548,0.4490218460559845,0.2798002567142248,4 +(p1 U Gp0) U Gp1,"'p1' until 'p0' must always hold, and this continues until 'p1' must always hold",((p1 U p0) U (G p1)),"'p1' until 'p0', and this continues until 'p1' must always hold",ImplicitG,0.15675555169582367,0.375934898853302,0.27093450352549553,4 +X(!p1 & Fp1),"In the next step, both 'p1' is false and at some point, 'p1' will hold",((X (! p1)) & (F p1)),"Both in the next step, 'p1' is false and at some point, 'p1' will hold",BadStateIndex,0.15703541040420532,0.5122520327568054,0.31117600947618484,4 +G((p1 U Xp0) U (p1 U p0)),"'p1' until in the next step, 'p0', and this continues until 'p1' until 'p0' is always true",(G (((p1 U (X p0)) U p1) U p0)),"'p1' until in the next step, 'p0' until 'p1', and this continues until 'p0' is always true",Precedence,0.05677766725420952,0.42033082246780396,0.27548400592058897,4 +XF(p1 | Xp1),"In the next step, eventually, either 'p1' or in the next step, 'p1'",(X (p1 | (X p1))),"In the next step, either 'p1' or in the next step, 'p1'",ImplicitF,0.19797521829605103,0.2917979061603546,0.2598084807395935,3 +X((p1 U Xp0) U p0),"In the next step, 'p1' until in the next step, 'p0' until 'p0'",(X (p0 U (p1 U (X p0)))),"In the next step, 'p0' until 'p1' until in the next step, 'p0'",BadStateQuantification,0.07310346513986588,0.31792864203453064,0.19551605358719826,2 +XGp0 U Gp1,"In the next step, 'p0' must always hold until 'p1' must always hold",((X p0) U (G p1)),"In the next step, 'p0' until 'p1' must always hold",ImplicitG,0.1579393595457077,0.6297464966773987,0.31908923760056496,4 +G!p0 | XXp0,"Either 'p0' will never occur or in 2 steps, 'p0'",((G (! p0)) | (X (X (X p0)))),"Either 'p0' will never occur or in 3 steps, 'p0'",BadStateIndex,0.15925383567810059,0.5202227830886841,0.35656195878982544,4 +XFp1 U ((p1 & XFp0) | (!p1 & XG!p0)),"In the next step, at some point, 'p1' will hold until either both 'p1' and in the next step, at some point, 'p0' will hold or both 'p1' is false and in the next step, 'p0' will never occur",(((X (F p1)) U (p1 & (X (F p0)))) | ((! p1) & (X (G (! p0))))),"Either in the next step, at some point, 'p1' will hold until both 'p1' and in the next step, at some point, 'p0' will hold or both 'p1' is false and in the next step, 'p0' will never occur",Precedence,0.05829669162631035,0.4984566569328308,0.18829810060560703,6 +(p0 U p1) | (p1 U Xp1),"Either 'p0' until 'p1' or 'p1' until in the next step, 'p1'",((p1 U p0) | (p1 U (X p1))),"Either 'p1' until 'p0' or 'p1' until in the next step, 'p1'",BadStateQuantification,0.07464408874511719,0.47939932346343994,0.29544374719262123,4 +X(Fp0 U !p1) U Gp0,"In the next step, at some point, 'p0' will hold until 'p1' is false until 'p0' must always hold",((X ((F p0) U (! p1))) U p0),"In the next step, at some point, 'p0' will hold until 'p1' is false until 'p0'",ImplicitG,0.16024534404277802,0.40748849511146545,0.27275933921337125,5 +X(p0 & !p1),"In the next step, both 'p0' and 'p1' is false",((X p0) & (! p1)),"Both in the next step, 'p0' and 'p1' is false",BadStateIndex,0.16037122905254364,0.6120498776435852,0.3862105533480644,2 +X((p0 & Xp1) | (!p0 & X!p1)),"In the next step, either both 'p0' and in the next step, 'p1' or both 'p0' is false and in the next step, 'p1' is false",(X (((p0 & (X p1)) | (! p0)) & (X (! p1)))),"In the next step, both either both 'p0' and in the next step, 'p1' or 'p0' is false and in the next step, 'p1' is false",Precedence,0.0598900131881237,0.2605189085006714,0.16020446084439754,2 +(p1 U p0) & Xp0,"Both 'p1' until 'p0' and in the next step, 'p0'",((p0 U p1) & (X p0)),"Both 'p0' until 'p1' and in the next step, 'p0'",BadStateQuantification,0.07519134134054184,0.5730811357498169,0.32413623854517937,2 +p0 U XX(Gp1 U p0),"'p0' until in 2 steps, 'p1' must always hold until 'p0'",(p0 U (X (X (X ((G p1) U p0))))),"'p0' until in 3 steps, 'p1' must always hold until 'p0'",BadStateIndex,0.16249607503414154,0.4183444678783417,0.3019712008535862,4 +p1 & XG(!p0 U p1),"Both 'p1' and in the next step, 'p0' is false until 'p1' is always true",(p1 & (X ((! p0) U p1))),"Both 'p1' and in the next step, 'p0' is false until 'p1'",ImplicitG,0.16366077959537506,0.4299864172935486,0.27890338003635406,4 +(p1 | X!p0) U ((!p0 & X!p0) | (p0 & Xp0)),"Either 'p1' or in the next step, 'p0' is false hold until either both 'p0' is false and in the next step, 'p0' is false or both 'p0' and in the next step, 'p0'",(((p1 | (X (! p0))) U ((! p0) & (X (! p0)))) | (p0 & (X p0))),"Either 'p1' or in the next step, 'p0' is false hold until both 'p0' is false and in the next step, 'p0' is false or both 'p0' and in the next step, 'p0'",Precedence,0.06011570990085602,0.52745121717453,0.23245379514992237,4 X(p1 U p0),"In the next step, 'p1' until 'p0'",(X (p0 U p1)),"In the next step, 'p0' until 'p1'",BadStateQuantification,0.08421752601861954,0.5432999134063721,0.344382606446743,3 -((p3 U (F p1)) & (G (p3 -> (! (F p1))))),"Both 'p3' until at some point, 'p1' will hold and at all times, if 'p3', then not at some point, 'p1' will hold",((p3 U (F p1)) & (p3 -> (! (F p1)))),"Both 'p3' until at some point, 'p1' will hold and if 'p3', then not at some point, 'p1' will hold",ImplicitG,0.08505173772573471,0.4061712324619293,0.289356429874897,5 -(X (((X p1) -> p2) & (p3 -> p0))),"In the next step, both if in the next step, 'p1', then 'p2' holds and if 'p3' holds, then 'p0' holds",((X ((X p1) -> p2)) & (p3 -> p0)),"Both in the next step, if in the next step, 'p1', then 'p2' holds and if 'p3' holds, then 'p0' holds",BadStateIndex,0.09651118516921997,0.3920551836490631,0.287649542093277,3 -((p1 | p0) U (((F p2) & p3) & (F p1))),"At least one of 'p1' or 'p0' hold until both at some point, 'p2' will hold and 'p3' and at some point, 'p1' will hold",((p1 | p0) U (((F p2) & p3) & p1)),"At least one of 'p1' or 'p0' hold until both at some point, 'p2' will hold and 'p3' and 'p1'",ImplicitF,0.11937731504440308,0.6894240379333496,0.27272829413414,6 -(Gp3 U Xp0) | Fp1,"Either 'p3' must always hold until in the next step, 'p0' or at some point, 'p1' will hold",((((G p3) U (X p0)) | (G (G p3))) | (F p1)),"Either 'p3' must always hold until in the next step, 'p0' or at all times, 'p3' or at some point, 'p1' will hold",WeakU,0.1245269775390625,0.5009090900421143,0.2504582405090332,5 -(((X p2) | p0) U ((! ((X p2) | p0)) | (p3 & p2))),"Either in the next step, 'p2' or 'p0' hold until either neither in the next step, 'p2' nor 'p0' or both 'p3' and 'p2'",((((X p2) | p0) U (! ((X p2) | p0))) | (p3 & p2)),"Either in the next step, 'p2' or 'p0' hold until neither in the next step, 'p2' nor 'p0' or both 'p3' and 'p2'",Precedence,0.04540524631738663,0.5387542247772217,0.2179892659187317,5 -((p0 U (F p1)) & (G (p0 -> (! (F p1))))),"Both 'p0' until at some point, 'p1' will hold and at all times, if 'p0', then not at some point, 'p1' will hold",((p0 U (F p1)) & (p0 -> (! (F p1)))),"Both 'p0' until at some point, 'p1' will hold and if 'p0', then not at some point, 'p1' will hold",ImplicitG,0.08571310341358185,0.3936465382575989,0.23511863748232523,6 -((((X p2) | p3) U ((F p2) | p3)) & (G (! (((X p2) | p3) & ((F p2) | p3))))),"Both either in the next step, 'p2' or 'p3' hold until either at some point, 'p2' will hold or 'p3' and it is never the case that both either in the next step, 'p2' or 'p3' and either at some point, 'p2' will hold or 'p3'",((((X p2) | p3) U ((F p2) | p3)) & (F (! (((X p2) | p3) & ((F p2) | p3))))),"Both either in the next step, 'p2' or 'p3' hold until either at some point, 'p2' will hold or 'p3' and eventually, it will not be the case that both either in the next step, 'p2' or 'p3' and either at some point, 'p2' will hold or 'p3'",BadStateQuantification,0.08660925924777985,0.4033510386943817,0.23819689825177193,4 -p0 & X(p1 & (!p0 | !p2)),"Both 'p0' and in the next step, both 'p1' and not both 'p0' and 'p2'",(p0 & ((X p1) & ((! p0) | (! p2)))),"Both 'p0' and both in the next step, 'p1' and not both 'p0' and 'p2'",BadStateIndex,0.09772362560033798,0.5759117007255554,0.37638361006975174,3 -(X (((F p1) -> p2) & (F p3))),"In the next step, both if at some point, 'p1' will hold, then 'p2' holds and at some point, 'p3' will hold",(X (((F p1) -> p2) & p3)),"In the next step, both if at some point, 'p1' will hold, then 'p2' holds and 'p3'",ImplicitF,0.12310720980167389,0.5043647885322571,0.27577129006385803,4 -(((p3 | p1) U (! p2)) & (G (! ((p3 | p1) & (! p2))))),Both at least one of 'p3' or 'p1' hold until 'p2' is false and it is never the case that both at least one of 'p3' or 'p1' and 'p2' is false,((((p3 | p1) U (! p2)) | (G (p3 | p1))) & (G (! ((p3 | p1) & (! p2))))),Both either at least one of 'p3' or 'p1' hold until 'p2' is false or always have either 'p3' or 'p1' and it is never the case that both at least one of 'p3' or 'p1' and 'p2' is false,WeakU,0.12589393556118011,0.32602033019065857,0.2151953637599945,5 -((!p0 | p3) & XXp0) | (p0 & !p3 & XX!p0),"Either both either 'p0' is false or 'p3' and in 2 steps, 'p0' or both 'p0' and 'p3' is false and in 2 steps, 'p0' is false",(((((! p0) | p3) & (X (X p0))) | (p0 & (! p3))) & (X (X (! p0)))),"Both either both either 'p0' is false or 'p3' and in 2 steps, 'p0' or both 'p0' and 'p3' is false and in 2 steps, 'p0' is false",Precedence,0.04554428532719612,0.28295162320137024,0.1624156596759955,3 -X(p0 U p3),"In the next step, 'p0' until 'p3'",(X (p3 U p0)),"In the next step, 'p3' until 'p0'",BadStateQuantification,0.0900951400399208,0.4956358075141907,0.33615104605754215,3 -(((G p3) -> p2) U ((! ((G p3) -> p2)) & (p0 -> p3))),"If 'p3' must always hold, then 'p2' holds until both 'p3' must always hold, but not 'p2' and if 'p0' holds, then 'p3' holds",(((G p3) -> p2) U ((! (p3 -> p2)) & (p0 -> p3))),"If 'p3' must always hold, then 'p2' holds until both 'p3', but not 'p2' and if 'p0' holds, then 'p3' holds",ImplicitG,0.09025835990905762,0.34275302290916443,0.2114135151108106,6 -(X (((F p0) | p1) & ((X p1) & p2))),"In the next step, both either at some point, 'p0' will hold or 'p1' and both in the next step, 'p1' and 'p2'",((X ((F p0) | p1)) & ((X p1) & p2)),"Both in the next step, either at some point, 'p0' will hold or 'p1' and both in the next step, 'p1' and 'p2'",BadStateIndex,0.1026991754770279,0.4575364887714386,0.31032146140933037,4 -(((G p3) -> p0) U (((F p2) -> p1) & (G (G p3)))),"If 'p3' must always hold, then 'p0' holds until both if at some point, 'p2' will hold, then 'p1' holds and at all times, 'p3'",(((G p3) -> p0) U ((p2 -> p1) & (G (G p3)))),"If 'p3' must always hold, then 'p0' holds until both if 'p2' holds, then 'p1' holds and at all times, 'p3'",ImplicitF,0.12346068769693375,0.337312251329422,0.2065150427321593,6 -((((! p2) | p0) U p0) & (G (((! p2) | p0) -> (! p0)))),"Both either 'p2' is false or 'p0' hold until 'p0' and if either 'p2' is false or 'p0', then not 'p0' is always true",(((((! p2) | p0) U p0) | (G ((! p2) | p0))) & (G (((! p2) | p0) -> (! p0)))),"Both either 'p2' is false or 'p0' hold until 'p0' or always have either 'p2' is false or 'p0' and if either 'p2' is false or 'p0', then not 'p0' is always true",WeakU,0.1286027878522873,0.37017664313316345,0.24930460453033448,5 -(Fp3 U p0) U (p3 U Gp1),"At some point, 'p3' will hold until 'p0', and this continues until 'p3' until 'p1' must always hold",((((F p3) U p0) U p3) U (G p1)),"At some point, 'p3' will hold until 'p0' until 'p3', and this continues until 'p1' must always hold",Precedence,0.045582808554172516,0.35584917664527893,0.23125888283054033,6 -(((p1 & p0) U (F p2)) & (G ((p1 & p0) -> (! (F p2))))),"Both 'p1' and 'p0' hold until at some point, 'p2' will hold and at all times, if both 'p1' and 'p0', then not at some point, 'p2' will hold",(((p1 & p0) U (F p2)) & ((p1 & p0) -> (! (F p2)))),"Both 'p1' and 'p0' hold until at some point, 'p2' will hold and if both 'p1' and 'p0', then not at some point, 'p2' will hold",ImplicitG,0.09037087857723236,0.40757039189338684,0.26233986020088196,6 -Gp0 U (!p0 | (p1 & p3)),'p0' must always hold until either 'p0' is false or both 'p1' and 'p3',((G p0) U (G ((! p0) | (p1 & p3)))),'p0' must always hold until always have either 'p0' is false or both 'p1' and 'p3',BadStateQuantification,0.09152600914239883,0.41693347692489624,0.23366023153066634,5 -(X (((G p1) & p3) & (! p0))),"In the next step, both 'p1' must always hold and 'p3' and 'p0' is false",((X ((G p1) & p3)) & (! p0)),"Both in the next step, both 'p1' must always hold and 'p3' and 'p0' is false",BadStateIndex,0.10643599182367325,0.5495067834854126,0.30764263309538364,4 -((G p1) U ((! (G p1)) & ((F p1) | p3))),"'p1' must always hold until both it is not the case that 'p1' must always hold and either at some point, 'p1' will hold or 'p3'",(((G p1) U ((! (G p1)) & ((F p1) | p3))) | (G (G p1))),"Either 'p1' must always hold until both it is not the case that 'p1' must always hold and either at some point, 'p1' will hold or 'p3' or at all times, 'p1'",WeakU,0.12948283553123474,0.5531959533691406,0.2667570263147354,5 -(((X p3) -> p2) U ((! ((X p3) -> p2)) | ((F p3) & p0))),"If in the next step, 'p3', then 'p2' holds until either in the next step, 'p3', but not 'p2' or both at some point, 'p3' will hold and 'p0'",(((X p3) -> p2) U ((! ((X p3) -> p2)) | (p3 & p0))),"If in the next step, 'p3', then 'p2' holds until either in the next step, 'p3', but not 'p2' or both 'p3' and 'p0'",ImplicitF,0.13020284473896027,0.49387961626052856,0.260651171207428,6 -(p3 U Xp0) U (p2 U p1),"'p3' until in the next step, 'p0', and this continues until 'p2' until 'p1'",(((p3 U (X p0)) U p2) U p1),"'p3' until in the next step, 'p0' until 'p2', and this continues until 'p1'",Precedence,0.04631377384066582,0.42235496640205383,0.23479179944843054,4 -X(FGp3 U ((p3 U p1) U p2)),"In the next step, eventually, 'p3' will always be true until 'p3' until 'p1', and this continues until 'p2'",(X ((F (G p3)) U (F ((p3 U p1) U p2)))),"In the next step, eventually, 'p3' will always be true until eventually, 'p3' until 'p1', and this continues until 'p2'",BadStateQuantification,0.09275685995817184,0.4013374447822571,0.2730415426194668,6 -((! p3) U (p1 & (G ((F p3) -> p2)))),"'p3' is false until both 'p1' and at all times, if at some point, 'p3' will hold, then 'p2' holds",((! p3) U (p1 & ((F p3) -> p2))),"'p3' is false until both 'p1' and if at some point, 'p3' will hold, then 'p2' holds",ImplicitG,0.09401790797710419,0.6226906180381775,0.26009408065250944,7 -(X ((G p0) & (p1 -> p3))),"In the next step, both 'p0' must always hold and if 'p1' holds, then 'p3' holds",((X (G p0)) & (p1 -> p3)),"Both in the next step, 'p0' must always hold and if 'p1' holds, then 'p3' holds",BadStateIndex,0.10660488158464432,0.5265659689903259,0.28082766085863115,5 -((G p2) U (((F p3) & p2) & (F ((G p2) & p1)))),"'p2' must always hold until both at some point, 'p3' will hold and 'p2' and eventually 'p1' will occur, and from then on 'p2' will always hold",(((G p2) U (((F p3) & p2) & (F ((G p2) & p1)))) | (G (G p2))),"Either 'p2' must always hold until both at some point, 'p3' will hold and 'p2' and eventually 'p1' will occur, and from then on 'p2' will always hold or at all times, 'p2'",WeakU,0.13080976903438568,0.6666805744171143,0.32677003368735313,4 -((((F p3) & p0) U ((! p1) -> p0)) & (G (((F p3) & p0) -> (! ((! p1) -> p0))))),"Both at some point, 'p3' will hold and 'p0' hold until 'p0' unless 'p1' and if both at some point, 'p3' will hold and 'p0', then not 'p0' unless 'p1' is always true",((((F p3) & p0) U ((! p1) -> p0)) & (G ((p3 & p0) -> (! ((! p1) -> p0))))),"Both at some point, 'p3' will hold and 'p0' hold until 'p0' unless 'p1' and if both 'p3' and 'p0', then not 'p0' unless 'p1' is always true",ImplicitF,0.1309593915939331,0.3799649775028229,0.23854931071400642,4 +!p1 U XXp1,"'p1' is false until in 2 steps, 'p1'",((! p1) U (X (X (X p1)))),"'p1' is false until in 3 steps, 'p1'",BadStateIndex,0.16254232823848724,0.3727336823940277,0.29015181586146355,4 +Fp1 U (!p0 U Gp0),"At some point, 'p1' will hold until 'p0' is false until 'p0' must always hold",((F p1) U ((! p0) U p0)),"At some point, 'p1' will hold until 'p0' is false until 'p0'",ImplicitG,0.16381803154945374,0.44320714473724365,0.318364155292511,5 +(p1 U Xp0) U (p0 U Gp1),"'p1' until in the next step, 'p0', and this continues until 'p0' until 'p1' must always hold",(((p1 U (X p0)) U p0) U (G p1)),"'p1' until in the next step, 'p0' until 'p0', and this continues until 'p1' must always hold",Precedence,0.06078732758760452,0.4130331873893738,0.23652653247117997,5 +X(Gp0 U Gp1),"In the next step, 'p0' must always hold until 'p1' must always hold",(X ((G p1) U (G p0))),"In the next step, 'p1' must always hold until 'p0' must always hold",BadStateQuantification,0.08546637743711472,0.45085281133651733,0.23636372573673725,4 +!p1 | XXp1,"Either 'p1' is false or in 2 steps, 'p1'",((! p1) | (X (X (X (X p1))))),"Either 'p1' is false or in 4 steps, 'p1'",BadStateIndex,0.1634017676115036,0.3308771848678589,0.24713947623968124,2 +X(p0 U (G!p1 | (p1 & XFp1))),"In the next step, 'p0' until either 'p1' will never occur or both 'p1' and in the next step, at some point, 'p1' will hold",(X ((p0 U (G (! p1))) | (p1 & (X (F p1))))),"In the next step, either 'p0' until 'p1' will never occur or both 'p1' and in the next step, at some point, 'p1' will hold",Precedence,0.06203468143939972,0.3148716688156128,0.2041328489780426,5 +XG(!p0 | Xp1),"In the next step, always have either 'p0' is false or in the next step, 'p1'",(X ((! p0) | (X p1))),"In the next step, either 'p0' is false or in the next step, 'p1'",ImplicitG,0.16856099665164948,0.44863948225975037,0.28078072269757587,3 +(XFp0 & Gp1) | (XG!p0 & F!p1),"Either both in the next step, at some point, 'p0' will hold and 'p1' must always hold or both in the next step, 'p0' will never occur and eventually, not 'p1'",(((X (G p0)) & (F p1)) | ((X (F (! p0))) & (G (! p1)))),"Either both in the next step, 'p0' must always hold and at some point, 'p1' will hold or both in the next step, eventually, not 'p0' and 'p1' will never occur",BadStateQuantification,0.08862829953432083,0.4140421450138092,0.21038065403699874,5 +((F p1) U ((F p1) -> p1)),"At some point, 'p1' will hold until if at some point, 'p1' will hold, then 'p1' holds",(((F p1) U (F p1)) -> p1),"If at some point, 'p1' will hold until at some point, 'p1' will hold, then 'p1' holds",Precedence,0.06217395141720772,0.3283836841583252,0.2008910709992051,4 +X(!p0 & p1),"In the next step, both 'p0' is false and 'p1'",((X (! p0)) & p1),"Both in the next step, 'p0' is false and 'p1'",BadStateIndex,0.16448168456554413,0.6075959801673889,0.3860388323664665,2 diff --git a/src/templates/version.html b/src/templates/version.html index ee672d8..6f2d365 100644 --- a/src/templates/version.html +++ b/src/templates/version.html @@ -1 +1 @@ -1.9.1 \ No newline at end of file +1.9.2 \ No newline at end of file