<jupyter_start><jupyter_text>Verification of L-CSS SemanticsConsider two words, $w_1, w_2 \in \Sigma^\omega$ such that * $w_1 \models \varphi_1 \land \varphi_2$,* $w_2 \models \varphi_3$.There are $64$ possible preferences between the three outcomes since for any $i, j = 1, 2, 3$ and $i \neq j$, we may have * $(\varphi_i,\varphi_j) \in P$;* $(\varphi_j,\varphi_i) \in P$;* $(\varphi_i,\varphi_j) \in I$;* $(\varphi_i,\varphi_j) \in J$.In this notebook, we first generate all 64 cases. For each case, we apply our procedure in L-CSS paper to determine the relation between $w_1, w_2$ based on $\succeq$. We **manually** verify if the $\succeq$ is correct.   **In this notebook, we ignore I, since it can be merged into P, J by OR-ing of indifferent formulas.**<jupyter_code>RELATIONS = ["->", "<-", "||"] 
OUTCOMES = ["o1", "o2", "o3"]
from itertools import product

cases = []
cases_str = []
icount = 0
for r12, r23, r31 in product(RELATIONS, RELATIONS, RELATIONS):
    P = set()
    R = set()
    I = set()
    J = set()
    
    if r12 == "->":
        R.add(("o1", "o2"))
        P.add(("o2", "o1"))
    elif r12 == "<-":
        R.add(("o2", "o1"))
        P.add(("o1", "o2"))
    else: # r12 == "||":
        J.add(("o1", "o2"))
        J.add(("o2", "o1"))
        
    if r23 == "->":
        R.add(("o2", "o3"))
        P.add(("o3", "o2"))
    elif r23 == "<-":
        R.add(("o3", "o2"))
        P.add(("o2", "o3"))
    else: # r23 == "||":
        J.add(("o2", "o3"))
        J.add(("o3", "o2"))
        
    if r31 == "->":
        R.add(("o3", "o1"))
        P.add(("o1", "o3"))
    elif r31 == "<-":
        R.add(("o1", "o3"))
        P.add(("o3", "o1"))
    else: # r31 == "||":
        J.add(("o3", "o1"))
        J.add(("o1", "o3"))
    
    
    icount += 1
    cases.append((f"{icount}: \to1 {r12} o2, \to2 {r23} o3, \to3 {r31} o1", P, R, I, J))
    cases_str.append(f"{icount}: \to1 {r12} o2, \to2 {r23} o3, \to3 {r31} o1")

for case in cases:
    print(f"{case[0]}: \n\tP: {case[1]}, \n\tR: {case[2]}, \n\tI: {case[3]}, \n\tJ: {case[4]}")<jupyter_output>1: 	o1 -> o2, 	o2 -> o3, 	o3 -> o1: 
	P: {('o2', 'o1'), ('o1', 'o3'), ('o3', 'o2')}, 
	R: {('o2', 'o3'), ('o1', 'o2'), ('o3', 'o1')}, 
	I: set(), 
	J: set()
2: 	o1 -> o2, 	o2 -> o3, 	o3 <- o1: 
	P: {('o2', 'o1'), ('o3', 'o1'), ('o3', 'o2')}, 
	R: {('o2', 'o3'), ('o1', 'o2'), ('o1', 'o3')}, 
	I: set(), 
	J: set()
3: 	o1 -> o2, 	o2 -> o3, 	o3 || o1: 
	P: {('o2', 'o1'), ('o3', 'o2')}, 
	R: {('o2', 'o3'), ('o1', 'o2')}, 
	I: set(), 
	J: {('o1', 'o3'), ('o3', 'o1')}
4: 	o1 -> o2, 	o2 <- o3, 	o3 -> o1: 
	P: {('o2', 'o1'), ('o2', 'o3'), ('o1', 'o3')}, 
	R: {('o3', 'o1'), ('o1', 'o2'), ('o3', 'o2')}, 
	I: set(), 
	J: set()
5: 	o1 -> o2, 	o2 <- o3, 	o3 <- o1: 
	P: {('o2', 'o1'), ('o2', 'o3'), ('o3', 'o1')}, 
	R: {('o1', 'o3'), ('o1', 'o2'), ('o3', 'o2')}, 
	I: set(), 
	J: set()
6: 	o1 -> o2, 	o2 <- o3, 	o3 || o1: 
	P: {('o2', 'o1'), ('o2', 'o3')}, 
	R: {('o1', 'o2'), ('o3', 'o2')}, 
	I: set(), 
	J: {('o1', 'o3'), ('o3', 'o1')}
7: 	o1 -> o2, 	o2 || o3, 	o3 -> o1: 
	P: {('o2', 'o1'), ('o1', 'o3')[...]<jupyter_text>Next, we reject cases represeting inconsistent preferences.<jupyter_code>import networkx as nx

consistent_cases = []
for case in cases: 
    FLAG_no_loops = True
    FLAG_transitivity = True
    
    # Get strict preference set
    P = case[1]
    
    # Create a graph to identify cycles
    G = nx.DiGraph()
    G.add_nodes_from(["o1", "o2", "o3"])
    G.add_edges_from(P)
    if len(list(nx.simple_cycles(G))) > 0:
        FLAG_no_loops = False
    
    # Check transitivity (TODO)
    for (oi, oj), (ok, ol) in product(P, P):
        if oj == ok and not (oi, ol) in P:
            FLAG_transitivity = False
    
    if FLAG_no_loops and FLAG_transitivity:
        consistent_cases.append(case)
            

print(f"consistent cases: {len(consistent_cases)} out of {len(cases)}")
for case in consistent_cases:
    print(f"{case[0]}: \n\tP: {case[1]}, \n\tR: {case[2]}, \n\tI: {case[3]}, \n\tJ: {case[4]}")<jupyter_output>consistent cases: 19 out of 27
2: 	o1 -> o2, 	o2 -> o3, 	o3 <- o1: 
	P: {('o2', 'o1'), ('o3', 'o1'), ('o3', 'o2')}, 
	R: {('o2', 'o3'), ('o1', 'o2'), ('o1', 'o3')}, 
	I: set(), 
	J: set()
4: 	o1 -> o2, 	o2 <- o3, 	o3 -> o1: 
	P: {('o2', 'o1'), ('o2', 'o3'), ('o1', 'o3')}, 
	R: {('o3', 'o1'), ('o1', 'o2'), ('o3', 'o2')}, 
	I: set(), 
	J: set()
5: 	o1 -> o2, 	o2 <- o3, 	o3 <- o1: 
	P: {('o2', 'o1'), ('o2', 'o3'), ('o3', 'o1')}, 
	R: {('o1', 'o3'), ('o1', 'o2'), ('o3', 'o2')}, 
	I: set(), 
	J: set()
6: 	o1 -> o2, 	o2 <- o3, 	o3 || o1: 
	P: {('o2', 'o1'), ('o2', 'o3')}, 
	R: {('o1', 'o2'), ('o3', 'o2')}, 
	I: set(), 
	J: {('o1', 'o3'), ('o3', 'o1')}
8: 	o1 -> o2, 	o2 || o3, 	o3 <- o1: 
	P: {('o2', 'o1'), ('o3', 'o1')}, 
	R: {('o1', 'o3'), ('o1', 'o2')}, 
	I: set(), 
	J: {('o2', 'o3'), ('o3', 'o2')}
9: 	o1 -> o2, 	o2 || o3, 	o3 || o1: 
	P: {('o2', 'o1')}, 
	R: {('o1', 'o2')}, 
	I: set(), 
	J: {('o3', 'o1'), ('o2', 'o3'), ('o1', 'o3'), ('o3', 'o2')}
10: 	o1 <- o2, 	o2 -> o3, 	o3 -> o1: 
	P: [...]<jupyter_text>Since we have two fixed words, we consider two equivalence classes of final states. First one is the set of final states in $F_1 \times F_2 \times (Q_3 \setminus F_3)$ and the other set is final states in  $(Q_1 \setminus F_1) \times (Q_2 \setminus F_2) \times F_3$.<jupyter_code>def label(case):
    q1_label = set()
    q2_label = set()
    
    P = case[1]
    
    # Determine most-preferred outcome in q1.
    mp_outcome = set()
    if ("o1", "o2") in P:
        mp_outcome = {"o1"}
    
    elif ("o2", "o1") in P:
        mp_outcome = {"o2"}
    
    else:
        mp_outcome = {"o1", "o2"}
    
    # Most-preferred outcome in q2 is always o3.
    mp_outcome.add("o3")
    
    
    # Generate label by comparing MP outcomes
    for (oi, oj) in P:
        if oi not in mp_outcome or oj not in mp_outcome:
            continue
        
        if oi in ["o1", "o2"]:
            q1_label.add(f"x_{oi[1]}{oj[1]}")
        
        if oi in ["o3"]:
            q2_label.add(f"x_{oi[1]}{oj[1]}")
        
        if oj in ["o1", "o2"] and oi not in ["o1", "o2"]:
            q1_label.add(f"y_{oi[1]}{oj[1]}")
        
        if oj in ["o3"]:
            q2_label.add(f"y_{oi[1]}{oj[1]}")
    
    return q1_label, q2_label

labeled_cases = []
for case in consistent_cases: 
    q1_label, q2_label = label(case)
    n_case = case + (q1_label, q2_label)
    labeled_cases.append(n_case)

for case in labeled_cases:
    print(f"{case[0]}: \n\n\tP: {case[1]}, \n\tR: {case[2]}, \n\tI: {case[3]}, \n\tJ: {case[4]},"
          f" \n\tq1_label: {case[5]}, \n\tq2_label: {case[6]}")
    print()
def relation(case):
    q1_label, q2_label = case[5:]
    
    q1_x = [lbl for lbl in q1_label if "x" in lbl]
    q1_y = [lbl for lbl in q1_label if "y" in lbl]
    q2_x = [lbl for lbl in q2_label if "x" in lbl]
    q2_y = [lbl for lbl in q2_label if "y" in lbl]
    
    # is q1 > q2?
    q1_P_q2 = False
    for lbl in q1_x:
        if lbl.replace("x", "y") in q2_y:
            q1_P_q2 = True
    
    # is q2 > q1?
    q2_P_q1 = False
    for lbl in q2_x:
        if lbl.replace("x", "y") in q1_y:
            q2_P_q1 = True
    
    if q1_P_q2 and not q2_P_q1:
        return "q1 > q2"
    elif not q1_P_q2 and q2_P_q1:
        return "q1 < q2"
    else:
        return "q1 || q2"
eval_cases = []
for case in labeled_cases: 
    res = relation(case)
    n_case = case + (res,)
    eval_cases.append(n_case)

for case in eval_cases:
    print(f"{case[0]}: \n\n\tP: {case[1]}, \n\tR: {case[2]}, \n\tI: {case[3]}, \n\tJ: {case[4]},"
          f" \n\tq1_label: {case[5]}, \n\tq2_label: {case[6]}, \n\trelation: {case[7]}")
    print()<jupyter_output>2: 	o1 -> o2, 	o2 -> o3, 	o3 <- o1: 

	P: {('o2', 'o1'), ('o3', 'o1'), ('o3', 'o2')}, 
	R: {('o2', 'o3'), ('o1', 'o2'), ('o1', 'o3')}, 
	I: set(), 
	J: set(), 
	q1_label: {'y_32'}, 
	q2_label: {'x_32'}, 
	relation: q1 < q2

4: 	o1 -> o2, 	o2 <- o3, 	o3 -> o1: 

	P: {('o2', 'o1'), ('o2', 'o3'), ('o1', 'o3')}, 
	R: {('o3', 'o1'), ('o1', 'o2'), ('o3', 'o2')}, 
	I: set(), 
	J: set(), 
	q1_label: {'x_23'}, 
	q2_label: {'y_23'}, 
	relation: q1 > q2

5: 	o1 -> o2, 	o2 <- o3, 	o3 <- o1: 

	P: {('o2', 'o1'), ('o2', 'o3'), ('o3', 'o1')}, 
	R: {('o1', 'o3'), ('o1', 'o2'), ('o3', 'o2')}, 
	I: set(), 
	J: set(), 
	q1_label: {'x_23'}, 
	q2_label: {'y_23'}, 
	relation: q1 > q2

6: 	o1 -> o2, 	o2 <- o3, 	o3 || o1: 

	P: {('o2', 'o1'), ('o2', 'o3')}, 
	R: {('o1', 'o2'), ('o3', 'o2')}, 
	I: set(), 
	J: {('o1', 'o3'), ('o3', 'o1')}, 
	q1_label: {'x_23'}, 
	q2_label: {'y_23'}, 
	relation: q1 > q2

8: 	o1 -> o2, 	o2 || o3, 	o3 <- o1: 

	P: {('o2', 'o1'), ('o3', 'o1')}, 
	R: {('o1', 'o3'), ('o1', 'o2')}, 
	[...]
{'fraction_non_alphanumeric': 0.2686154908505006, 'fraction_numerical': 0.06951317758084935, 'mean_word_length': 2.4941696823482107, 'pattern_counts': {'":': 9, '<': 34, '<?xml version=': 0, '>': 51, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '3', 'dir': 'jupyter-structured-clean-dedup', 'id': '518104', 'license': 'BSD-3-Clause', 'n_tokens_mistral': 4454, 'n_tokens_neox': 4279, 'n_words': 1081, 'path': 'jp-notebooks/lcss-semantics2.ipynb', 'repo_name': 'abhibp1993/preference-planning', 'size': '8689'}