from pythogic.base.Formula import AtomicFormula, TrueFormula, FalseFormula, Not, And, Or # Propositions a = AtomicFormula(a_sym) b = AtomicFormula(b_sym) c = AtomicFormula(c_sym) # Elementary formulas not_a = Not(a) not_a_and_b = And(Not(a), b) not_a_or_c = Or(not_a, c) true = TrueFormula() false = FalseFormula()

from pythogic.pl.PL import PL from pythogic.pl.semantics.PLInterpretation import PLInterpretation # A dictionary which assign each symbol to a truth value symbol2truth = { a_sym: True, b_sym: False, c_sym: True } # The propositional interpretation I = PLInterpretation(alphabet, symbol2truth) # main class which contains useful methods PL = PL(alphabet) PL.truth(a, I) # returns true PL.truth(b, I) # returns false PL.truth(c, I) # returns true PL.truth(not_a, I) # returns false PL.truth(not_a_and_b, I) # returns false PL.truth(not_a_or_c, I) # returns true PL.truth(true, I) # returns true PL.truth(false, I) # returns false

from pythogic.base.Alphabet import Alphabet from pythogic.base.Formula import LogicalTrue, AtomicFormula, Not, And, Or, PathExpressionSequence, \ PathExpressionEventually, PathExpressionTest, TrueFormula, FalseFormula, End, LDLfLast, Next, Until, \ PathExpressionAlways, PathExpressionStar, PathExpressionUnion from pythogic.base.Symbol import Symbol from pythogic.base.utils import print_nfa, print_dfa from pythogic.ldlf_empty_traces.LDLf_EmptyTraces import LDLf_EmptyTraces from pythogic.ltlf.semantics.FiniteTrace import FiniteTrace # Define symbols and the alphabet a_sym = Symbol("a") b_sym = Symbol("b") c_sym = Symbol("c") alphabet_abc = Alphabet({a_sym, b_sym, c_sym}) # Define the formal system instance ldlf = LDLf_EmptyTraces(alphabet_abc) # Define a Finite Trace (i.e. the semantics for LDLf) # first, a list of sets of symbols trace_list = [ {a_sym, b_sym}, {a_sym, c_sym}, {a_sym, b_sym}, {a_sym, c_sym}, {b_sym, c_sym}, ] # the FiniteTrace instance trace = FiniteTrace(trace_list, alphabet_abc) # some formula tt = LogicalTrue() ff = LogicalTrue() TRUE = TrueFormula() FALSE = FalseFormula() a = AtomicFormula(a_sym) b = AtomicFormula(b_sym) c = AtomicFormula(c_sym) END = End() LAST = LDLfLast() seq_aANDb_aANDc = PathExpressionSequence(And(a,b), And(a,c)) union_b_c = PathExpressionUnion(b, c) ev_seq_aANDb_aANDc__not_c = PathExpressionEventually(seq_aANDb_aANDc, Not(c)) ev_aANDb__aANDc = PathExpressionEventually(And(a,b), And(a,c)) ev_test_a__c = PathExpressionEventually(PathExpressionTest(a), c) ev_test_a__b = PathExpressionEventually(PathExpressionTest(a), b) always_true__bORc = PathExpressionAlways(PathExpressionStar(TrueFormula()), Or(b, c)) # Notice: you can use abbreviations (not elementary formulas) next_aANDc = PathExpressionEventually(TrueFormula(), And(a,c)) equiv_next_aANDc = Next(And(a,c)) a_until_bANDc = Until(a, And(b, c)) # evaluate formulas over the trace ldlf.truth(Not(a), trace, 0) #False ldlf.truth(Not(a), trace, 4) #True ldlf.truth(And(a, b), trace, 0) #True ldlf.truth(And(a, b), trace, 1) #False ldlf.truth(Or(a, b), trace, 1) #True ldlf.truth(ev_aANDb__aANDc, trace, 0) #True ldlf.truth(ev_seq_aANDb_aANDc__not_c, trace, 0) #True ldlf.truth(ev_seq_aANDb_aANDc__not_c, trace, 1) #False ldlf.truth(ev_test_a__c, trace, 0) #False ldlf.truth(ev_test_a__b, trace, 0) #True ldlf.truth(next_aANDc, trace, 0) #True ldlf.truth(equiv_next_aANDc, trace, 0) #True ldlf.truth(a_until_bANDc, trace, 0) #True ldlf.truth(always_true__bORc, trace, 0) #True # convert formulas to NFA and print them to a file nfa = ldlf.to_nfa(ev_seq_aANDb_aANDc__not_c) print_nfa(nfa, "NFA_ev_seq_aANDb_aANDc__not_c") print_dfa(nfa, "DFA_ev_seq_aANDb_aANDc__not_c") nfa = ldlf.to_nfa(always_true__bORc) print_nfa(nfa, "NFA_always_true__bORc") print_dfa(nfa, "DFA_always_true__bORc")