merge Header.js removing the admin condition for design

designer/designer/src/pt/ist/socialsoftware/blendedworkflow/designer/remote/resourcemodel/ResourceModelInterface.java

@@ -8,8 +8,6 @@
 import org.springframework.web.client.RestClientException;
 import org.springframework.web.client.RestTemplate;
 
-import pt.ist.socialsoftware.blendedworkflow.designer.remote.datamodel.dto.RelationDTO;
-import pt.ist.socialsoftware.blendedworkflow.designer.remote.datamodel.dto.RuleDTO;
 import pt.ist.socialsoftware.blendedworkflow.designer.remote.resourcemodel.dto.CapabilityDTO;
 import pt.ist.socialsoftware.blendedworkflow.designer.remote.resourcemodel.dto.PersonDTO;
 import pt.ist.socialsoftware.blendedworkflow.designer.remote.resourcemodel.dto.PositionDTO;
@@ -34,9 +32,7 @@ public static ResourceModelInterface getInstance() {
 		}
 		return instance;
 	}
-
-
-
+
 	public Boolean cleanResourceModel(String specId) {
 		logger.debug("cleanResourceModel: {}", specId);
 
@@ -50,7 +46,7 @@ public Boolean cleanResourceModel(String specId) {
 
 		return response;
 	}
-	
+
 	public Boolean checkEntityIsPerson(String specId, String path, BWNotification notification) {
 		logger.debug("cleanResourceModel: {}", specId);
 
@@ -63,7 +59,7 @@ public Boolean checkEntityIsPerson(String specId, String path, BWNotification no
 		Boolean response = false;
 		try {
 			response = restTemplate.postForObject(uri, path, Boolean.class, params);
-			
+
 			if (response) {
 				notification.addError(new BWError("Entity is not person", "Entity provided is not a person"));
 			}
@@ -72,14 +68,13 @@ public Boolean checkEntityIsPerson(String specId, String path, BWNotification no
 		} catch (Exception e) {
 			notification.addError(new BWError("Error", e.getMessage()));
 		}
-
 
 		return response;
 	}
-	
+
 	public boolean createResourceModel(String specId, BWNotification notification) {
 		logger.debug("createResourceModel");
-		
+
 		final String uri = BASE_URL + "/specs/{specId}/resourcemodel/";
 
 		Map<String, String> params = new HashMap<>();
@@ -94,10 +89,10 @@ public boolean createResourceModel(String specId, BWNotification notification) {
 		} catch (Exception e) {
 			notification.addError(new BWError("Error", e.getMessage()));
 		}
-		
+
 		return result;
 	}
-	
+
 	public CapabilityDTO createCapability(CapabilityDTO capability, BWNotification notification) {
 		logger.debug("createCapability: {}, {}", capability.getName(), capability.getDescription());
 
@@ -115,10 +110,10 @@ public CapabilityDTO createCapability(CapabilityDTO capability, BWNotification n
 		} catch (Exception e) {
 			notification.addError(new BWError("Error", e.getMessage()));
 		}
-		
+
 		return result;
 	}
-	
+
 	public RoleDTO createRole(RoleDTO role, BWNotification notification) {
 		logger.debug("createRole: {}, {}", role.getName(), role.getDescription());
 
@@ -136,10 +131,10 @@ public RoleDTO createRole(RoleDTO role, BWNotification notification) {
 		} catch (Exception e) {
 			notification.addError(new BWError("Error", e.getMessage()));
 		}
-		
+
 		return result;
 	}
-	
+
 	public UnitDTO createUnit(UnitDTO unit, BWNotification notification) {
 		logger.debug("createUnit: {}, {}", unit.getName(), unit.getDescription());
 
@@ -157,12 +152,13 @@ public UnitDTO createUnit(UnitDTO unit, BWNotification notification) {
 		} catch (Exception e) {
 			notification.addError(new BWError("Error", e.getMessage()));
 		}
-		
+
 		return result;
 	}
-	
+
 	public PositionDTO createPosition(PositionDTO position, BWNotification notification) {
-		logger.debug("createPerson: {}, {}, {}, {}, {}, {}", position.getName(), position.getUnit(), position.getRoles(), position.getDelegateToRelations(), position.getReportsTo());
+		logger.debug("createPerson: {}, {}, {}, {}, {}, {}", position.getName(), position.getUnit(),
+				position.getRoles(), position.getDelegateToRelations(), position.getReportsTo());
 
 		final String uri = BASE_URL + "/specs/{specId}/resourcemodel/positions";
 
@@ -178,12 +174,13 @@ public PositionDTO createPosition(PositionDTO position, BWNotification notificat
 		} catch (Exception e) {
 			notification.addError(new BWError("Error", e.getMessage()));
 		}
-		
+
 		return result;
 	}
-	
+
 	public PositionDTO initPosition(PositionDTO position, BWNotification notification) {
-		logger.debug("createPerson: {}, {}, {}, {}, {}, {}", position.getName(), position.getUnit(), position.getRoles(), position.getDelegateToRelations(), position.getReportsTo());
+		logger.debug("createPerson: {}, {}, {}, {}, {}, {}", position.getName(), position.getUnit(),
+				position.getRoles(), position.getDelegateToRelations(), position.getReportsTo());
 
 		final String uri = BASE_URL + "/specs/{specId}/resourcemodel/positions/init";
 
@@ -199,10 +196,10 @@ public PositionDTO initPosition(PositionDTO position, BWNotification notificatio
 		} catch (Exception e) {
 			notification.addError(new BWError("Error", e.getMessage()));
 		}
-		
+
 		return result;
 	}
-	
+
 	public PersonDTO createPerson(PersonDTO person, BWNotification notification) {
 		logger.debug("createPerson: {}, {}, {}, {}", person.getName(), person.getCapabilities(), person.getPositions());
 
@@ -220,11 +217,12 @@ public PersonDTO createPerson(PersonDTO person, BWNotification notification) {
 		} catch (Exception e) {
 			notification.addError(new BWError("Error", e.getMessage()));
 		}
-		
+
 		return result;
 	}
 
-	public ResourceRelationDTO createEntityIsPersonRelation(ResourceRelationDTO resourceRelationDTO, BWNotification notification) {
+	public ResourceRelationDTO createEntityIsPersonRelation(ResourceRelationDTO resourceRelationDTO,
+			BWNotification notification) {
 		logger.debug("createRelations: {}", resourceRelationDTO.getEntityName());
 
 		final String uri = BASE_URL + "/specs/{specId}/resourcerules/relations/";
@@ -241,7 +239,7 @@ public ResourceRelationDTO createEntityIsPersonRelation(ResourceRelationDTO reso
 		} catch (Exception e) {
 			notification.addError(new BWError("Error", e.getMessage()));
 		}
-		
+
 		return result;
 	}
 
@@ -257,7 +255,7 @@ public boolean createResourceRule(ResourceRuleDTO ruleDTO, BWNotification notifi
 		ResourceRuleDTO result = null;
 		try {
 			result = restTemplate.postForObject(uri, ruleDTO, ResourceRuleDTO.class, params);
-			
+
 			return true;
 		} catch (RestClientException rce) {
 			notification.addError(new BWError("REST connection", rce.getMessage()));

designer/designer/src/pt/ist/socialsoftware/blendedworkflow/designer/remote/resourcemodel/WriteResourceModelService.java

@@ -7,7 +7,6 @@
 
 import pt.ist.socialsoftware.blendedworkflow.designer.blendedWorkflow.Capability;
 import pt.ist.socialsoftware.blendedworkflow.designer.blendedWorkflow.Person;
-import pt.ist.socialsoftware.blendedworkflow.designer.blendedWorkflow.Position;
 import pt.ist.socialsoftware.blendedworkflow.designer.blendedWorkflow.ResourceSpecification;
 import pt.ist.socialsoftware.blendedworkflow.designer.blendedWorkflow.Role;
 import pt.ist.socialsoftware.blendedworkflow.designer.blendedWorkflow.Unit;
@@ -21,101 +20,106 @@
 import pt.ist.socialsoftware.blendedworkflow.designer.remote.utils.BWNotification;
 
 public class WriteResourceModelService {
-private Logger logger = LoggerFactory.getLogger(WriteDataModelService.class);
-	
+	private final Logger logger = LoggerFactory.getLogger(WriteDataModelService.class);
+
 	private ResourceModelInterface repository = null;
-	
+
 	private WriteResourceRulesService rulesService = null;
-	
+
 	public WriteResourceModelService(DataModelInterface dmRepository, ResourceModelInterface repository) {
 		this.repository = repository;
 		this.rulesService = new WriteResourceRulesService(dmRepository, repository);
 	}
-	
+
 	public void writeResourceModel(ResourceSpecification spec, String specId, BWNotification notification) {
 		System.out.println("[WriteRM] Begin writing resource model");
-		
+
 		createCapabilities(spec, specId, notification);
-		
+
 		createRoles(spec, specId, notification);
-		
+
 		createUnits(spec, specId, notification);
-		
+
 		createPositions(spec, specId, notification);
-		
+
 		createPersons(spec, specId, notification);
-		
-		rulesService.writeResourceRules(spec.getResourceRules(), specId, notification);
-	
+
+		this.rulesService.writeResourceRules(spec.getResourceRules(), specId, notification);
+
 		System.out.println("[WriteRM] Finish writing resource model");
 	}
-	
+
 	public void createResourceModel(String specId, BWNotification notification) {
-		repository.createResourceModel(specId, notification);
+		this.repository.createResourceModel(specId, notification);
 	}
 
 	private void createCapabilities(ResourceSpecification spec, String specId, BWNotification notification) {
 		for (Capability c : spec.getCapabilities()) {
 			System.out.printf("[WriteCapability] Name: %s; Description: %s\n", c.getName(), c.getDescription());
-			repository.createCapability(new CapabilityDTO(specId, c.getName(), c.getDescription()), notification);
+			this.repository.createCapability(new CapabilityDTO(specId, c.getName(), c.getDescription()), notification);
 		}
 	}
 
 	private void createRoles(ResourceSpecification spec, String specId, BWNotification notification) {
 		for (Role r : spec.getRoles()) {
 			System.out.printf("[WriteRole] Name: %s; Description: %s\n", r.getName(), r.getDescription());
-			repository.createRole(new RoleDTO(specId, r.getName(), r.getDescription()), notification);
+			this.repository.createRole(new RoleDTO(specId, r.getName(), r.getDescription()), notification);
 		}
 	}
-	
+
 	private void createUnits(ResourceSpecification spec, String specId, BWNotification notification) {
 		for (Unit u : spec.getUnits()) {
 			System.out.printf("[WriteUnit] Name: %s; Description: %s\n", u.getName(), u.getDescription());
-			repository.createUnit(new UnitDTO(specId, u.getName(), u.getDescription()), notification);
+			this.repository.createUnit(new UnitDTO(specId, u.getName(), u.getDescription()), notification);
 		}
 	}
-	
+
 	private void createPositions(ResourceSpecification spec, String specId, BWNotification notification) {
 		// First pass: Create simple positions with names
 		spec.getPositions().stream().forEach(p -> {
 			PositionDTO position = new PositionDTO(specId, p.getName(), p.getUnit().getName(), p.getDescription());
-			System.out.printf("[WritePosition] Name: %s; Description: %s\n", position.getName(), position.getDescription());
-			repository.createPosition(position, notification);
+			System.out.printf("[WritePosition] Name: %s; Description: %s\n", position.getName(),
+					position.getDescription());
+			this.repository.createPosition(position, notification);
 		});
-		
+
 		// Second pass: Create associations between positions
 		spec.getPositions().stream().forEach(p -> {
 			PositionDTO position = new PositionDTO(specId, p.getName(), p.getUnit().getName(), p.getDescription());
-			System.out.printf("[InitPosition] Name: %s; Description: %s\n", position.getName(), position.getDescription());
+			System.out.printf("[InitPosition] Name: %s; Description: %s\n", position.getName(),
+					position.getDescription());
 			if (p.getRoles() != null) {
 				position.setRoles(p.getRoles().stream().map(r -> r.getName()).collect(Collectors.toList()));
 			}
-			
+
 			if (p.getDelegateTo() != null) {
-				position.setDelegateToRelations(p.getDelegateTo().stream().map(r -> r.getName()).collect(Collectors.toList()));
+				position.setDelegateToRelations(
+						p.getDelegateTo().stream().map(r -> r.getName()).collect(Collectors.toList()));
 			}
-			
+
 			if (p.getReportsTo() != null) {
 				position.setReportsTo(p.getReportsTo().getName());
 			}
-			
-			repository.initPosition(position, notification);		
+
+			this.repository.initPosition(position, notification);
 		});
 	}
-	
+
 	private void createPersons(ResourceSpecification spec, String specId, BWNotification notification) {
 		for (Person p : spec.getPersons()) {
 			PersonDTO personDTO = new PersonDTO(specId, p.getName(), p.getDescription());
-			
+
 			if (p.getCapabilities() != null) {
-				personDTO.setCapabilities(p.getCapabilities().stream().map(c -> c.getName()).collect(Collectors.toList()));
+				personDTO.setCapabilities(
+						p.getCapabilities().stream().map(c -> c.getName()).collect(Collectors.toList()));
 			}
-			
+
 			if (p.getOccupies() != null) {
-				personDTO.setPositions(p.getOccupies().stream().map(position -> position.getName()).collect(Collectors.toList()));
+				personDTO.setPositions(
+						p.getOccupies().stream().map(position -> position.getName()).collect(Collectors.toList()));
 			}
 			System.out.printf("[WritePerson] Name: %s; Description: %s\n", p.getName(), p.getDescription());
-			repository.createPerson(personDTO, notification);		
+			this.repository.createPerson(personDTO, notification);
 		}
 	}
 }

designer/models/doctorappointment/src/A-A.bw

@@ -1,6 +1,6 @@
 Specification: "A associate to A" 
 
-Entity A mandatory {
+Entity A mandatory { 
 	att1 : Number
 } 
 

designer/models/doctorappointment/src/doctorappointment.bw

@@ -1,7 +1,7 @@
 Specification: "Doctor Appointment"  
 
-Entity Patient {
-	name : String
+Entity Patient { 
+	name : String 
 	age : Number
 	heartProblems : Boolean
 }         

designer/models/doctorappointment/src/entityA.bw

@@ -1,6 +1,6 @@
 Specification: "Two Entities" 
 
-Entity A mandatory {
+Entity A mandatory { 
 	att1 : Number
 } 
 

designer/models/doctorappointment/src/fourEntities.bw

@@ -1,6 +1,6 @@
 Specification: "Four Entities" 
 
-Entity A mandatory {
+Entity A mandatory { 
 	att1 : Number
 } 
 

frontend/bw-react/src/components/Header.js

@@ -113,7 +113,7 @@ class ConnectedHeader extends React.Component {
                          <NavItem eventKey={2}>
                             {this.props.spec.name}
                         </NavItem>
-                        {this.props.user.username === "Admin" && <NavDropdown eventKey={3} title="Designer" id="basic-nav-dropdown">
+                        <NavDropdown eventKey={3} title="Designer" id="basic-nav-dropdown">
                             <LinkContainer to='/specifications/designer/datamodel'>
                                 <MenuItem eventKey={3.1}>Data Model</MenuItem>
                             </LinkContainer>
@@ -122,7 +122,7 @@ class ConnectedHeader extends React.Component {
                                 <MenuItem eventKey={3.3}>Goal Model</MenuItem>
                             </LinkContainer>
                             <MenuItem eventKey={3.4}>Activity Model</MenuItem>
-                        </NavDropdown>}
+                        </NavDropdown>
                         <NavDropdown eventKey={4} title="Instance" id="basic-nav-dropdown">
                             <LinkContainer to='/specifications/instances'>
                                 <MenuItem eventKey={4.1} onClick={() => {this.props.selectInstance('')}}>Manage Instances</MenuItem>

verifier/ApproachOperationAsSignature/DoctorAppointment/ActivityModelExec.als

@@ -4,7 +4,7 @@ open filesystem/ActivityModelExec
 
 open filesystem/DoctorAppointment/ActivityModel
 
-run final for 4 but 7 State, 6 Activity, 5 Int
+//run final for 4 but 7 State, 6 Activity, 5 Int
 
 assert preserveInvariants {
 	all s, s': State, a: Activity |

verifier/ApproachOperationAsSignature/DoctorAppointment/GoalModelExec.als

@@ -4,7 +4,7 @@ open filesystem/GoalModelExec
 
 open filesystem/DoctorAppointment/GoalModel
 
-run final for 4 but 11 State, 10 Goal, 5 Int
+//run final for 4 but 11 State, 10 Goal, 5 Int
 
 assert preserveInvariants {
 	all s, s': State, g: Goal |