Add Enums to refinement language and verification as parameters.

[CatarinaGamboa]

Why?

Enums can be received as parameters and the state changes can depend on the values gotten from the enum parameter.

Example

From an example from modeling flight controllers code with the library mavsdk (gitrepo)

public enum Mode {
	Photo,
	Video,
	Unkown
}

class Camera {
	public void setMode(Mode mode) {...}
	
	public void takePhoto() {...}
}

In this case, the method setMode defines the current mode of the camera. If the value in the parameter is Mode.Photo the transition of the method should be to photoMode in which the method takePhoto() should be allowed. However, if the Mode used is a different one, takePhoto() should not be allowed.

Intended behavior

The idea here is to add enums to the refinements language and their verification as parameters.
Ideally, the piece of code from above should be modeled in the following way:

@StateSet({"photoMode", "videoMode", "noMode"})
class Camera {
	
	@StateRefinement(to="noMode(this)")
	public Camera() {}
	
	
	@StateRefinement(from="noMode(this) && mode == Mode.Photo", to="photoMode(this)")
	@StateRefinement(from="noMode(this) && mode == Mode.Video", to="videoMode(this)")
	public void setMode(Mode mode) {...}
	
	@StateRefinement(from="photoMode(this)")
	public void takePhoto() {...}
	
	
	public static void main(String[] args) {
		// Correct
		Camera st = new Camera();
		st.setMode(Mode.Photo);
		st.takePhoto();

		// Incorrect
		Camera st = new Camera();
		st.setMode(Mode.Video);
		st.takePhoto(); //error
	}
}

This would represent a symbolic automata with the following view:

The language of the refinements to add the enums should be discussed prior to implementation since there could be several options. One possibility would be the one presented above mode == Mode.Video, but others could be value(mode) == Mode.Video or video(mode).

High-level steps to change the current behavior

1. Change the refinements grammar to allow the invocation of the enumerate.
2. Change the traversing of the AST to analyze enum definitions and store the values in context
3. Change the traversing of the AST to account for the enumerate as a parameter and store its information in the context.
4. See how the enums information can be translated into the SMT and check if the verification condition works.