HTTPS SSH

README

Authors

  • Anja Petković
  • mentor: dr. Alex Simpson

Contents

Implementation of direct algorithm for evaluating μ-terms in Lukasiewicz μ-calculus. Main reference: M. Mio, A. Simpson: Lukasiewicz μ-calculus, arXiv:1510.00797 [cs.LO]

  • muTerms.py - contains class definitions for μ-terms representation
  • evaluating_algorithm.py - contains necessary functions and implemented algorithm (basic and optimized version)
  • examples.py - script that shows basic examples
  • random_example_generator.py - contains function to generate random μ-terms (appropriate for testing)
  • test.py - script for testing performance and executing code
  • problematic_examples.py - contains some problematic examples that demonstrate problems with algorithm
  • unit_tests.py - contains unit tests for μ-terms and evaluating algorithm functions (not finished)
  • sharedModule.py - contains global variables for testing performance of the evaluating algorithm
  • quantifierElimination.py - contains functions for quantifier elimination used for optimizing the constraint sets in evaluating algorithm
  • graphs.py - script that reads pefrormance results and draws graphs using matplotlib library (numpy and matplotlib modules needed)

Get started

  • run python 3 shell
  • run command:
from examples import *
  • see results for basic examples

Run tests

You may want to run the tests to make sure the code is working properly. Insert the following code into your command prompt to see which tests go through:

python3 unit_tests.py -v

Short guide

μ-terms are generated using the muTerm class. A muTerm has a simple tree structure with attributes operator, subterm1, subterm2, value, name. Value is only relevant for constants and rational multiplication, whereas name is only relevant for variables and operators μ and ν. The default value for unnecessary attributes is None. To construct a term ν y.((μ x.(x ⊕ 1))⊙( 1/2 ∏(y∐0))) we need to write

testTerm = muTerm('nu', muTerm('.',muTerm('mu',muTerm('+',muTerm('var',None,None,None,'x'),muTerm('1',None)),None,None,'x'),
    muTerm('m',muTerm('r',muTerm('1',None),None,0.5),muTerm('M',muTerm('var',None,None,None,'y'),muTerm('0',None)))),None,None,'y')

Because we want a cannonical variable names, we run the function

testTerm.rename_variables()

This names the variables by indeces var(i). We have a pretty print function to see what term we inputed

>>> print(testTerm)
ν var(1).((μ var(2).((var(2))(1)))((0.5(1))((var(1))(0))))

To evaluate the terms we run the function evaluate and give a list of values as the second argument. Closed terms are evaluated with empty list.

result = evaluate(testTerm,[])
result1 = evaluate_optimized(testTerm,[])

A conditioned linear expression is returned as a tuple of list of inequalities and a linear expression. Inequalities are a tuple (sign, expression1, expression2), where sign is one of "<", ">", ">=", "<=" and denotes the relation between expressions i.e. if sign is "<", this means expression1 < expression2. Linear expressions are lists of numbers (either fractions or floats) [q0,q1,q2,...] and they are interpreted as q0 + q1 x1 + q2 x2 + ...

Because this is hard to read, we have pretty print functions to help us understand what is going on. Print fuctions convert conditioned linear expressions in the form {inequalities} ⊢ linear expression.

>>> print(conditioned_linear_expression_to_string(result[0],result[1]))
{ 0 + 1x_1 <= 1, 0 + 1x_1 >= 0, 0 + 1x_1 >= 0, 0.5 <= 0 + 1x_1 }   0.5

Sometimes we want to generate a random closed term with a certain number of μs and νs.

from random_example_generator import *
#generate a random term with 2 μs and 1 ν.
t = generate_random_muTerm(2,1)

There is also an optimized version of evaluating algorithm, that (using quantifier elimination) shrinks the constraint sets to the absolutely necessary constraints.

result1 = evaluate_optimized(testTerm,[])

To test the performance of both versions of algorithm use test.py module and functions performance_test and run_performance_test.

# test the performance of algorithm evaluate on terms with 2 nu's and 2 mu's on 100 different examples. 
# Write the results in performance.txt file
performance_results = performance_test(100, 2, 2, 'performance.txt', evaluate)

# test the performance of algorithm evaluate_optimized on terms with 2 nu's and 2 mu's on 100 different examples. 
# Write the results in performance_optimized.txt file
performance_results_optimized = performance_test(100, 2, 2, 'performance_optimized.txt', evaluate_optimized)

# run the performance tests on terms with up to 10 fixed points for algorithm evaluate
performance_results_all = run_performance_tests(100, 10,'performance.txt', evaluate)

To analyze the performance, draw graphs (graphs.py module) that show the performance (on the logarithmic scale). You need matplotlib and numpy modules to run this part of the code

draw_performance_graphs()