Issue 6: PLURAL: Warn user that they need frame permission to change state
Status:  Accepted
Owner: ----
Project Member Reported by nels.bec...@gmail.com, Aug 28, 2008
1. Run PLURAL on the attached file

This file should have no errors, right? Or is it nonsense to try to pack a
shared object to some state? Even if I insert the following line:
@ClassStates({@State(name="OPEN")})

Which I think would reinforce the fact that there are no state invariants
for the state OPEN.
 
AtomicShare.java
550 bytes   View   Download
Aug 29, 2008
Project Member #1 kevin.bi...@gmail.com
This is expected behavior, and it's (I think) unrelated to whether OPEN has an
invariant or not.  Plural issues a warning in isOpen() b/c it cannot *un*pack b/c
there is no frame permission.  Specifying isOpen() with @Share(fieldAccess = true)
removes the error.  

    @Share(fieldAccess = true)
    @TrueIndicates("OPEN")
    boolean isOpen() { return true; }

(Another problem can be that OPEN is not declared as a state is therefore sometimes
not tried when packing.  That shouldn't be an issue here, but it can become a problem.)

I fell for this before as well; maybe there is some better error that we can report?
 The other question is whether unpacking and packing should be necessary for states
without invariants.
Status: Accepted
Aug 29, 2008
Project Member #2 nels.bec...@gmail.com
Okay, I can confirm that adding "fieldAccess = true" to the share permission makes
the error go away. I am going to change this issue to a low-priority feature request:
It would be nice if there was a different warning for this simple problem, and it
seems like the sort of thing a tree-walker could find.
Summary: PLURAL: Warn user that they need frame permission to change state
Labels: -Type-Defect -Priority-Medium Type-Enhancement Priority-Low
Sep 7, 2008
Project Member #3 nels.bec...@gmail.com
Uh oh...

I just tried this again, and I am getting the same problem, even with the 
"fieldAccess = true" line. Here's the code:

{{{
public class SimpleShareNoAtomic {
	@Share(fieldAccess = true)
	@TrueIndicates("OPEN")
	boolean isOpen() { return true; }
	
	@Share(requires="OPEN") void needsOpen() { }
	
	void foo(@Share SimpleShareAtomic a_s) {
		if( a_s.isOpen() )
			a_s.needsOpen(); // Error! 
	}
}
}}}

And on the isOpen method, I get the warning, "Could not bring the receiver into post-
condition states [OPEN] due to insufficient field permissions." Did something change?
Labels: -Type-Enhancement Type-Defect
Sep 8, 2008
Project Member #4 nels.bec...@gmail.com
Okay, I think this is just a NIMBY problem. No  big surprise there.
Labels: -Type-Defect Type-Enhancement