<jupyter_start><jupyter_text>Tips:When using AND, OR of preference formulas, the atomic preferences must be enclosed in brackets.<jupyter_code>PrefScLTL("a > b")
PrefScLTL("a >= b")
PrefScLTL("a ~ b")
PrefScLTL("(a > b)")
PrefScLTL("(a > b) & (c >= d)")
PrefScLTL("(a > b) | (c >= d)")
PrefScLTL("Fa > (b U c)")
PrefScLTL("(a U b) ~ (b U c)")
PrefScLTL("((a > b) & (Fb > Fc)) | ((c U d) > (d))")<jupyter_output><empty_output><jupyter_text>Translation<jupyter_code>f = PrefScLTL("a > b")
aut = f.translate()
print(aut)
f = PrefScLTL("a > b")
aut = f.translate()
print(aut)
graph, final = aut.make_explicit()
%pylab inline  
# `pylab notebook`  # for interactive plots
import networkx as nx
# import holoviews as hv
import matplotlib.pyplot as plt
g1=graph
nx.draw_spectral(graph, with_labels=True, node_size=1500)

nx.draw_networkx(final, with_labels=True, node_size=1500)<jupyter_output><empty_output><jupyter_text>Inconsistent PreferencesConsider the preference specification `f = PrefScLTL("(a > b) & (b > a)")`. It appears to be inconsistent. However, observe its preference automaton. Neither are the sets of states or edges in preference graph empty, nor are there any cycles in the preference graph.<jupyter_code>f = PrefScLTL("(a > b) & (b > a)")
aut = f.translate()
print(aut)<jupyter_output>This PrefDfa has 81 states.
    Alphabet: {'b', 'a'}
    Starting state: ((1, 1), (1, 1))
    Accepting states: MultiDiGraph with 4 nodes and 1 edges
    States: [((0, 0), (0, 0)), ((0, 0), (0, 1)), ((0, 0), (0, 2)), ((0, 0), (1, 0)), ((0, 0), (1, 1)), ((0, 0), (1, 2)), ((0, 0), (2, 0)), ((0, 0), (2, 1)), ((0, 0), (2, 2)), ((0, 1), (0, 0)), ((0, 1), (0, 1)), ((0, 1), (0, 2)), ((0, 1), (1, 0)), ((0, 1), (1, 1)), ((0, 1), (1, 2)), ((0, 1), (2, 0)), ((0, 1), (2, 1)), ((0, 1), (2, 2)), ((0, 2), (0, 0)), ((0, 2), (0, 1)), ((0, 2), (0, 2)), ((0, 2), (1, 0)), ((0, 2), (1, 1)), ((0, 2), (1, 2)), ((0, 2), (2, 0)), ((0, 2), (2, 1)), ((0, 2), (2, 2)), ((1, 0), (0, 0)), ((1, 0), (0, 1)), ((1, 0), (0, 2)), ((1, 0), (1, 0)), ((1, 0), (1, 1)), ((1, 0), (1, 2)), ((1, 0), (2, 0)), ((1, 0), (2, 1)), ((1, 0), (2, 2)), ((1, 1), (0, 0)), ((1, 1), (0, 1)), ((1, 1), (0, 2)), ((1, 1), (1, 0)), ((1, 1), (1, 1)), ((1, 1), (1, 2)), ((1, 1), (2, 0)), ((1, 1), (2, 1)), ((1, 1), (2, 2)), ((1, 2), (0, 0)), ((1,[...]<jupyter_text>However, the inconsistency of the specification is understood by observing the states in `(X2, X2)` and `(X1, X1)`. The states `((0, 1), (0, 1))` in `(X1, X1)` is impossible to achieve since the state `1` in the DFAs of `a` and `b` correspond to initial states. Thus, after one step in MDP, the state in both DFAs must be either `0` or `2`. This manifests in product MDP as unreachable states. The state `((0, 2), (0, 2))` is also not possible since first `(0, 2)` says `a` is satisfied and `b` is not, whereas second `(0, 2)` says `b` is satisfied and `a` is not. Since this cannot happen simultaneously in MDP, any state `(s, ((0, 2), (0, 2)))` is unreachable from any initial state of MDP.   Interesting Case: OR-preferencesConsider the automaton for `f = PrefScLTL("(a > b) | (b > c)")`.<jupyter_code>f = PrefScLTL("(a > b) | (b > c)")
aut = f.translate()
print(aut)<jupyter_output>This PrefDfa has 81 states.
    Alphabet: {'c', 'b', 'a'}
    Starting state: ((1, 1), (1, 1))
    Accepting states: MultiDiGraph with 4 nodes and 7 edges
    States: [((0, 0), (0, 0)), ((0, 0), (0, 1)), ((0, 0), (0, 2)), ((0, 0), (1, 0)), ((0, 0), (1, 1)), ((0, 0), (1, 2)), ((0, 0), (2, 0)), ((0, 0), (2, 1)), ((0, 0), (2, 2)), ((0, 1), (0, 0)), ((0, 1), (0, 1)), ((0, 1), (0, 2)), ((0, 1), (1, 0)), ((0, 1), (1, 1)), ((0, 1), (1, 2)), ((0, 1), (2, 0)), ((0, 1), (2, 1)), ((0, 1), (2, 2)), ((0, 2), (0, 0)), ((0, 2), (0, 1)), ((0, 2), (0, 2)), ((0, 2), (1, 0)), ((0, 2), (1, 1)), ((0, 2), (1, 2)), ((0, 2), (2, 0)), ((0, 2), (2, 1)), ((0, 2), (2, 2)), ((1, 0), (0, 0)), ((1, 0), (0, 1)), ((1, 0), (0, 2)), ((1, 0), (1, 0)), ((1, 0), (1, 1)), ((1, 0), (1, 2)), ((1, 0), (2, 0)), ((1, 0), (2, 1)), ((1, 0), (2, 2)), ((1, 1), (0, 0)), ((1, 1), (0, 1)), ((1, 1), (0, 2)), ((1, 1), (1, 0)), ((1, 1), (1, 1)), ((1, 1), (1, 2)), ((1, 1), (2, 0)), ((1, 1), (2, 1)), ((1, 1), (2, 2)), ((1, 2), (0, 0)),[...]<jupyter_text>Notice that the preference graph has cycles. This is expected by the way we define OR automaton construction. ```Edges: 	('X1', 'X2') --> ('X1', 'X1')	('X1', 'X2') --> ('X2', 'X1')	('X2', 'X1') --> ('X1', 'X1')	('X2', 'X1') --> ('X1', 'X2')	('X2', 'X2') --> ('X1', 'X1')	('X2', 'X2') --> ('X1', 'X2')	('X2', 'X2') --> ('X2', 'X1')```    **However, this hinders applicability of our current ranking scheme.** In this case, should we rank SCC's in preference graph. On a theoretical level, notice in the plot below that automaton does not have any cycles. Thus, although there are loops (e.g. `(X1, X2) -> (X2, X1) -> (X1, X2)`), such a loop cannot be realized by the underlying graph of automaton. This means the given specification is consistent. **Q. Is it correct to assume that an inconsistent formula will induce a loop in underlying structure?**<jupyter_code>%pylab inline  
# `pylab notebook`  # for interactive plots
import networkx as nx
# import holoviews as hv
import matplotlib.pyplot as plt
plt.rcParams['figure.figsize'] = [20, 20]

graph, final = aut.make_explicit()
nx.draw_spring(graph, with_labels=True, node_size=1500)

for cycle in nx.find_cycle(graph):
    print(cycle)<jupyter_output>(((0, 0), (0, 0)), ((0, 0), (0, 0)), 0)<jupyter_text>Toy problem with synthesis. A small MDP with simple specification.<jupyter_code>from ggsolver.ggsolver.ds import RandomizedStrategy
from ggsolver.ggsolver.mdp.model import MdpGame
from ggsolver.ggsolver.mdp.solvers import ASWinReach
from logic.pref_scltl import PrefScLTL
from planner import *

f = PrefScLTL("(p > q)")
print(f)

pref_dfa = f.translate()
print(pref_dfa)

graph = nx.MultiDiGraph()
graph.add_nodes_from([1, 2, 3])
graph.add_edges_from([(1, 2, {'action': "a"}), (1, 3, {'action': 'b'}), (2, 3, {'action': 'c'})])

mdp = MdpGame("MDP")
mdp.construct_explicit(graph, is_qualitative=True)
label_map = {1: {"p"}, 2: {"q"}, 3: {"p"}}
mdp.make_labeled({"a", "b"}, lambda x: label_map[x])
print(mdp)

prod_mdp = ProductMdp("product_mdp")
prod_mdp.construct(mdp, pref_dfa)
print(prod_mdp.succ((1, (1, 1))))
print(prod_mdp.pred((3, (0, 2))))

strategy = synthesize_strategy(prod_mdp)

print()
print("strategy at (1, (1, 1)): ", strategy[(1, (1, 1))])
print(prod_mdp.delta((1, (1, 1)), 'a'))
print(prod_mdp.delta((1, (1, 1)), 'b'))

print()<jupyter_output><logic.pref_scltl.Strict object at 0x7f7497115b00>

    This PrefDfa has 9 states.
    Alphabet: {'q', 'p'}
    Starting state: (1, 1)
    Accepting states: MultiDiGraph with 2 nodes and 1 edges
    States: [(0, 0), (0, 1), (0, 2), (1, 0), (1, 1), (1, 2), (2, 0), (2, 1), (2, 2)]
    Transition function:
		(0, 0) -- {} --> (0, 0)
		(0, 0) -- {'q'} --> (0, 0)
		(0, 0) -- {'p'} --> (0, 0)
		(0, 0) -- {'q', 'p'} --> (0, 0)
		(0, 1) -- {} --> (0, 2)
		(0, 1) -- {'q'} --> (0, 0)
		(0, 1) -- {'p'} --> (0, 2)
		(0, 1) -- {'q', 'p'} --> (0, 2)
		(0, 2) -- {} --> (0, 2)
		(0, 2) -- {'q'} --> (0, 2)
		(0, 2) -- {'p'} --> (0, 2)
		(0, 2) -- {'q', 'p'} --> (0, 2)
		(1, 0) -- {} --> (2, 0)
		(1, 0) -- {'q'} --> (2, 0)
		(1, 0) -- {'p'} --> (0, 0)
		(1, 0) -- {'q', 'p'} --> (2, 0)
		(1, 1) -- {} --> (2, 2)
		(1, 1) -- {'q'} --> (2, 0)
		(1, 1) -- {'p'} --> (0, 2)
		(1, 1) -- {'q', 'p'} --> (2, 2)
		(1, 2) -- {} --> (2, 2)
		(1, 2) -- {'q'} --> (2, 2)
		(1, 2) -- {'p'} --> (0, 2)
		(1, 2) -- {'q', 'p'[...]<jupyter_text>Example 2. Synthesis with AND-ing.<jupyter_code>f = PrefScLTL("(p > q) & (p > r)")
    # f = PrefScLTL("(p > q)")
    print(f)

    pref_dfa = f.translate()
    print(pref_dfa)

    graph = nx.MultiDiGraph()
    graph.add_nodes_from([1, 2, 3])
    graph.add_edges_from([(1, 2, {'action': "a"}), (1, 3, {'action': 'b'}), (2, 3, {'action': 'c'})])

    mdp = MdpGame("MDP")
    mdp.construct_explicit(graph, is_qualitative=True)
    label_map = {1: {"q"}, 2: {"p"}, 3: {"r"}}
    mdp.make_labeled({"p", "q", "r"}, lambda x: label_map[x])
    print(mdp)

    prod_mdp = ProductMdp("product_mdp")
    prod_mdp.construct(mdp, pref_dfa)
    # print(prod_mdp.succ((1, (1, 1))))
    # print(prod_mdp.pred((3, (0, 2))))

    strategy = synthesize_strategy(prod_mdp)

    for k in strategy.keys():
        print(k, strategy[k])
    # print("strategy at (1, (1, 1)): ", strategy[(1, (1, 1))])
    print(prod_mdp.delta((1, ((1, 1), (1, 1))), 'a'))
    print(prod_mdp.delta((1, ((1, 1), (1, 1))), 'b'))
    print(prod_mdp.pred((2, ((0, 2), (0, 2)))))         # TODO. Mistake here!
    #
    # print()<jupyter_output><empty_output><jupyter_text>Example for paper.<jupyter_code>f = PrefScLTL("(Fb > Fa) & (Fc > Fa) & (Fe > Fa) & (Fd > Fb) & (Fd > Fc)")
aut = f.translate()
len(aut.states())
f = PrefScLTL("(F(b | c | e) > Fa) & (Fd > Fb) & (Fd > Fc)")
aut = f.translate()
len(aut.states())
f = PrefScLTL("(Fb > Fa) | (Fe > Fa)")
aut = f.translate()
print(aut)
graph, _ = aut.make_explicit()
reachable = nx.descendants(graph, ((1, 1), (1, 1)))
valid_reachable = [((q0, q1), (q2, q3)) for ((q0, q1), (q2, q3)) in reachable if q1 == q3]
valid_reachable
f = PrefScLTL("(Fb > Fa) | (Fe > Fa)")
aut = f.translate()
print(aut)<jupyter_output><empty_output>
{'fraction_non_alphanumeric': 0.2799913848804652, 'fraction_numerical': 0.07344389403402972, 'mean_word_length': 3.8244155844155845, 'pattern_counts': {'":': 0, '<': 30, '<?xml version=': 0, '>': 99, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '8', 'dir': 'jupyter-structured-clean-dedup', 'id': '602684', 'license': 'BSD-3-Clause', 'n_tokens_mistral': 4456, 'n_tokens_neox': 4038, 'n_words': 1291, 'path': 'jp-notebooks/pref-scltl-test.ipynb', 'repo_name': 'abhibp1993/preference-planning', 'size': '9286'}