allow shorter spec --- @Interface is not mandatory

[cdsspec-compiler.git] / src / edu / uci / eecs / specExtraction / SpecExtractor.java

diff --git a/src/edu/uci/eecs/specExtraction/SpecExtractor.java b/src/edu/uci/eecs/specExtraction/SpecExtractor.java
index d3a2521223e3a3c5a9f918de46de5161fbaf8544..afa42f78033b5d34475c38c5601fa251950563fc 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/SpecExtractor.java
+++ b/src/edu/uci/eecs/specExtraction/SpecExtractor.java
@@ -624,7 +624,7 @@ public class SpecExtractor {
                        lineReader = new LineNumberReader(br);
                        // "/\*\*\s*@(DeclareState|Interface)"
                        Pattern regexpBegin = Pattern
-                                       .compile("/\\*\\*\\s*@(DeclareState|Interface|Define)");
+                                       .compile("/\\*\\*\\s*@(DeclareState|Interface|PreCondition|Transition|PostCondition|Define)");
                        Matcher matcher = regexpBegin.matcher("");
 
                        String line;
@@ -652,7 +652,10 @@ public class SpecExtractor {
                                        if (constructName.equals(SpecNaming.DeclareState)) {
                                                extractGlobalConstruct(file, lineReader, line,
                                                                beginLineNum);
-                                       } else if (constructName.equals(SpecNaming.Interface)) {
+                                       } else if (constructName.equals(SpecNaming.Interface)
+                                                       || constructName.equals(SpecNaming.PreCondition)
+                                                       || constructName.equals(SpecNaming.Transition)
+                                                       || constructName.equals(SpecNaming.PostCondition)) {
                                                extractInterfaceConstruct(file, lineReader, line,
                                                                beginLineNum);
                                        } else if (constructName.equals(SpecNaming.Define)) {