From 53a05282fa5d1968aabbc79ef6bc384004e79097 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Mon, 30 Jan 2012 22:46:27 +0000
Subject: [PATCH] Bug fix: PTA model checking using games should complain about
 not supporting system...endystem.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4526 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/pta/PTAModelChecker.java | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/prism/src/pta/PTAModelChecker.java b/prism/src/pta/PTAModelChecker.java
index 2e39099a..3511c49a 100644
--- a/prism/src/pta/PTAModelChecker.java
+++ b/prism/src/pta/PTAModelChecker.java
@@ -111,6 +111,11 @@ public class PTAModelChecker
 		// Starting model checking
 		timer = System.currentTimeMillis();
 
+		// Check for system...endsystem - not supported yet
+		if (modulesFile.getSystemDefn() != null) {
+			throw new PrismException("The system...endsystem construct is not supported yet (try the digital clocks engine instead)");
+		}
+		
 		// Translate ModulesFile object into a PTA object
 		mainLog.println("\nBuilding PTA...");
 		m2pta = new Modules2PTA(prism, modulesFile);