Adding support for condition of if statement

promela/analyse_comm_param.go

@@ -218,6 +218,15 @@ func (m *Model) AnalyseCommParam(pack string, fun *ast.FuncDecl, ast_map map[str
 									}
 								}
 							}
+
+							if sel.Sel.Name == "Mutex" {
+								switch sel := sel.X.(type) {
+								case *ast.Ident:
+									if sel.Name == "sync" {
+										contains_chan = true
+									}
+								}
+							}
 						}
 					}
 				}
@@ -228,7 +237,6 @@ func (m *Model) AnalyseCommParam(pack string, fun *ast.FuncDecl, ast_map map[str
 						// look inter procedurally
 						new_model := m.newModel(pack, fun_decl)
 						new_model.RecFuncs = m.RecFuncs
-						// new_model.AddRecFunc(pack, fun) // MAYBE THIS IS AN ERROR SO UNCOMMENT IF BUG
 						params_1, err1 := new_model.AnalyseCommParam(pack, fun_decl, ast_map, log)
 
 						if err1 != nil {

promela/if_stmt.go

@@ -2,10 +2,10 @@ package promela
 
 import (
 	"errors"
+	"github.com/nicolasdilley/gomela/promela/promela_ast"
 	"go/ast"
 	"go/token"
-
-	"github.com/nicolasdilley/gomela/promela/promela_ast"
+	"strconv"
 )
 
 func (m *Model) translateIfStmt(s *ast.IfStmt) (b *promela_ast.BlockStmt, defers *promela_ast.BlockStmt, err *ParseError) {
@@ -27,6 +27,16 @@ func (m *Model) translateIfStmt(s *ast.IfStmt) (b *promela_ast.BlockStmt, defers
 	}
 
 	stmts1, err2 := m.TranslateExpr(s.Cond)
+	// add the condition if it contains comm param
+
+	cond, contains_comm_param := m.translateIfCond(s.Cond)
+
+	// if contains_comm_param add the cond to the modelled if statement
+
+	var g promela_ast.Expr = &promela_ast.Ident{Name: "true"}
+	if contains_comm_param {
+		g = cond
+	}
 
 	if err2 != nil {
 		err = err2
@@ -44,7 +54,7 @@ func (m *Model) translateIfStmt(s *ast.IfStmt) (b *promela_ast.BlockStmt, defers
 	contains := false
 	if len(body.List) != 0 {
 		contains = true
-		i.Guards = append(i.Guards, &promela_ast.GuardStmt{Cond: &promela_ast.Ident{Name: "true"}, Body: body})
+		i.Guards = append(i.Guards, &promela_ast.GuardStmt{Cond: g, Body: body})
 	}
 
 	if s.Else != nil {
@@ -71,10 +81,17 @@ func (m *Model) translateIfStmt(s *ast.IfStmt) (b *promela_ast.BlockStmt, defers
 		}
 		if len(stmts.List) != 0 {
 			contains = true
-			i.Guards = append(i.Guards, &promela_ast.GuardStmt{Cond: &promela_ast.Ident{Name: "true"}, Body: stmts})
+
+			if contains_comm_param {
+				i.Guards = append(i.Guards, &promela_ast.GuardStmt{Cond: &promela_ast.Ident{Name: "else"}, Body: stmts})
+			} else {
+				i.Guards = append(i.Guards, &promela_ast.GuardStmt{Cond: &promela_ast.Ident{Name: "true"}, Body: stmts})
+			}
 		}
-	} else if contains {
+	} else if contains && !contains_comm_param {
 		i.Guards = append(i.Guards, &promela_ast.GuardStmt{Cond: &promela_ast.Ident{Name: "true"}, Body: &promela_ast.BlockStmt{}})
+	} else if contains_comm_param {
+		i.Guards = append(i.Guards, &promela_ast.GuardStmt{Cond: &promela_ast.Ident{Name: "else"}, Body: &promela_ast.BlockStmt{}})
 	}
 
 	if contains {
@@ -148,6 +165,45 @@ func (m *Model) isIfClosed(s *ast.IfStmt) (isClosed bool, b *promela_ast.BlockSt
 	return
 }
 
+func (m *Model) translateIfCond(expr ast.Expr) (promela_ast.Expr, bool) {
+	prom_expr := &promela_ast.BinaryExpr{}
+
+	switch expr := expr.(type) {
+	case *ast.BinaryExpr:
+		lhs, ident := ContainsCommParam(m.CommPars, &CommPar{Name: &ast.Ident{Name: m.getIdent(expr.X).Name}})
+		lit, err := strconv.Atoi(m.getIdent(expr.X).Name)
+
+		var x string = ""
+
+		if lhs {
+			x = VAR_PREFIX + ident.Name.Name
+		}
+
+		if err == nil {
+			lhs = true
+			x = strconv.Itoa(lit)
+		}
+
+		rhs, ident2 := ContainsCommParam(m.CommPars, &CommPar{Name: &ast.Ident{Name: m.getIdent(expr.Y).Name}})
+
+		lit, err = strconv.Atoi(m.getIdent(expr.Y).Name)
+
+		var y string = ""
+		if rhs {
+			y = VAR_PREFIX + ident2.Name.Name
+		}
+		if err == nil {
+			rhs = true
+			y = strconv.Itoa(lit)
+		}
+		if lhs && rhs {
+			return &promela_ast.BinaryExpr{Lhs: &promela_ast.Ident{Name: x}, Rhs: &promela_ast.Ident{Name: y}, Op: expr.Op.String()}, true
+		}
+	}
+	return prom_expr, false
+
+}
+
 func (m *Model) containsIsClosed(expr ast.Expr) bool {
 	for _, exprs := range m.ClosedVars {
 		for _, e := range exprs {