Skip to content

Commit

Permalink
Added a type checking rule for the Main Machine
Browse files Browse the repository at this point in the history
  • Loading branch information
Christine Zhou committed Oct 9, 2024
1 parent 8c4c600 commit cbd553f
Show file tree
Hide file tree
Showing 3 changed files with 27 additions and 11 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@
using Plang.Compiler.TypeChecker.AST;
using Plang.Compiler.TypeChecker.AST.Declarations;
using Plang.Compiler.TypeChecker.AST.ModuleExprs;
using Plang.Compiler.TypeChecker.Types;

namespace Plang.Compiler.TypeChecker
{
Expand Down Expand Up @@ -189,13 +190,21 @@ internal void CheckSafetyTest(SafetyTest test)
$"test module is not closed with respect to created interfaces; interface {@interface.First().Name} is created but not implemented inside the module");
}

//check that the test module main machine exists
// check that the test module main machine exists
var hasMainMachine = test.ModExpr.ModuleInfo.InterfaceDef.Values.Any(m => m.Name == test.Main && !m.IsSpec);
if (!hasMainMachine)
{
throw handler.NoMain(test.SourceLocation,
$"machine {test.Main} does not exist in the test module");
}

// make sure that the main machine does not take a parameter as input
globalScope.Get(test.Main, out Machine main);
if (!main.PayloadType.Equals(PrimitiveType.Null))
{
throw handler.NoMain(test.SourceLocation,
$"main machine {test.Main} cannot take an input parameter in the entry function of the start state.");
}
}

internal void CheckImplementationDecl(Implementation impl)
Expand Down
Original file line number Diff line number Diff line change
@@ -1,21 +1,20 @@

/* PSrc/FrontDesk.p */
type tRoomInfo = (roomNumber: int, isAvailable: bool);


machine Main {
var rooms: map[int, tRoomInfo];
start state Init {
entry {
new m1(default(map[int, tRoomInfo]));
}
}
}

machine m1 {
start state Init {
entry Init_Entry;
exit {
assert true;
}
}

fun Init_Entry(initialRooms: map[int, tRoomInfo]) {
new Main(default(map[int, tRoomInfo]));
assert true;
}
}


}
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
machine Main {
start state Init {
entry (payload: int) {};
exit {
assert true;
}
}
}

0 comments on commit cbd553f

Please sign in to comment.