#3 Universe extension isn't applied inside seqblock

[Daniel A. Sadilek]

I'm not sure if this is a bug. At least it does not behave as I would expect:

I extend a universe inside a seqblock. I would expect that the statements following this extension could work with the extended universe. Instead, the universe is not updated until the next ASM step.

Take the following program as an example. I would expect that it prints out:
Added Element33727
[InitRule] Place Element33727
[Next] Place Element33727

But it prints out:
Added Element33727
[Next] Place Element33727

------------------------
CoreASM Minimal

use Standard

universe Places

init InitRule

rule InitRule =
seqblock
extend Places with newPlace do par
print "Added " + newPlace
endpar

forall p in Places do
print "[InitRule] Place " + p

program(self) := @Next
endseqblock

rule Next =
forall p in Places do
print "[Next] Place " + p
------------------------

Am I wrong, or the implementation?

Best regards
Daniel Sadilek

CoreASM is version 0.4.5.

[Roozbeh Farahbod]

Logged In: YES
user_id=673608
Originator: NO

You are right Daniel. There is an implementation bug regarding universes in sequential blocks. The source of the problem is a combination of two things:

1) Application of sequential updates to state are implemented by a stack of updates; every sequential step adds one layer of updates to the stack. To lookup a value, the stack is traversed from top to bottom, so the most recent value of a function is returned. As a result, the actual state is not changed until the machine completes the step and merges the stack into the state.

2) To allow parallel incremental updates to universes in a simple fashion (contrary to sets for example), universes are viewed as their set-characteristic functions that also implement Enumerable interface.

Now, the problem is that when a new element E is added to a universe U in a sequential update, an update of the form U(E) := true is added to the stack, but the value of the universe element U is not changed. So, when U is viewed as an enumerable, U returns its original list of elements not including the new one. To give you the idea, this does not happen for sets as when a set S is updated, the aggregation method of the Set plugin gathers all the incremental updates and generates a single update to S that updates its value with a completely new element that has the recent changes. So, the changes to sets show up in the next seq step. Do you see the difference?

Universes are special in ASM and I didn't want to change the CoreASM element that is bound to a universe name during a run, so that if there are references to that value in the machine (e.g., as the value of some other functions), they stay valid while the universe grows or shrinks.

I still have to find a good and clean solution for this problem. Let me know if you have any idea.

BTW, have a look at the CoreASM wiki and specially this page:

http://scarlatti.cs.sfu.ca/coreasm-wiki/index.php/CoreASM-v1.1

I have already listed this bug at the bottom of the page. Feel free to create an account and update the todo list (or other pages).

Thanks.

[Daniel A. Sadilek]

Logged In: YES
user_id=747110
Originator: YES

Sorry, I don't understand why universes have to be treated so differently from sets? I am (of course) not that deep in the implementation. But both UniverseElement and SetElement have FunctionElement in their inheritance hierachy and I would expect that the same aggregation logic that is applied to sets could be applied to universes!?

I don't understand what you meant with this:
"Universes are special in ASM and I didn't want to change the CoreASM
element that is bound to a universe name during a run, so that if there are
references to that value in the machine (e.g., as the value of some other
functions), they stay valid while the universe grows or shrinks."
Is it just a technical problem or is it a conceptual problem?

Daniel

[Roozbeh Farahbod]

Set Example

[Roozbeh Farahbod]

Logged In: YES
user_id=673608
Originator: NO

This is not much an implementation issue. Universe is a fundamental concept in ASM. They are the categories of values in the ASM state.
So, we tried to formulate and implemented them in as simple as possible, before even introducing the Set background (the Set type).
The Set background is not in the CoreASM kernel and it is introduced as an extension by the Set Plugin.

Now, we still can treat the universes the same as sets, however that seems like a dirty solution to me. If we decide to do so, we shouldn't be relying
on the Set plugin; the treatment should be implement in the kernel.

> I don't understand what you meant with this:
> "Universes are special in ASM and I didn't want to change the CoreASM
> element that is bound to a universe name during a run, so that if there
> are
> references to that value in the machine (e.g., as the value of some other
> functions), they stay valid while the universe grows or shrinks."
> Is it just a technical problem or is it a conceptual problem?

To be consistent with the basic concepts of ASM, a set element is not modifiable; i.e., if you update a set element,
you will get a new set element. Let me give you an example (see also the attached file):

rule MainProgram =
if ctl_state = 0 then
a := {1, 2, 3}

if ctl_state = 1 then
b := a

if ctl_state = 2 then
add 5 to a

if ctl_state = 3 then
print "a is " + a + ", b is " + b
program(self) := undef

ctl_state := ctl_state + 1

The ASM program above (assuming that ctl_state is 0 in the initial state), prints the following:

a is {3, 5, 1, 2}, b is {3, 1, 2}

a gets the set element {1,2,3} and b also gets the same value. Now, updating a by adding 5 to the set does not change the original set but it creates a new set with the additional member 5. As a result, b holds the original value while a holds a new value. I don't think that it is a good idea to treat universes the same way. Let's say some part of your system keeps a reference to universe U. What happens that if you update U, that reference is now pointing to an outdated value.

Of course, the bug you mentioned has to be fixed, but my point is that the solution is not just to treat them as sets.

Let me know if I am still not clear.

File Added: SetExample.coreasm

[Roozbeh Farahbod]

Logged In: YES
user_id=673608
Originator: NO

I submitted the text in a hasty manner. Excuse my English! ;-)

[Daniel A. Sadilek]

Logged In: YES
user_id=747110
Originator: YES

Hi,

thank you for the clarification. What I'm still missing is an example for what you said: that it isn't a good idea to treat universes like sets. When would I want to use a reference to a universe? Are there any example programs in which this is done? I would expect that if this is necessary/helpful for universes, it is also necessary/helpful for sets.

In the default case, assignemnt has "copy value" semantics. Applying this to a universe U when I write "b := U", I would expect b to be just a copy of the universe, i.e., a set containing copies of all elements of the universe U. If it is really necessary to work with references (what I can imagine for both universes and sets), I can imagine two options: working with references explicitly or control the assignment semantics.

(1) Use the special operator @ to get a variable's reference, not it's value. This may look like this:
b := @a and b := @U.
In this case, b would contain a reference to a or U, respectively. The type of b would be "reference of ...". Therefore, an additional dereferncing operator would be necessary, for example "*". The print statement may then look like this:
print "a is " + a + ", b is " + *b
This would print out: "a is {3, 5, 1, 2}, b is {3, 5, 1, 2}".
If I want to change the value of a, I can write both "a := {42}" or "*b := {42}".

(2) The assignment itself could be changeable to "copy reference" semantics. This may look like this:
b &:= a and b &:= U.
Like in the first case, b would contain a reference to a or U, respectively. But b could be used (transparently) everywhere where a (or U) can be used. Thus, no change in the print statement would be necessary.

The first option corresponds to pointers and the second one to references in C++. (With references in C++, it is actually b being a reference type that controls the assignment semantics, not a special assignment operator. But usage is similar, I think.)

Bye
Daniel

[Daniel A. Sadilek]

Logged In: YES
user_id=747110
Originator: YES

Just to clarify:
b := @a would not mean that b holds a reference to {1, 2, 3} but that b holds a reference to a, so working with *b is like working with the original function a. Similarly for the second option with the special assignment operator.

(1)
If a has parameters, it would look like this:
a(x, y) := z
b := @a
*b(x, y) := v
// a(x, y) = v

or like this:
a(x, y) := z
b := @a(x, y) // b points to the function a and has additionally copies of the values x and y to access the defined location
*b := v
// a(x, y) = z

(2)
If a has parameters, it would look like this:
a(x, y) := z
b &:= a
b(x, y) := v
// a(x, y) = v

or like this:
a(x, y) := z
b &:= a(x, y) // b points to the function a and has additionally copies of the values x and y to access the defined location
b := v
// a(x, y) = z

(All these inside seqblocks or in different rules like in your example.)