Issue 8: Can't get field permissions for unique receiver?
Status:  Fixed
Owner:
Closed:  Sep 2008
Project Member Reported by nels.bec...@gmail.com, Sep 11, 2008
The following program

@States({"OPEN", "CLOSED"})
@ClassStates({@State(name="OPEN", inv="fact == true"), 
	      @State(name="CLOSED", inv="fact == false")})
public class UniqueUnpack {

	private boolean fact = true;

	@Unique(fieldAccess = true, requires="OPEN", ensures="CLOSED")
	void doUnpacking() {
		fact = false;
	}	
}

Should report no errors, as far as I know. Instead, it reports the error, 
"Could not bring receiver into post-condition states [CLOSED] due to 
insufficient field permissions." Replacing @Unique with @Full works just 
fine.
Sep 11, 2008
Project Member #1 nels.bec...@gmail.com
Extra choices for contexts were inadvertently being removed during 
FractionalPermissions.atLeastAsPreciseAs(). Fixed in revision 40.
Status: Fixed