for loop analysis is broken

[nkrusch]

During analysis of a for loop, the implementation call a non-existent method rels.conditionRel.

This was, at some point, a method of RelationList class, but going back as far as old_dfg_mwp_python I have not found the implementation.

Trying to resolve this:

1. what does this method do?
2. (independent of previous) is it necessary to call this method?

Current implementation with added comments:

        # create empty relation list
        rels = RelationList([])

        # recursively analyze children of current AST node, update index value
        for child in node.stmt.block_items:
            index, rel_list = compute_rel(index, child)

            # add to relation list (will resize matrix as needed)
            rels = rels.composition(rel_list)

        # run fixpoint    
        rels = rels.fixpoint()

        # ?????
        rels = rels.conditionRel(list_var(node.cond))

        # return updated index, relation list
        return index, rels

(actual source without comments)

list_var extends c_ast.NodeVisitor and returns node names, implementation: [1], [2]

[seiller]

I believe this is were some additional treatment for the loop is required. Basically in all analyses one computes the matrix/relation of the body, then compute a fixed point. But the matrix for the loop itself is not just this fixed point, as there is usually a specific operation to perform to take care of the loop condition. This is what the missing method should do. (But since there are two types of loops with different operations to perform in the mwp case, in the end we will end up with two different methods I guess.)

On 1 May 2021, at 04:00, Neea Rusch @.***> wrote:

 During analysis of a for loop, the implementation call a non-existent method rels.conditionRel.

This was, at some point, a method of RelationList class, but going back as far as old_dfg_mwp_python I have not found the implementation.

Trying to resolve this:

what does this method do? (independent of previous) is it necessary to call this method? Current implementation with added comments:

    # create empty relation list
    rels = RelationList([])

    # recursively analyze children of current AST node, update index value
    for child in node.stmt.block_items:
        index, rel_list = compute_rel(index, child)

        # add to relation list (will resize matrix as needed)
        rels = rels.composition(rel_list)

    # run fixpoint    
    rels = rels.fixpoint()

    # ?????
    rels = rels.conditionRel(list_var(node.cond))

    # return updated index, relation list
    return index, rels

(actual source without comments)

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or unsubscribe.

[aubertc]

Some more tests with for loops:

• We need to have a condition enforcing that the variables in the header do not occur in the body of the loop (the value is not "fixed", cf. https://github.com/seiller/pymwp/blob/master/c_files/for_body.c ).
• If this is the case, then we should be able to analyze small programs such as the one at https://github.com/seiller/pymwp/blob/master/c_files/for_body.c

As of now, the analysis for that file yields

y    |     +m+w.delta(0,0)+p.delta(2,0)  +o
x    |     +o+w.delta(0,0)+p.delta(1,0)+p.delta(2,0)  +m

but hand calculation shows that we should get:

['  +m+w.delta(0,0)+m.delta(1,0)+p.delta(2,0)', '  +o']
['  +o+w.delta(0,0)+p.delta(1,0)+p.delta(2,0)', '  +m']

(There is a +m.delta(1,0) that diverges between the two).

You can experiment with the following "helper" (put it in /pymwp and run with python composition_example4.py

from pymwp import Polynomial, Monomial
from pymwp.matrix import identity_matrix, matrix_prod, matrix_sum, fixpoint, equals, show

l1=identity_matrix(2)
l1[0][0] = Polynomial([Monomial('w', [(0, 0)]), Monomial('m', [(1, 0)]), Monomial('p', [(2, 0)])])
l1[1][0] = Polynomial([Monomial('w', [(0, 0)]), Monomial('p', [(1, 0)]), Monomial('m', [(2, 0)])])

show(l1, prefix="[   y ,    x ]")

show(fixpoint(l1), prefix="[   y ,    x ]")

The l1 matrix was obtained by running the analysis on the body of the loop (and checking it by hand).