"""
author Shuhao Qi
"""
import itertools
import re
from dataclasses import dataclass
import matplotlib.pyplot as plt
import networkx as nx
import pygraphviz as pgv
from ltlf2dfa.parser.ltlf import LTLfParser
from networkx.drawing.nx_agraph import from_agraph
[docs]
@dataclass
class DFA:
"""Deterministic Finite Automaton representation.
Represents a DFA with states, alphabet, transitions, and sink states.
Used to encode Linear Temporal Logic (LTL) specifications.
Attributes
----------
states:
List of state indices in the DFA
alphabet:
List of alphabet symbols (atomic propositions)
transitions:
Dictionary mapping (state, symbol) to next state
initial_state:
The starting state of the DFA
sink_states:
List of accepting or sink states
AP:
List of atomic propositions
"""
states: "list[int]"
alphabet: "list[str]"
transitions: "dict[tuple[int, tuple[bool, ...]], int]"
initial_state: int
sink_states: "list[int]"
AP: "list[str]"
[docs]
def get_alphabet(self, letter: str) -> "tuple[bool, ...]":
# Create a tuple based on the presence of each letter in ap_set in the string 'letter'
return tuple(ap in letter for ap in self.AP)
[docs]
def is_sink_state(self, state: int) -> bool:
return state in self.sink_states
[docs]
@classmethod
def from_spec(cls, spec: str, AP_set: "list[str] | None" = None) -> "DFA":
if AP_set is None:
AP_set = list(set(re.findall(r"[a-z]", spec)))
ltl_spec = LTL_Spec(spec, AP_set)
return ltl_spec.dfa
[docs]
@classmethod
def null_dfa(cls) -> "DFA":
return cls(
states=[],
alphabet=[],
transitions={},
initial_state=0,
sink_states=[],
AP=[],
)
[docs]
class LTL_Spec:
"""Linear Temporal Logic specification translator.
Converts LTL formula strings to DFA representations using the ltlf2dfa library.
Supports atomic propositions and standard LTL operators.
"""
def __init__(self, spec: str, AP_set: "list[str]"):
self.spec = spec
self.AP = AP_set
self.alphabet_set = tuple(itertools.product((True, False), repeat=len(self.AP)))
self.dfa = self.translate(spec)
assert set(re.findall(r"[a-z]", spec)) == set(self.AP), "AP_set and spec lowercase letters do not match"
assert len(set(AP_set)) == len(AP_set), "AP_set must contain unique elements"
[docs]
def translate(self, spec):
parser = LTLfParser()
formula = parser(spec) # returns an LTLfFormula
dfa_dot = formula.to_dfa()
dfa_graph = self.to_network(dfa_dot)
edges_info = {edge: label["label"] if "label" in label else None for edge, label in dfa_graph.edges.items()}
state_set = [*range(1, len(dfa_graph.nodes))]
trans_condition: "dict[tuple[int, int, int], str]" = {}
sink_states = []
initial_state = 0
for edge, label in edges_info.items():
if label is not None:
trans_condition[(int(edge[0]), int(edge[1]), int(edge[2]))] = label
if (label == "true") and (edge[0] == edge[1]):
sink_states.append(int(edge[0]))
if (edge[0] == "init") and (label is None):
initial_state = int(edge[1])
transitions_set = self.gen_transition(trans_condition)
dfa = DFA(
states=state_set,
alphabet=self.alphabet_set,
transitions=transitions_set,
initial_state=initial_state,
sink_states=sink_states,
AP=self.AP,
)
return dfa
[docs]
def get_alphabet(self, letter):
# Create a tuple based on the presence of each letter in ap_set in the string 'letter'
return tuple(ap in letter for ap in self.AP)
[docs]
def gen_transition(
self, trans_condition: "dict[tuple[int, int, int], str]"
) -> "dict[tuple[int, tuple[bool, ...]], int]":
def parse_expression(expression):
# Replace logical operators with Python equivalents
expression = expression.replace("&", " and ")
expression = expression.replace("|", " or ")
expression = expression.replace("~", " not ")
return expression
def evaluate_condition(condition, AP_set: "list[str]", letter: "tuple[bool, ...]"):
expression = parse_expression(condition)
# Create a dictionary to map words to their boolean values
# Replace words in the expression with their boolean values
for AP, value in zip(AP_set, letter):
expression = re.sub(r"\b" + AP + r"\b", str(value), expression)
# Evaluate the final expression
return eval(expression)
transition_set = {}
for edge, condition in trans_condition.items():
for letter in self.alphabet_set:
if condition == "true":
transition_set[(edge[0], letter)] = edge[1]
else:
if evaluate_condition(condition, self.AP, letter):
transition_set[(edge[0], letter)] = edge[1]
return transition_set
[docs]
def to_network(self, dfa_dot, plot: bool = False):
agraph = pgv.AGraph(string=dfa_dot)
dfa_graph = from_agraph(agraph)
if plot:
pos = nx.spring_layout(dfa_graph)
nx.draw(dfa_graph, pos, with_labels=True)
plt.show()
return dfa_graph
if __name__ == "__main__":
# The syntax of LTLf is defined in the link: http://ltlf2dfa.diag.uniroma1.it/ltlf_syntax
# AP_set = ['n', 'v', 'i', 'g']
# safe_frag = Translate("G(!n & !v) & G(!i U g)", AP_set)
safe_spec = LTL_Spec("G(~i U g) & G(~v) & G(~n)", AP_set=["i", "g", "v", "n"])
# print(safe_frag.get_alphabet('r&o'))
# scltl_frag = Translate("F(t)", ['t'])