Messages

 

This page contains selected messages communicated via the course mailing list: sv032_list. If you did not get any messages from this list, your account is not included - please ask Ilana Gottlieb to include your account.

 


Sent: Friday, May 09, 2003 12:05

Hi,

> -----Original Message-----
> From: assayag eldad
> Sent: Friday, May 09, 2003 02:32
> To: Barak Naveh
> Subject: sv032 ex4: variable-indexes
>
> Hello Barak,
> Thanks for all your previous answers, they were really helpful.

You're welcome.

> I 3 questions about the variable-indexes:
> 1. Can I assume that a given Robdd that is passed to a function always
> has its variable-indexes starting with 1 and incremented by 1 in each
> descending of a level?
> (because the algorithm of 'apply' is using this feature).

The indexes are incremented as a result of the variable ordering. In this
implementation we don't change ordering, so i<j implies the ordering Xi<Xj.
However, j-i may not be 1, it would be wrong to assume that.

> 2. Do I need to maintain the feature mentioned in my question#1 when i
> return
> an robdd as result in 'restrict' and 'apply'?
> (because if yes - then there should be a massive update of variable-
> indexes
> in the end of these operations)

The robdd has to maintain the order of the variables. However, take another
look at restrict and apply - it comes "for free". No special action
required.

> 3. Nodes 0,1 are taken as the [maximum variable index] 1.
> Do 'restrict' and 'apply' have to support a case in which the highest
> variable index is disappeared from the expression because of
> simplifying it?
> (support means here to update the variable-index of nodes 0,1 to the
> new max 1).

It's up to your implementation.
Nodes '0' and '1' do not "really" have variable index. They were
artificially added for convenience. If your implementation does not make use
of them, there is of course no point in updating them at all (you can set
them to -1 to ease debugging). On the other hand, if your implementation do
make use of them, you must update them so that resulting robdds will be
valid for further operations, like new robdds.

> And Another question about the .bsh file(s) to submit:
> 4. Do I have to submit my own 'bsh' file with further operations in it,
> or can I submit your one without change?
> What .bsh files exactly do I need to submit?
> (because anyway you'll have *your* new set of checks when you come to
> check
> this assignment).

You can submit one .bsh file that includes all tests.
You can use mine as a starting point, but you would have to add more
invocations, to show all required ROBDD Operations are working.

If you using BeanShell during at your work, it does not require any
additional work on your side. You anyway need to test your stuff, and
BeanShell is probably the easiest way of doing so. Just accumulate these
tests into the .bsh file, and submit it when you're done.

> Thank you in advance,
> Eldad.

All the best,
Barak


Sent: Thursday, May 08, 2003 19:46

Hi,

> -----Original Message-----
> From: assayag eldad
> Sent: Thursday, May 08, 2003 17:43
> To: Barak Naveh
> Subject: sv032 ex4: basic robdd
>
> Hello Barak,
>
> I have 2 questions about your play.bsh file:
> 1. The following 2 variables of type BooleanExpression:
> -----------------------------------------------------------------------
> -
> and2 = parser.parse("and( or( x1, x12), 0)"); --> was simplified to
> "0"
> or3 = parser.parse("or( or( x1, x2), 1)"); --> was simplified to "1"
> -----------------------------------------------------------------------
> -
> Do I have to simplify parsed expressions?
> Because in my program, BooleanExpressions are parsed only after
> performing
> an operation on them (such as: apply , restrict), and its seems like
> your
> program expects them to be simplified when building them.


Parser.parse should return parsed expression, but the returned expression
does not have to be simplified.

Calls to BooleanExpressions.assign must eliminate unnecessary *constants*,
but doesn't have to eliminate unnecessary *variables*.


> 2. The following robdds:
> ---------------------------------
> assert(const0bdd.nodeCount(), 1);
> assert(const1bdd.nodeCount(), 1);
> assert(and2bdd.nodeCount(), 1);
> assert(or3bdd.nodeCount(), 1);
> ---------------------------------
> It looks like you assume that an robdd of a constant has only 1 node,
> which is the constant itself. But I thought that every robdd contains
> the two constants "0" and "1" automatically, because that's what we saw
> in the lesson. It will be problematic for a program to maintain an
> robdd
> that can have only one of these 2 special nodes, because all the
> functions
> will have to support this special case.
> So do I have to change all the implementation now in order to support
> it?

In our algorithms, we automatically initialized our tables to contain the
"0" and "1" nodes. However, for boolean expression such as, say, "and(1, 1)"
- the correct robdd is "1". This robdd has exactly one node.

If you want, you are free to keep the "0" node in your tables and
structures. But then you would have to make sure nodeCount() method does not
count it when it's not reachable - it's a mistake.

> Thank you in advance,
> Eldad.

All the best,
Barak


Sent: Tuesday, May 06, 2003 12:25

Hi,

> I have 3 questions:
> 1. The 'anySat' Algorithm, appearing in the bddnotes.ps document,
> looks very wierd... maby i don't understand it well, but here is
> what it look like: as long as your 'low' son != 0, keep selecting
> the 'high' son for your path. when your 'low' son == 0, select the
> 'low' son for your path, and make a recursion call on your son
> which will lead to an 'error' message.
> That means, that 'anySat' will return 'true' only if you have a
> straight path of 'high's directly to the node "1".
> I would be glad if you can correct me, since I'm almost sure that
> I got this algorithm wrong somehow.

Let's take another look at the AnySat algorithm:

line 1:
if we are at node 0, obviously there is no satisfying truth assignment.

Line 2:
If we are at node 1, any arbitrary truth assignment is satisfying.

Line 3:
If we are at node u, where low(u)=0, this means that if we take the low path we will hit a dead-end. We avoid it by taking the high path.

Line 4:
We take an arbitrary path and move down towards the leaves (low path in this implementation).

Why it works?
Draw any robdd and pick any random path leading to the 0 node. Once you reached the 0 node, take one step back, to the previous node u in the path (the one just before 0). Note that u must have TWO outgoing edges. Because it's an robdd, you cannot have them both going to 0. Therefore, take the other edge. Either you got to 1 or you are on a path that eventually leads to 1. That's the property that makes the algorithm linear in time.

Note: this algorithm does NOT work on any bdd - it works only on robdd.

>
> 2. Please elaborate about what should be in the readme file.
> In tirgul#6 it's written:
> * a description of the system (why? the interfaces are forming
> a pre-defined structure, which hasn't been change...)
> * how we build (build what? an robdd from a boolean expression?
> from the look of the user, or from the look of the system?)
> * how to run (but I thought that it's already determined by your
> Interpreter class... that the user should just run:
> prompt> java Interpreter <params>
> so what should we write here?)

* description - one paragraph that summarizes the structure of system - a roadmap for an outside observer. Interfaces are too detailed for that. It shows you understood what you were doing.

* build - how to compile + which jdk compliance (should be short).

* run - again, short. what you wrote is just fine + need to specify your .bsh file with run examples.

> 3. It's the first time that I'll use the http submission system (we have
> always submitted by a single unix shell command).
> In case there would be problems with the submission system, to which
> mail can I submit it - to yours? or maybe there's a mail like
> sv032@cs...?

In case of problems you can submit by email, as one compressed .zip file, provided that:

1. YOU SEND IT ONLY *ONCE* !!!
2. FILE SIZE IS UNDER 150kb !!!

> Thank you in advance,
> Eldad.

You're welcome,
Barak


Sent: Tuesday, May 06, 2003 01:48

Dear class,

You probably have a class of graph Node holding values of (i,l,h) triplet.
MK creates such Node instances and put them in a Hashtable (or HashMap). A naive implementation of Node will lead to a weird bug: the hashtable will have many Node instances with the same (i,l,h) triplets(!). How can that be? How can a hashtable map the same key to many different values!?

The answer is that Hashtable class decides the equality of keys by using the equals() method of the keys. In the *default* implementation of equals() - two objects are never equal. Hence, whenever the Hashtable inquires for quality of two naive Node instances, it finds them to be NON-equal, even if they have the same (i,l,h) triplet.

To fix the problem, you need to override the equals method to properly reflect the equality relation. Consequently, hashCode method should be overridden as well.

To avoid a frustrating debugging I recommend a careful reading of the documentation of:

- java.lang.Object.equals()
- java.lang.Object.hashCode()

If you need a working example of how to override them, consider their implementations in class "String":

- java.lang.String.equals()
- java.lang.String.hashCode()


All the best,
Barak


Sent: Sunday, May 04, 2003 16:02

Hi

In short - no. It's not supposed to be that way - it's my design flaw.

In details:

The robdd must be that way, because there is only one robdd representation for every boolean expression. The expression "( or( x1, x12), 0)" equals to "0" and therefore its robdd has only one node. If we generalize, robdd will never have unnecessary variables (with respect to a given order).

As for the boolean expressions, you can eliminate unnecessary variables but you don't have to (according to current design). BooleanExpression.assign demands eliminating unnecessary *constants*, but does NOT require eliminating unnecessary *variables*.

In a better design, the contract of BooleanOperator should have had constructing "compute" methods with BooleanExpressions instead of booleans. If it had, eliminating unnecessary subexpressions would have been a piece of cake, and the design could have demanded it. Unfortunately, it's too late to change interfaces at this stage.

Thanks for the feedback,
Barak



-----Original Message-----
From: Arik Peltz 
Sent: Saturday, May 03, 2003 19:22
To: Barak Naveh
Cc: obsfeld
Subject: ex4 - play.bsh

Hi,
 
According to "play.bsh" you expect RobddImpl constructor
to get an optimized boolean expression:
----------------------------
and2 = parser.parse("and(  or( x1, x12), 0)");
and2bdd = factory.createRobdd(and2);
assert(and2bdd.nodeCount(), 1);
----------------------------
(Otherwise T will be initialized with 2 nodes, that can't be removed according to the algorithm)
 
On the other hand, you expect to keep unnecessary variables:
----------------------------
not2 = parser.parse("not(and(  or( x1, x2), 0))");
assert(not2.findMaxVariableIndex(), 2);
---------------------------
 
 
Is it suppose to be that way ?
Thanks in advance,
Arik and Tal


Sent: Sunday, May 04, 2003 14:37

That's true.

The restrict algorithm in the document is "restricting" a given robdd - it "cuts" unnecessary branches and reuse existing nodes where possible. It therefore leaves "garbage" in the form of unlinked nodes (in the tables).

In our implementation the robdd is an immutable object, therefore the restrict method does not change its own object - it constructs a new one.
The algorithm should be slightly modified.

Depending on your implementation, you can make references to nodes in the original robdd (assuming you have immutable node objects). It makes an elegant use of the immutability property. Alternatively, you can duplicate necessary nodes (less elegant).

All the best,
Barak


> Hi,
>
> Looking at the restrict algorithm in the document you've supplied in your
> link, I see a problem.
>
> New nodes are created only when var(u) == j (by a call to mk)
> Thus, existing nodes in the original robdd are not included in the
> new robdd, and the new robdd includes only nodes 0,1 and those created
> by mk.
>
> How do I include the exising nodes in the new robdd ?
>
> Best,
> Tal Obsfeld
>


Sent: Tuesday, April 29, 2003 20:54

> Hi,
>
> 1.
> In the pseudo code of apply() there is a call to app(u1,u2).
> In app function there is a call to var(u1).
> As far as we see, this must return the var index of the node u1 in T, but
> we don't have an access to T (there is no access method in your
> interface of Robdd).

One way of doing it is to put T as a member variable in the class that implements the Robdd interface. When a method receives the argument r, it assumes it's of the same implementation and casts it to the implementing class. Example:

public class RobddImpl implements Robdd {
    ...
    private <some-type> m_T;
    ...
    public Robdd apply(Robdd r, BooleanOperator op) {
        RobddImpl ri = (RobddImpl) r;

        // now we have r's m_T visible in ri.m_T
        ...
    }
    ...
}

This assumption allows us to keep the interface simple and generic. The penalty - we do not support concurrent interoperability between different implementations. Not a terrible loss.

> 2.
> We assume that G is of size this.nodeCount() X robdd.nodeCount(). Is that
> true ?

Perfectly true.

> Thanks in advance,
> Tal and Arik

you're welcome,
Barak


Sent: Tuesday, April 29, 2003 20:22

You can think of G(i,j) as a "cache" of results already computed by APP(i,j). Since results are already computed, no need to do any further check - only to look them up.

Another thing, when processing apply for two robdds (r, s) and operator (op1), all recursive invocations of APP(i,j) are relating to the same op1.
i and j will get different node-id values, as the recursion progresses down from the roots (r,s) towards the leaves.

It's true, however, that G has to be initialized ("invalidated" in cache terms) before invoking APP(r,s).

Hope it answers your question,
Barak


> -----Original Message-----
> From: zack shaul [mailto:zacksh]
> Sent: Tuesday, April 29, 2003 15:57
> To: Barak Naveh
> Subject: Apply algorithm and G data structure
>
>
> How came when checking if G contains an earlier computed result of
> APP(i,j) it does not taking into account the type of the BooleanOperator?
>
> Why G doesn't "check" for which BooleanOperator it computed the last
> result and only if the BooleanOperator is the same as this time it return
> G(u1,u2).
>
> Thanks Shaul
>


Sent: Tuesday, April 29, 2003 20:00

No no - neither one, note that assignment of false to variable x5 has no effect on variable x10. We get:

x10 [ false / x5 ] = x10

Therefore, in such cases assign should return the original value (unchanged).


-----Original Message-----
From: Yuval Klein [mailto:kleiny]
Sent: Tuesday, April 29, 2003 13:10
To: Barak Naveh
Subject: robdd

Hi Barak, I have a question about the ROBDD assignment:
In the bsl example you wrote:
    var10 = parser.parse(" x10 ");
    var10ass = var10.assign(5,false);
var10 has no var with index 5! is this a mistake or should I return an error msg?
 
best
Uv


Sent: Tuesday, April 01, 2003 18:10

Dear class,

In the tirgul of this week I'll present the Java assignment (ex #4). It is recommended you briefly read it before class and prepare questions. The algorithmic material required for the exercise will be studied on next week's lecture + tirgul.

All the best,
Barak


Sent: Wednesday, March 26, 2003 14:34

Hi Chen,

> In the interest of saving time and understanding. We have proven in class
that adding a node to a sufficient cut point as in this case and using
backward or forward propgating assertion will promise to keep partial
correctness. And so I wonder what else is there to prove, can I use the
general claim proven in class (pages 35-40) for Q1.
> All the best
> Chen
>

Indeed, we proved the general case in class, so obviously the correctness of
each special case follows.

The purpose of the question is to give you the "hand on" feel and intuition.

What you say is correct, if you use the claim proven in class - there is
nothing prove.

However, doing so will defeat the purpose of the question - therefore you
should not use it.

Barak


Sent: Tuesday, March 25, 2003 22:46

Hi Arik,

>
> In the third part of question 1, we need to prove partial correctness on
> the network {L0, L3, L2}.
> Therefore, we need to prove VC03, VC33, VC32, VC32'.
> I assume we can use the assertions from the first and the second part of
> the question.
>
> My question is: can we prove the last part according to the previous
> proofs ?
> For example, in order to prove VC03, we can use the previous proofs of
> VC01 and VC13,
> and the previous assertion of L1 (that is not an assertion in this case)
> helps us in the middle (like "Ta'anat Ezer").
>
> Best,
> Arik Peltz

I'm not sure I understand your question, so I clarify again: You can salvage any claim from previous exercise, and "reuse" it by quoting it as a "proven lemma". However, do it only if:

a) It really saves you time.
b) You actually DID prove it (correctly) in previous exercise.
c) I can easily understand your references.

All the best,

Barak


Sent: Sunday, March 23, 2003 11:40

Hello,

Solution for assignment 1 is now available on my page: http://www.cs.bgu.ac.il/~barnav/teaching/verification03b.

You are encouraged to compare it to your solution. If you made mistakes it will help you to avoid them on next assignments.

If I made mistakes, please let me know. A bonus of 5 points will be credited on the assignment of the first student who informs me on any principal mistake in my solutions.

All the best,

Barak


Sent: Wednesday, March 19, 2003 12:58

Please note,

In your partial correctness proof, you do NOT need to prove that array accesses are non-faulty.

This means your partial correctness proof will NOT ensure that array-index-out-of-range never happens. That part is completed in assignment 2 (q2).

Barak


Sent: Sunday, March 16, 2003 21:43

Hello Boris,

> Can I submit our first assignment some other way (instead of hand-in in
> class).
> It is Purim week and I work all this week in Herzlia.
> I can send you the assignment by mail and next week I'll bring you
> its hard copy.

1. The BEST submission method is to bring it to class. Try to get the help of a friend that do come to class. Fax or email a scan to him/her, and ask them to hand-in the printout.

If 1 is not possible:

2. You can SCAN the assignment and email me the file:
a) Compress it and try to keep the file under 0.5MB.
b) Print the scanned version and make sure the paper version is readable.
c) Send it only ONCE.
d) I recommend sending me a "test-page" to verify file opens properly.
e) You would have to submit by Wednesday, before midnight.

3. As last (and strongly discouraged) resort, I might be able to receive a fax:
a) Please contact me to coordinate transmission.
b) You would have to finish submission by Wednesday, before midnight.

If you use 2 or 3, you don't need to submit the hard-copy.

Best regards,
Barak