package FoldableDrill {
	private import ScalarValues::*;
	private import ScalarFunctions::*;
	private import Hierarchy::*;
	private import Communication::*;
	private import MathFunctions::*;

	// Definitions
	
	// This enum can be used for the command to open/close the system
	enum def Cmd_Enum {
		enum OPEN;
		enum CLOSE;
	}
	
	// This enum can be used for the command to handle the motors
	enum def Motor_Enum {
		enum OPEN;
		enum CLOSE;
		enum IDLE;
	}
	
	part def FoldableDrill {
		in command : Cmd_Enum;
		
		part drill : Drill::Drill;
		part cavity : DrillCavity::DrillCavity;
		part controller : Controller::Controller;
			
 		bind command = controller.command;
		connect drill.sensed_value to controller.drill_sensed_value;
		connect cavity.sensed_value to controller.door_sensed_value;
		connect controller.drill_operation to drill.operation;
		connect controller.door_operation to cavity.operation;
	}	
		
	package Drill {	
		part def Drill {
			in operation : Motor_Enum;
			out sensed_value : Integer;
			
			part hinge : DrillFoldHinge::DrillFoldHinge;
			part drill_motor : ElectricMotor::ElectricMotor;
			part drill_angle_sensor : AngleSensor::AngleSensor;
			
			connect hinge.percentage to drill_angle_sensor.value;
			connect drill_motor.torque to hinge.torque;
			bind drill_angle_sensor.sensed_value = sensed_value;
			bind operation = drill_motor.operation;
		}
	}
	
	package DrillFoldHinge {	
		part def DrillFoldHinge {
			in torque : Integer;
			out percentage : Integer;
			
			state DrillFoldHingeStates {
				
				// init transition, drill is open
				entry assign percentage := 100; // transition effect as variables assigments
				then primary; 
				
				// states declaration 
				state primary;

	            transition 'idle'
		            first primary
		            if torque == 0  // guard
		            do assign percentage := percentage // effect
		            then primary;

	            transition 'increment'
		            first primary
		            if torque > 0 // guard
		            do assign percentage := min(100, percentage + 10) // effect
		            then primary;

	            transition 'decrement'
		            first primary
		            if torque < 0 // guard
		            do assign percentage := max(0, percentage - 10) // effect
		            then primary;
			}
		}
	}
	
	package DrillCavity {	
		part def DrillCavity {
			in operation : Motor_Enum;
			out sensed_value : Integer;
			
			part door : DrillCavityDoor::DrillCavityDoor;
			part door_motor : ElectricMotor::ElectricMotor;
			part door_angle_sensor : AngleSensor::AngleSensor;
			
			connect door.percentage to door_angle_sensor.value;
			connect door_motor.torque to door.torque;
			bind door_angle_sensor.sensed_value = sensed_value;
			bind operation = door_motor.operation;
		}
	}
	
	package DrillCavityDoor {	
		part def DrillCavityDoor {
			in torque : Integer;
			out percentage : Integer;
			
			state DrillCavityDoorStates {
				
				// init transition, door is closed
				entry assign percentage := 0; // transition effect as variables assigments
				then primary; 
				
				// states declaration 
				state primary;

	            transition 'increment'
		            first primary
		            if torque > 0 // guard
		            do assign percentage := min(100, percentage + 10) // effect
		            then primary;

	            transition 'decrement'
		            first primary
		            if torque < 0 // guard
		            do assign percentage := max(0, percentage - 10) // effect
		            then primary;

	            transition 'idle'
		            first primary
		            if torque == 0  // guard
		            do assign percentage := percentage // effect
		            then primary;
			}
		}
	}
	
	package AngleSensor {	
		part def AngleSensor {
			in value : Integer;
			out sensed_value : Integer;

			state AngleSensorStates {
				
				// init transition				
				entry assign sensed_value := value; // transition effect as variables assigments
				then primary; 
				
				// states declaration 
				state primary;
				
	            transition 'primary-primary'
		            first primary
		            do action {assign sensed_value := value;} // effect
		            then primary;
			}
		}
	}
 	
	package ElectricMotor {	
		part def ElectricMotor {
			in operation : Motor_Enum;
			out torque : Integer;
			
			state ElectricMotorStates {
				
				// init transition				
				entry assign torque := 0;
				then idle; 
				
				// states declaration 
				state idle;
				state opening;
				state closing;
				
	            transition 'idle-opening'
		            first idle
		            if operation == Motor_Enum::OPEN	// guard
		            do assign torque := 10 				// effect
		            then opening;

	            transition 'opening-idle'
		            first opening
		            if operation == Motor_Enum::IDLE	// guard
		            do assign torque := 0				// effect
		            then idle; 
		            
	            transition 'idle-closing'
		            first idle
		            if operation == Motor_Enum::CLOSE	// guard
		            do assign torque := -10				// effect
		            then closing;
		            
	            transition 'closing-idle'
		            first closing
		            if operation == Motor_Enum::IDLE	// guard
		            do assign torque := 0				// effect
		            then idle;

	            transition 'closing-opening'
		            first closing
		            if operation == Motor_Enum::OPEN	// guard
		            do assign torque := 10				// effect
		            then opening;

	            transition 'opening-closing'
		            first opening
		            if operation == Motor_Enum::CLOSE	// guard
		            do assign torque := -10				// effect
		            then closing;
		            
	            transition 'opening-opening'
		            first opening
		            if operation == Motor_Enum::OPEN	// guard
		            do assign torque := 10				// effect
		            then opening;
		            
	            transition 'closing-closing'
		            first closing
		            if operation == Motor_Enum::CLOSE	// guard
		            do assign torque := -10				// effect
		            then closing;
		            
	            transition 'idle-idle'
		            first idle
		            if operation == Motor_Enum::IDLE	// guard
		            do assign torque := 0				// effect
		            then idle;
			}
		}
	}
	
	package Controller {	
		part def Controller {
			in command : Cmd_Enum;
			in drill_sensed_value : Integer;
			in door_sensed_value : Integer;
			out drill_operation : Motor_Enum;
			out door_operation : Motor_Enum;
			
			state ControllerStates {			

				// init transition, motors stopped
				entry action {assign drill_operation := Motor_Enum::IDLE; assign door_operation := Motor_Enum::IDLE;} // transition effect as variables assigments
//				then Drill_open; 
				then drill_closed; 
				
				// states declaration 
				state drill_open;
				state door_opening_when_open;
				state drill_closing;
				state door_closing_when_open;
				state drill_closed;
				state door_opening_when_closed;
				state drill_opening;
				state door_closing_when_closed;
				
				// self loop, do nothing until CLOSE				
	            transition 'drill_open_self'
		            first drill_open
		            if command == Cmd_Enum::OPEN // guard
		            do action {assign drill_operation := Motor_Enum::IDLE; assign door_operation := Motor_Enum::IDLE;} // effect
		            then drill_open;

				// start opening the door		
	            transition 'drill_open-door_opening_when_open'
		            first drill_open
		            if command == Cmd_Enum::CLOSE // guard
		            do action {assign drill_operation := Motor_Enum::IDLE; assign door_operation := Motor_Enum::OPEN;} // effect
		            then door_opening_when_open;

				// self loop, door is not open enough yet				
	            transition 'door_opening_when_open-self'
		            first door_opening_when_open
		            if command == Cmd_Enum::CLOSE and door_sensed_value < 40 // guard
		            do action {assign drill_operation := Motor_Enum::IDLE; assign door_operation := Motor_Enum::OPEN;} // effect
		            then door_opening_when_open;

				// the door is open enough, start to close the drill and stop the door
	            transition 'door_opening_when_open-drill_closing'
		            first door_opening_when_open
		            if command == Cmd_Enum::CLOSE and door_sensed_value >= 40  // guard
		            do action {assign drill_operation := Motor_Enum::CLOSE; assign door_operation := Motor_Enum::OPEN;} // effect
		            then drill_closing;

				// self loop when the drill is not closed enough, keep closing the drill
	            transition 'drill_closing-self'
		            first drill_closing
		            if command == Cmd_Enum::CLOSE and drill_sensed_value > 40 // guard
		            do action {assign drill_operation := Motor_Enum::CLOSE; assign door_operation := Motor_Enum::IDLE;} // effect
		            then drill_closing;

				// the drill is closed enough, start to close also the door
	            transition 'drill_closing-door_closing_when_open'
		            first drill_closing
		            if command == Cmd_Enum::CLOSE and drill_sensed_value <= 40 // guard
		            do action {assign drill_operation := Motor_Enum::CLOSE; assign door_operation := Motor_Enum::CLOSE;} // effect
		            then door_closing_when_open;

				// self loop when both motors are active
	            transition 'door_closing_when_open-self1'
		            first door_closing_when_open
		            if command == Cmd_Enum::CLOSE and door_sensed_value > 0 and drill_sensed_value > 0// guard
		            do action {assign drill_operation := Motor_Enum::CLOSE; assign door_operation := Motor_Enum::CLOSE;} // effect
		            then door_closing_when_open;

				// self loop when only door is closing
	            transition 'door_closing_when_open-self2'
		            first door_closing_when_open
		            if command == Cmd_Enum::CLOSE and door_sensed_value > 0 and drill_sensed_value == 0// guard
		            do action {assign drill_operation := Motor_Enum::IDLE; assign door_operation := Motor_Enum::CLOSE;} // effect
		            then door_closing_when_open;

				// the door is closed, stop the motors
	            transition 'door_closing_when_open-drill_closed'
		            first door_closing_when_open
		            if command == Cmd_Enum::CLOSE and door_sensed_value == 0 // guard
		            do action {assign drill_operation := Motor_Enum::IDLE; assign door_operation := Motor_Enum::IDLE;} // effect
		            then drill_closed;

				// self loop until an OPEN arrives
	            transition 'drill_closed-self'
		            first drill_closed
		            if command == Cmd_Enum::CLOSE // guard
		            do action {assign drill_operation := Motor_Enum::IDLE; assign door_operation := Motor_Enum::IDLE;} // effect
		            then drill_closed;

				// start opening the door
	            transition 'drill_closed-door_opening_when_closed'
		            first drill_closed
		            if command == Cmd_Enum::OPEN // guard
		            do action {assign drill_operation := Motor_Enum::IDLE; assign door_operation := Motor_Enum::OPEN;} // effect
		            then door_opening_when_closed;

				// self loop, door is not open enough yet				
	            transition 'door_opening_when_closed_self'
		            first door_opening_when_closed
		            if command == Cmd_Enum::OPEN and door_sensed_value < 40 // guard
		            do action {assign drill_operation := Motor_Enum::IDLE; assign door_operation := Motor_Enum::OPEN;} // effect
		            then door_opening_when_closed;

				// the door is open enough, start to open the drill and stop the door
	            transition 'door_opening_when_closed-drill_opening'
		            first door_opening_when_closed
		            if command == Cmd_Enum::OPEN and door_sensed_value >= 40 // guard
		            do action {assign drill_operation := Motor_Enum::OPEN; assign door_operation := Motor_Enum::OPEN;} // effect
		            then drill_opening;

				// self loop when the drill is not open enough, keep opening the drill	
	            transition 'drill_opening_self'
		            first drill_opening
		            if command == Cmd_Enum::OPEN and drill_sensed_value < 40 // guard
		            do action {assign drill_operation := Motor_Enum::OPEN; assign door_operation := Motor_Enum::IDLE;} // effect
		            then drill_opening;

				// the drill is open enough, start to close the door
	            transition 'drill_opening-door_closing_when_closed'
		            first drill_opening
		            if command == Cmd_Enum::OPEN and drill_sensed_value >= 40 // guard
		            do action {assign drill_operation := Motor_Enum::OPEN; assign door_operation := Motor_Enum::CLOSE;} // effect
		            then door_closing_when_closed;			
					
				// self loop when both motors are active				
	            transition 'door_closing_when_closed-self1'
		            first door_closing_when_closed
		            if command == Cmd_Enum::OPEN and door_sensed_value > 0 and drill_sensed_value < 100 // guard
		            do action {assign drill_operation := Motor_Enum::OPEN; assign door_operation := Motor_Enum::CLOSE;} // effect
		            then door_closing_when_closed;

				// self loop when only door is active
	            transition 'door_closing_when_closed-self2'
		            first door_closing_when_closed
		            if command == Cmd_Enum::OPEN and door_sensed_value > 0 and drill_sensed_value == 100  // guard
		            do action {assign drill_operation := Motor_Enum::IDLE; assign door_operation := Motor_Enum::CLOSE;} // effect
		            then door_closing_when_closed;

				// the door is closed, stop the motor		
	            transition 'door_closing_when_closed-drill_open'
		            first door_closing_when_closed
		            if command == Cmd_Enum::CLOSE and door_sensed_value == 0 // guard
		            do action {assign drill_operation := Motor_Enum::IDLE; assign door_operation := Motor_Enum::IDLE;} // effect
		            then drill_open;
		            
		         // Backward transitions

				 // close the door
				 transition 'door_opening_when_open-door_closing_when_closed'
		            first door_opening_when_open
		            if command == Cmd_Enum::OPEN // guard
		            do action {assign drill_operation := Motor_Enum::IDLE; assign door_operation := Motor_Enum::IDLE;} // effect
		            then door_closing_when_closed;
		         
				 // open the drill and close the door
				 transition 'drill_closing-door_closing_when_closed'
		            first drill_closing
		            if command == Cmd_Enum::OPEN // guard
		            do action {assign drill_operation := Motor_Enum::OPEN; assign door_operation := Motor_Enum::IDLE;} // effect
		            then door_closing_when_closed;
		         
				// open the door and stop drill
				transition 'door_closing_when_open-door_opening_when_closed'
		            first door_closing_when_open
		            if command == Cmd_Enum::OPEN // guard
		            do action {assign drill_operation := Motor_Enum::IDLE; assign door_operation := Motor_Enum::OPEN;} // effect
		            then door_opening_when_closed;
		         
				// close the door
				transition 'door_opening_when_closed-door_closing_when_open'
		            first door_opening_when_closed
		            if command == Cmd_Enum::CLOSE // guard
		            do action {assign drill_operation := Motor_Enum::IDLE; assign door_operation := Motor_Enum::CLOSE;} // effect
		            then door_closing_when_open;

				// close the drill and the door
				transition 'drill_opening-door_closing_when_open'
		            first drill_opening
		            if command == Cmd_Enum::CLOSE // guard
		            do action {assign drill_operation := Motor_Enum::CLOSE; assign door_operation := Motor_Enum::CLOSE;} // effect
		            then door_closing_when_open;
		         
				// open the door
				transition 'door_closing_when_closed-door_opening_when_open'
		            first door_closing_when_closed
		            if command == Cmd_Enum::CLOSE // guard
		            do action {assign drill_operation := Motor_Enum::IDLE; assign door_operation := Motor_Enum::IDLE;} // effect
		            then door_opening_when_open;
	        }
		}
	}
	// Usage level: system decomposition and parts are interconnected
	part system : FoldableDrill, SystemComponent {
	}
}
/*
 * For model checking, use: 
 *   System component + invar + ic3 controller.State!=drill_open											// state reachability
 *   controller component + invar + ic3 State!=drill_open													// state reachability on the single component
 *   controller component + ltlspec + ic3 G(State=drill_closed -> X(State!=drill_closed))					// state instability if valid (no self loop)
 *   System component + ltlspec + ic3 G(controller.State=drill_closed -> G(controller.State=drill_closed))	// state trap if valid
 *   System component + ltlspec + ic3 G(controller.State = drill_closing -> cavity.door.percentage >= 40)	// it shows that it can happen!
 *   System component + ltlspec + ic3 G(controller.State=drill_open -> cavity.door.percentage=0)			// the door should be closed, but it isn't
 */
