How to use

How to use

• Propositional Calculus
• First-order Logic
• REf
• Linear Temporal Logic on Finite Traces
• Linear Dynamic Logic on Finite Traces
• Linear Dynamic Logic on Finite Traces for empty traces

Propositional Calculus

Create some formulas:

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()

Using Propositional Calculus:

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

First-Order Logic

TODO

REf

TODO

LTLf

TODO

LDLf

TODO

LDLf_FiniteTraces

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")