diff --git a/src/de/unibremen/informatik/hets/model/Actuals.java b/src/de/unibremen/informatik/hets/model/Actuals.java new file mode 100644 index 0000000..e0a04f1 --- /dev/null +++ b/src/de/unibremen/informatik/hets/model/Actuals.java @@ -0,0 +1,11 @@ +package de.unibremen.informatik.hets.model; + +public class Actuals extends Spec { + public Actuals(String cont, String anno) { + super(cont, anno); + } + + public String toString() { + return content + "\n"; + } +} diff --git a/src/de/unibremen/informatik/hets/model/Basicspec.java b/src/de/unibremen/informatik/hets/model/Basicspec.java new file mode 100644 index 0000000..62e7033 --- /dev/null +++ b/src/de/unibremen/informatik/hets/model/Basicspec.java @@ -0,0 +1,7 @@ +package de.unibremen.informatik.hets.model; + +public class Basicspec extends Spec { + public Basicspec(String cont, String anno) { + super(cont, anno); + } +} diff --git a/src/de/unibremen/informatik/hets/model/HetFile.java b/src/de/unibremen/informatik/hets/model/HetFile.java new file mode 100644 index 0000000..ead64ab --- /dev/null +++ b/src/de/unibremen/informatik/hets/model/HetFile.java @@ -0,0 +1,42 @@ +package de.unibremen.informatik.hets.model; + +import java.util.ArrayList; + +public class HetFile { + private String libname; + private ArrayList specdefns; + + public HetFile(String name) { + libname = name; + specdefns = new ArrayList(); + } + + public void add(SpecDefn specdefn) { + specdefns.add(specdefn); + } + + public String toString() { + StringBuilder builder = new StringBuilder(); + + builder.append("library "); + builder.append(libname); + builder.append("\n\n"); + + String logic = ""; + + for (SpecDefn specdefn : specdefns) { + if (logic != specdefn.getLogic()) { + logic = specdefn.getLogic(); + + builder.append("logic "); + builder.append(logic); + builder.append("\n\n"); + } + + builder.append(specdefn.toString()); + builder.append("\n"); + } + + return builder.toString(); + } +} diff --git a/src/de/unibremen/informatik/hets/model/PPXMLParser.java b/src/de/unibremen/informatik/hets/model/PPXMLParser.java new file mode 100644 index 0000000..abb7be6 --- /dev/null +++ b/src/de/unibremen/informatik/hets/model/PPXMLParser.java @@ -0,0 +1,156 @@ +package de.unibremen.informatik.hets.model; + +import java.util.ArrayList; +import java.io.InputStream; +import java.io.IOException; + +import de.unibremen.informatik.hets.model.HetFile; +import de.unibremen.informatik.hets.model.PPXMLParserException; +import de.unibremen.informatik.hets.common.xml.Dom; +import de.unibremen.informatik.hets.common.lang.StringUtils; + +import org.w3c.dom.Document; +import org.w3c.dom.Element; +import org.w3c.dom.Node; +import org.xml.sax.SAXException; + +import javax.xml.parsers.DocumentBuilderFactory; +import javax.xml.parsers.ParserConfigurationException; + +public class PPXMLParser { + static { + } + + public PPXMLParser() { + super(); + } + + private static String getrange(String hetfile, String range) throws PPXMLParserException { + int minus = range.indexOf('-'); + int fromdot, todot; + int fromline, fromcolumn; + int toline, tocolumn; + + String from, to; + + try { + from = range.substring(0, minus); + to = range.substring(minus+1); + } catch (IndexOutOfBoundsException e) { + throw new PPXMLParserException(e); + } + + fromdot = from.indexOf('.'); + todot = to.indexOf('.'); + + if (fromdot == -1 || todot == -1) { + throw new PPXMLParserException(); + } + + try { + fromline = Integer.parseInt(from.substring(0, fromdot)); + fromcolumn = Integer.parseInt(from.substring(fromdot+1)); + + toline = Integer.parseInt(to.substring(0, todot)); + tocolumn = Integer.parseInt(to.substring(todot+1)); + } catch (NumberFormatException e) { + throw new PPXMLParserException(e); + } catch (IndexOutOfBoundsException e) { + throw new PPXMLParserException(e); + } + + try { + return StringUtils.getSlice(hetfile, fromline, fromcolumn, toline, tocolumn); + } catch (java.io.IOException e) { + throw new PPXMLParserException(e); + } + } + + private static Spec parsespec(String hetfile, Element spec) throws PPXMLParserException { + spec = Dom.getFirstChildElement(spec); + + if (spec == null) { + throw new PPXMLParserException(" block doesnt have a child"); + } + + if (spec.getTagName() == "Union") { + Union un = new Union(); + ArrayList speclist = Dom.getChildElements(spec); + + for (Element s : speclist) { + un.add(parsespec(hetfile, s)); + } + return un; + } else { + return parsespecspec(hetfile, spec); + } + } + + private static Spec parsespecspec(String hetfile, Element spec) throws PPXMLParserException { + Element left = Dom.getFirstChildElement(spec); + + String annotation = ""; + + if (left != null && left.getTagName() == "Left") { + annotation = Dom.getTextContent(Dom.getFirstChildElement(left)); + } + + if (spec.getTagName() == "Basicspec") { + return new Basicspec(getrange(hetfile, spec.getAttribute("range")), annotation); + } else if (spec.getTagName() == "Actuals") { + return new Actuals(spec.getAttribute("name"), annotation); + } else { + throw new PPXMLParserException(); + } + } + + public static HetFile parse(InputStream ppxml, String hetfile) throws PPXMLParserException { + Document document; + + try { + document = DocumentBuilderFactory.newInstance().newDocumentBuilder().parse(ppxml); + } catch (ParserConfigurationException e) { + throw new PPXMLParserException(e); + } catch (org.xml.sax.SAXException e) { + throw new PPXMLParserException(e); + } catch (IOException e) { + throw new PPXMLParserException(e); + } + + Node root = document.getDocumentElement(); + + HetFile het = new HetFile(((Element)root).getAttribute("name")); + + ArrayList list = Dom.getChildElements(root); + + String currentlogic = ""; + + for (Element item : list) { + if (item.getNodeName() == "Logic") { + currentlogic = ((Element)item).getAttribute("name"); + } else if (item.getNodeName() == "SpecDefn") { + if (currentlogic == "") { + throw new PPXMLParserException(); + } + + SpecDefn specdefn = new SpecDefn(((Element)item).getAttribute("name"), currentlogic); + + Element child = Dom.getFirstChildElement(item); + + if (child.getTagName() == "Basicspec") { + specdefn.add(parsespecspec(hetfile, child)); + } else if (child.getTagName() == "Extension") { + ArrayList speclist = Dom.getChildElements(child); + + for (Element spec : speclist) { + specdefn.add(parsespec(hetfile, spec)); + } + } + + het.add(specdefn); + } + } + + return het; + } +} diff --git a/src/de/unibremen/informatik/hets/model/PPXMLParserException.java b/src/de/unibremen/informatik/hets/model/PPXMLParserException.java new file mode 100644 index 0000000..b4f15bc --- /dev/null +++ b/src/de/unibremen/informatik/hets/model/PPXMLParserException.java @@ -0,0 +1,15 @@ +package de.unibremen.informatik.hets.model; + +public class PPXMLParserException extends Exception { + public PPXMLParserException(Throwable cause) { + super(cause); + } + + public PPXMLParserException() { + super(); + } + + public PPXMLParserException(String message) { + super(message); + } +} diff --git a/src/de/unibremen/informatik/hets/model/Spec.java b/src/de/unibremen/informatik/hets/model/Spec.java new file mode 100644 index 0000000..173b0af --- /dev/null +++ b/src/de/unibremen/informatik/hets/model/Spec.java @@ -0,0 +1,29 @@ +package de.unibremen.informatik.hets.model; + +public class Spec { + protected String annotation; + protected String content; + + public Spec(String cont, String anno) { + content = cont; + annotation = anno; + } + + public Spec(String cont) { + content = cont; + annotation = null; + } + + public Spec() { + content = null; + annotation = null; + } + + public String toString() { + return content; + } + + public String getAnnotation() { + return annotation; + } +} diff --git a/src/de/unibremen/informatik/hets/model/SpecDefn.java b/src/de/unibremen/informatik/hets/model/SpecDefn.java new file mode 100644 index 0000000..675231f --- /dev/null +++ b/src/de/unibremen/informatik/hets/model/SpecDefn.java @@ -0,0 +1,59 @@ +package de.unibremen.informatik.hets.model; + +import java.util.ArrayList; +import java.util.Iterator; + +public class SpecDefn { + private ArrayList specs; + private String name; + private String logic; + + public SpecDefn(String n, String l) { + name = n; + logic = l; + specs = new ArrayList(); + } + + public void add(Spec spec) { + specs.add(spec); + } + + public String getLogic() { + return logic; + } + + public String toString() { + StringBuilder builder = new StringBuilder(); + + builder.append("spec "); + builder.append(name); + builder.append(" ="); + + Iterator it = specs.iterator(); + for (;;) { + Spec spec = it.next(); + String annotation = spec.getAnnotation(); + + if (annotation != null) { + builder.append(" "); + builder.append(spec.getAnnotation()); + } + + if (!(spec instanceof Union)) { + builder.append("\n"); + } + builder.append(spec.toString()); + + if (it.hasNext()) { + builder.append("then"); + } else { + break; + } + } + + builder.append("end"); + builder.append("\n"); + + return builder.toString(); + } +} diff --git a/src/de/unibremen/informatik/hets/model/Union.java b/src/de/unibremen/informatik/hets/model/Union.java new file mode 100644 index 0000000..16d1565 --- /dev/null +++ b/src/de/unibremen/informatik/hets/model/Union.java @@ -0,0 +1,46 @@ +package de.unibremen.informatik.hets.model; + +import java.util.ArrayList; +import java.util.Iterator; + +public class Union extends Spec { + private ArrayList specs; + + public Union() { + specs = new ArrayList(); + } + + public void add(Spec spec) { + if (spec instanceof Union) { + return; + } else { + specs.add(spec); + } + } + + public String toString() { + StringBuilder builder = new StringBuilder(); + + Iterator it = specs.iterator(); + for (;;) { + Spec spec = it.next(); + String annotation = spec.getAnnotation(); + + if (annotation != null) { + builder.append(" "); + builder.append(spec.getAnnotation()); + } + + builder.append("\n"); + builder.append(spec.toString()); + + if (it.hasNext()) { + builder.append("and"); + } else { + break; + } + } + + return builder.toString(); + } +}