diff --git a/src/exercisebuilder.py b/src/exercisebuilder.py
index ae82d31..04ceb6b 100644
--- a/src/exercisebuilder.py
+++ b/src/exercisebuilder.py
@@ -20,6 +20,8 @@ class ExerciseBuilder:
def __init__(self, userLogs, complexity=5):
self.userLogs = userLogs
+ self.numUserLogs = len(userLogs)
+
self.DEFAULT_WEIGHT = 0.7
self.ltl_priorities = spotutils.DEFAULT_LTL_PRIORITIES.copy()
@@ -163,8 +165,10 @@ def contains_undersirable_lit(s):
TAUTOLOGY = r'\b1\b'
UNSAT = r'\b0\b'
# remove all the parens
- y = s.replace('(', '').replace(')', '')
- return bool(re.search(TAUTOLOGY, y)) or bool(re.search(UNSAT, y))
+ y = s.replace('(', ' ').replace(')', ' ').replace("'", ' ')
+ x = bool(re.search(TAUTOLOGY, y)) or bool(re.search(UNSAT, y))
+
+ return x
self.set_ltl_priorities()
@@ -200,14 +204,54 @@ def contains_undersirable_lit(s):
if question is not None:
questions.append(question)
- ## Make sure we have enough questions
- chosen_questions = random.sample(questions, min(num_questions, len(questions)))
- return chosen_questions
+ def formula_choice_metric(question):
+
+ formula = question['question']
+ if question['type'] == self.ENGLISHTOLTL:
+ formula = question['answer']
+
+ temporal_op_count = formula.count('G') + formula.count('X') + formula.count('U') + formula.count('F')
+ aut_size = spotutils.get_aut_size(formula)
+
+
+ scaled_aut_size = aut_size * math.log(self.numUserLogs + 1)
+ return temporal_op_count + scaled_aut_size
+
+ chosen_questions = sorted(questions, key=formula_choice_metric, reverse=True)[:num_questions]
+
+
+ # Now choose the question with the highest metric, that is of each type from the chosen_questions
+
+ highest_ltl_to_eng = next((q for q in chosen_questions if q['type'] == self.ENGLISHTOLTL), None)
+ highest_trace_sat_mc = next((q for q in chosen_questions if q['type'] == self.TRACESATMC), None)
+ highest_trace_sat_yn = next((q for q in chosen_questions if q['type'] == self.TRACESATYN), None)
+
+
+ final_choices = []
+ if highest_ltl_to_eng is not None:
+ final_choices.append(highest_ltl_to_eng)
+ if highest_trace_sat_mc is not None:
+ final_choices.append(highest_trace_sat_mc)
+ if highest_trace_sat_yn is not None:
+ final_choices.append(highest_trace_sat_yn)
+
+ remaining = num_questions - len(final_choices)
+ if remaining > 0:
+ # Add the remaining questions from chosen_questions, but dont add the ones already added
+ for q in chosen_questions:
+ if q not in final_choices:
+ final_choices.append(q)
+ remaining -= 1
+ if remaining <= 0:
+ break
+ return remaining
+
def gen_nl_question(self, formula):
formula_eng = ltlnode.parse_ltl_string(formula).__to_english__()
- #print("Generating NL question for " + formula + " and got " + str(formula_eng))
+ if formula_eng is None or formula_eng == "":
+ return None
### If there are multiple '.' in a row, replace with a single '.'
formula_eng = re.sub(r'\.{2,}', '.', formula_eng)
@@ -251,8 +295,14 @@ def build_english_to_ltl_question(self, answer):
if options is None:
return None
+ question = self.gen_nl_question(answer)
+
+ if question is None or question == "":
+ print("Question generation failed unexpectedly.")
+ return None
+
return {
- "question": self.gen_nl_question(answer),
+ "question": question,
"type": self.ENGLISHTOLTL,
"options": options
}
diff --git a/src/ltlnode.py b/src/ltlnode.py
index 9eb6c43..d829fef 100644
--- a/src/ltlnode.py
+++ b/src/ltlnode.py
@@ -7,6 +7,8 @@
from ltlParser import ltlParser
from abc import ABC, abstractmethod
from spotutils import areEquivalent
+import random
+import ltltoeng
## We use this for Grammatical englsih generation
import spacy
@@ -37,6 +39,11 @@ def __str__(self):
@abstractmethod
def __to_english__(self):
+ x = ltltoeng.apply_special_pattern_if_possible(self)
+ if x is not None:
+ return x
+ # We should draw inspiration from:
+ # https://matthewbdwyer.github.io/psp/patterns/ltl.html
pass
@staticmethod
@@ -134,6 +141,9 @@ def __str__(self):
return f'({self.operator} {str(self.operand)})'
def __to_english__(self):
+ x = ltltoeng.apply_special_pattern_if_possible(self)
+ if x is not None:
+ return x
return self.__str__()
@@ -148,6 +158,9 @@ def __str__(self):
return f'({str(self.left)} {self.operator} {str(self.right)})'
def __to_english__(self):
+ x = ltltoeng.apply_special_pattern_if_possible(self)
+ if x is not None:
+ return x
return self.__str__()
@@ -160,6 +173,12 @@ def __str__(self):
return self.value
def __to_english__(self):
+ x = ltltoeng.apply_special_pattern_if_possible(self)
+ if x is not None:
+ return x
+
+ ### TODO: COuld we override so that this is more meaningful
+ # for some cases?
return f"'{self.value}' holds"
@@ -169,6 +188,9 @@ def __init__(self, left, right):
super().__init__(UntilNode.symbol, left, right)
def __to_english__(self):
+ x = ltltoeng.apply_special_pattern_if_possible(self)
+ if x is not None:
+ return x
lhs = self.left.__to_english__()
rhs = self.right.__to_english__()
english = f"{lhs} until {rhs}."
@@ -181,6 +203,9 @@ def __init__(self, operand):
super().__init__(NextNode.symbol, operand)
def __to_english__(self):
+ x = ltltoeng.apply_special_pattern_if_possible(self)
+ if x is not None:
+ return x
op = self.operand.__to_english__()
english = f"in the next state, {op}."
return self.corrected_sentence(english)
@@ -192,8 +217,19 @@ def __init__(self, operand):
super().__init__(GloballyNode.symbol, operand)
def __to_english__(self):
+ x = ltltoeng.apply_special_pattern_if_possible(self)
+ if x is not None:
+ return x
+
+
op = self.operand.__to_english__()
- english = f"from this point on, {op}."
+ patterns = [
+ f"it is always the case that {op}",
+ f"in all future states, {op}",
+ f"globally, {op}"
+ ]
+
+ english = random.choice(patterns)
return self.corrected_sentence(english)
@@ -203,8 +239,19 @@ def __init__(self, operand):
super().__init__(FinallyNode.symbol, operand)
def __to_english__(self):
+ x = ltltoeng.apply_special_pattern_if_possible(self)
+ if x is not None:
+ return x
op = self.operand.__to_english__()
- english = f"eventually, {op}."
+
+ patterns = [
+ f"eventually, {op}",
+ f"now or in the future, {op}",
+ f"at this or some future point, {op}"
+ ]
+
+
+ english = f"eventually, {op}"
return self.corrected_sentence(english)
@@ -216,6 +263,9 @@ def __init__(self, left, right):
super().__init__(OrNode.symbol, left, right)
def __to_english__(self):
+ x = ltltoeng.apply_special_pattern_if_possible(self)
+ if x is not None:
+ return x
lhs = self.left.__to_english__()
rhs = self.right.__to_english__()
english = f"{lhs} or {rhs}."
@@ -228,6 +278,9 @@ def __init__(self, left, right):
super().__init__(AndNode.symbol, left, right)
def __to_english__(self):
+ x = ltltoeng.apply_special_pattern_if_possible(self)
+ if x is not None:
+ return x
lhs = self.left.__to_english__()
rhs = self.right.__to_english__()
english = f"{lhs} and {rhs}."
@@ -240,8 +293,21 @@ def __init__(self, operand):
super().__init__(NotNode.symbol, operand)
def __to_english__(self):
+ x = ltltoeng.apply_special_pattern_if_possible(self)
+ if x is not None:
+ return x
+
op = self.operand.__to_english__()
- english = f"it is not the case that {op}."
+
+ ## If the operand is a literal, we can just negate it
+ if isinstance(self.operand, LiteralNode):
+ english = f"{op}"
+ # Replace 'holds' with does not hold in english.
+ if "holds" in english:
+ english = english.replace("holds", "does not hold")
+ ## TODO: We can start donig some more. better special cases.
+ else:
+ english = f"it is not the case that {op}."
return self.corrected_sentence(english)
class ImpliesNode(BinaryOperatorNode):
@@ -252,7 +318,15 @@ def __init__(self, left, right):
def __to_english__(self,depth=0):
lhs = self.left.__to_english__()
rhs = self.right.__to_english__()
- english = f"if {lhs} then {rhs}."
+
+ # Potential patterns:
+ patterns = [
+ f"if {lhs}, then {rhs}",
+ f"{rhs} is necessary for {lhs}"
+ ]
+
+ # Choose a pattern randomly, and then return the corrected sentence
+ english = random.choice(patterns)
return self.corrected_sentence(english)
@@ -262,9 +336,22 @@ def __init__(self, left, right):
super().__init__(EquivalenceNode.symbol, left, right)
def __to_english__(self):
+ x = ltltoeng.apply_special_pattern_if_possible(self)
+ if x is not None:
+ return x
lhs = self.left.__to_english__()
rhs = self.right.__to_english__()
- english = f"{lhs} if and only if {rhs}."
+
+ # Potential patterns:
+ patterns = [
+ f"{lhs} is necessary and sufficient for {rhs}",
+ f"{lhs} exactly when {rhs}",
+ f"{lhs} is equivalent to {rhs}",
+ f"{lhs} if and only if {rhs}"
+ ]
+
+ # Choose a pattern randomly, and then return the corrected sentence
+ english = random.choice(patterns)
return self.corrected_sentence(english)
diff --git a/src/ltltoeng.py b/src/ltltoeng.py
index 6ad573c..298c479 100644
--- a/src/ltltoeng.py
+++ b/src/ltltoeng.py
@@ -1,41 +1,196 @@
-# from transformers import pipeline
-# import spacy
-
-# nlp = spacy.load("en_core_web_sm")
-
-# generator = pipeline('text-generation', model='distilgpt2')
-
-# # Function to generate a grammatically correct sentence using a transformer model
-# def generate_grammatically_correct_sentence(english_sentence):
-# prompt = f"Translate this logical expression to a grammatically correct English sentence: {english_sentence}."
-# result = generator(prompt, max_length=50, num_return_sequences=1)
-# return result[0]['generated_text']
-
-
-# def ltl_to_english_sentence(ltl_formula):
-# print("Translating " + str(ltl_formula) + " to English")
-# english_phrases = ltl_formula.__to_english__()
-# prompt = english_phrases
-# print("Symbolic pass: " + prompt)
-
-# #english_sentence = generate_text(model, tokenizer, prompt)
-
-# doc = nlp(prompt)
-# corrected_sentence = ' '.join([token.text for token in doc])
-
-
-# print("After SpaCy pass (directly on symbolic): " + corrected_sentence)
-
-# y = generate_grammatically_correct_sentence(prompt)
-# print("After transformer pass (directly on symbolic): " + y)
-
-
-# return corrected_sentence
-
-
-# from transformers import pipeline
-
-
+import ltlnode
+import random
+
+## We should list the various patterns of LTL formulae that we can handle
+
+### What do we do about nested Globally and Finally nodes? ###
+
+patterns = []
+def pattern(func):
+ patterns.append(func)
+ return func
+
+
+#### Globally special cases ####
+
+# Pattern: G ( p -> (F q) )
+# English, whenever p (holds), eventually q will (hold)
+
+@pattern
+def response_pattern_to_english(node):
+ if type(node) is ltlnode.GloballyNode:
+ op = node.operand
+ if type(op) is ltlnode.ImpliesNode:
+ left = op.left
+ right = op.right
+ if type(right) is ltlnode.FinallyNode:
+ return "whenever " + left.__to_english__() + ", eventually " + right.operand.__to_english__()
+
+ return None
+
+
+# Pattern G (F p)
+# English: p (happens) repeatedly TODO: Think about how to properly phrase this
+@pattern
+def recurrence_pattern_to_english(node):
+ if type(node) is ltlnode.GloballyNode:
+ op = node.operand
+ if type(op) is ltlnode.FinallyNode:
+
+ inner_op = op.operand
+ if type(inner_op) is ltlnode.LiteralNode:
+ return f"'{inner_op.value}' will repeatedly hold"
+ return "there will always be a point in the future where " + op.operand.__to_english__()
+ return None
+
+
+## Chain precedence
+# Pattern G(p -> (X (q U r)))
+# English: Whenever p (happens), q will (hold) until r (holds)
+
+@pattern
+def chain_precedence_pattern_to_english(node):
+ if type(node) is ltlnode.GloballyNode:
+ op = node.operand
+ if type(op) is ltlnode.ImpliesNode:
+ left = op.left
+ right = op.right
+ if type(right) is ltlnode.UntilNode:
+ lhs = right.left
+ rhs = right.right
+ return "whenever " + left.__to_english__() + ", " + lhs.__to_english__() + " until " + rhs.__to_english__()
+ return None
+
+
+## Chain response
+# Pattern: G (p -> ( (F q) & (F r) ) )
+# English: Whenever p (holds), q and r will (hold) eventually
+@pattern
+def chain_response_pattern_to_english(node):
+ if type(node) is ltlnode.GloballyNode:
+ op = node.operand
+ if type(op) is ltlnode.ImpliesNode:
+ left = op.left
+ right = op.right
+ if type(right) is ltlnode.AndNode:
+ lhs = right.left
+ rhs = right.right
+ if type(lhs) is ltlnode.FinallyNode and type(rhs) is ltlnode.FinallyNode:
+ return "whenever " + left.__to_english__() + ", eventually" + lhs.operand.__to_english__() + " and " + rhs.operand.__to_english__()
+ return None
+
+
+## G !p
+# English: It will never be the case that p (holds)
+@pattern
+def never_globally_pattern_to_english(node):
+ if type(node) is ltlnode.GloballyNode:
+ op = node.operand
+ if type(op) is ltlnode.NotNode:
+
+ negated = op.operand
+ if type(negated) is ltlnode.LiteralNode:
+ return f"'{negated.value}' will never hold"
+
+ return "it will never be the case that " + op.operand.__to_english__()
+
+
+##### Finally special cases ####
+
+# F ( !p )
+# English: Eventually, it will not be the case that p (holds)
+@pattern
+def finally_not_pattern_to_english(node):
+ if type(node) is ltlnode.FinallyNode:
+ op = node.operand
+ if type(op) is ltlnode.NotNode:
+ return "eventually, it will not be the case that " + op.operand.__to_english__()
+ return None
+
+
+# F (G !p)
+# English: Eventually, it will never be the case that p (holds)
+@pattern
+def finally_never_globally_pattern_to_english(node):
+ if type(node) is ltlnode.FinallyNode:
+ op = node.operand
+ if type(op) is ltlnode.GloballyNode:
+ negated = op.operand
+ if type(negated) is ltlnode.NotNode:
+ return "eventually, it will never be the case that " + negated.operand.__to_english__()
+ return None
+
+
+# F (G p)
+# English: Eventually, p will always (hold)
+@pattern
+def finally_globally_pattern_to_english(node):
+ if type(node) is ltlnode.FinallyNode:
+ op = node.operand
+ if type(op) is ltlnode.GloballyNode:
+ return "eventually, it will always be the case that " + op.operand.__to_english__()
+ return None
+
+
+# F (p & q)
+# English: Eventually at the same time, p and q will (hold)
+@pattern
+def finally_and_pattern_to_english(node):
+ if type(node) is ltlnode.FinallyNode:
+ op = node.operand
+ if type(op) is ltlnode.AndNode:
+ return "eventually at the same time, " + op.left.__to_english__() + " and " + op.right.__to_english__()
+ return None
+
+# ! (F p)
+# English: It will never be the case that p (holds)
+@pattern
+def not_finally_pattern_to_english(node):
+ if type(node) is ltlnode.NotNode:
+ op = node.operand
+ if type(op) is ltlnode.FinallyNode:
+ return "it will never be the case that " + op.operand.__to_english__()
+ return None
+
+### Until special cases ###
+
+# (p U q) U r
+# English: p will (hold) until q (holds), and this will continue until r (holds)
+@pattern
+def nested_until_pattern_to_english(node):
+ if type(node) is ltlnode.UntilNode:
+ left = node.left
+ right = node.right
+ if type(left) is ltlnode.UntilNode:
+ return "it will be the case that " + left.left.__to_english__() + " until " + left.right.__to_english__() + ", and this will continue until " + right.__to_english__()
+ return None
+
+#### neXt special cases ####
+
+# X X X X r
+# English: In _n_ states, r will (hold)
+@pattern
+def apply_next_special_pattern_if_possible(node):
+
+ number_of_nexts = 0
+
+ while type(node) is ltlnode.NextNode:
+ number_of_nexts += 1
+ node = node.operand
+
+ if number_of_nexts > 1:
+ return "In " + str(number_of_nexts) + " states, " + node.__to_english__()
+ return None
+
+
+def apply_special_pattern_if_possible(node):
+
+ for pattern in patterns:
+ result = pattern(node)
+ if result is not None:
+ print("Pattern matched: " + str(result))
+ return result
+ return None
diff --git a/src/spotutils.py b/src/spotutils.py
index 298cf92..39a4e19 100644
--- a/src/spotutils.py
+++ b/src/spotutils.py
@@ -140,4 +140,11 @@ def to_priority_string(d):
## Returns the Mana Pneulli classification of the formula
def get_mana_pneulli_class(formula):
f = spot.formula(formula)
- return spot.mp_class(f, 'v')
\ No newline at end of file
+ return spot.mp_class(f, 'v')
+
+
+def get_aut_size(formula):
+ f = spot.formula(formula)
+ aut = spot.translate(f)
+ num_states = aut.num_states()
+ return num_states
\ No newline at end of file
diff --git a/src/static/img/overlap.png b/src/static/img/overlap.png
index f3c6adb..a7a1a47 100644
Binary files a/src/static/img/overlap.png and b/src/static/img/overlap.png differ
diff --git a/src/templates/index.html b/src/templates/index.html
index 9fcabc8..6114fd4 100644
--- a/src/templates/index.html
+++ b/src/templates/index.html
@@ -28,7 +28,7 @@ Getting Started with this tool?
Once you are familiar with LTL syntax used by this tool, we recommend
- starting with this initial exercise..
+ starting with this initial exercise.