Mercurial > hg > Members > kono > jpf-core
view src/main/gov/nasa/jpf/report/Publisher.java @ 0:61d41facf527
initial v8 import (history reset)
author | Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> |
---|---|
date | Fri, 23 Jan 2015 10:14:01 -0800 |
parents | |
children |
line wrap: on
line source
/* * Copyright (C) 2014, United States Government, as represented by the * Administrator of the National Aeronautics and Space Administration. * All rights reserved. * * The Java Pathfinder core (jpf-core) platform is licensed under the * Apache License, Version 2.0 (the "License"); you may not use this file except * in compliance with the License. You may obtain a copy of the License at * * http://www.apache.org/licenses/LICENSE-2.0. * * Unless required by applicable law or agreed to in writing, software * distributed under the License is distributed on an "AS IS" BASIS, * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. * See the License for the specific language governing permissions and * limitations under the License. */ package gov.nasa.jpf.report; import gov.nasa.jpf.Config; import java.io.PrintWriter; import java.text.DateFormat; import java.util.ArrayList; import java.util.Date; import java.util.List; /** * abstract base for all format specific publishers. Note that this interface * also has to work for non-stream based reporting, i.e. within Eclipse * (we don't want to re-parse from text reports there) */ public abstract class Publisher { // output phases public static final int START = 1; public static final int TRANSITION = 2; public static final int PROBE = 3; public static final int CONSTRAINT = 4; public static final int PROPERTY_VIOLATION = 5; public static final int FINISHED = 6; protected Config conf; protected Reporter reporter; // our master protected String[] startItems = {}; protected String[] transitionItems = {}; protected String[] propertyViolationItems = {}; protected String[] constraintItems = {}; protected String[] finishedItems = {}; protected String[] probeItems = {}; DateFormat dtgFormatter = DateFormat.getDateTimeInstance(DateFormat.SHORT, DateFormat.SHORT); ArrayList<PublisherExtension> extensions; /** * to be initialized in openChannel * NOTE - not all publishers need to have one */ protected PrintWriter out; public PrintWriter getOut () { return out; } protected Publisher (Config conf, Reporter reporter){ this.conf = conf; this.reporter = reporter; setTopicItems(); } public void setItems (int category, String[] newTopics){ switch (category){ case START: startItems = newTopics; break; case PROBE: probeItems = newTopics; break; case TRANSITION: transitionItems = newTopics; break; case CONSTRAINT: constraintItems = newTopics; break; case PROPERTY_VIOLATION: propertyViolationItems = newTopics; break; case FINISHED: finishedItems = newTopics; break; default: Reporter.log.warning("unknown publisher topic: " + category); } } public abstract String getName(); protected void setTopicItems () { setTopicItems(getName()); } protected void setTopicItems (String name) { String prefix = "report." + name; startItems = conf.getStringArray(prefix + ".start", startItems); transitionItems = conf.getStringArray(prefix + ".transition", transitionItems); probeItems = conf.getStringArray(prefix + ".probe", transitionItems); propertyViolationItems = conf.getStringArray(prefix + ".property_violation", propertyViolationItems); constraintItems = conf.getStringArray(prefix + ".constraint", constraintItems); finishedItems = conf.getStringArray(prefix + ".finished", finishedItems); } public void addExtension (PublisherExtension ext) { if (extensions == null) { extensions = new ArrayList<PublisherExtension>(); } extensions.add(ext); } // <2do> should not be a list we can add to private static final List<PublisherExtension> EMPTY_LIST = new ArrayList<PublisherExtension>(0); public List<PublisherExtension> getExtensions(){ if (extensions != null){ return extensions; } else { return EMPTY_LIST; // make life easier for callers } } public String getLastErrorId() { return reporter.getCurrentErrorId(); } public boolean hasTopic (String topic) { for (String s : startItems) { if (s.equalsIgnoreCase(topic)){ return true; } } for (String s : transitionItems) { if (s.equalsIgnoreCase(topic)){ return true; } } for (String s : constraintItems) { if (s.equalsIgnoreCase(topic)){ return true; } } for (String s : propertyViolationItems) { if (s.equalsIgnoreCase(topic)){ return true; } } for (String s : finishedItems) { if (s.equalsIgnoreCase(topic)){ return true; } } return false; } public String formatDTG (Date date) { return dtgFormatter.format(date); } /** static public String _formatHMS (long t) { t /= 1000; // convert to sec long s = t % 60; long h = t / 3600; long m = (t % 3600) / 60; StringBuilder sb = new StringBuilder(); sb.append(h); sb.append(':'); if (m < 10){ sb.append('0'); } sb.append(m); sb.append(':'); if (s < 10){ sb.append('0'); } sb.append(s); return sb.toString(); } **/ static char[] tBuf = { '0', '0', ':', '0', '0', ':', '0', '0' }; static synchronized public String formatHMS (long t) { int h = (int) (t / 3600000); int m = (int) ((t / 60000) % 60); int s = (int) ((t / 1000) % 60); tBuf[0] = (char) ('0' + (h / 10)); tBuf[1] = (char) ('0' + (h % 10)); tBuf[3] = (char) ('0' + (m / 10)); tBuf[4] = (char) ('0' + (m % 10)); tBuf[6] = (char) ('0' + (s / 10)); tBuf[7] = (char) ('0' + (s % 10)); return new String(tBuf); } public String getReportFileName (String key) { String fname = conf.getString(key); if (fname == null){ fname = conf.getString("report.file"); if (fname == null) { fname = "report"; } } return fname; } public void publishTopicStart (String topic) { // to be done by subclasses } public void publishTopicEnd (String topic) { // to be done by subclasses } public boolean hasToReportStatistics() { for (String s : finishedItems) { if ("statistics".equalsIgnoreCase(s)){ return true; } } return false; } //--- open/close streams etc protected void openChannel(){} protected void closeChannel(){} //--- if you have different preferences about when to report things, override those public void publishStart() { for (String item : startItems) { if ("jpf".equalsIgnoreCase(item)){ publishJPF(); } else if ("platform".equalsIgnoreCase(item)){ publishPlatform(); } else if ("user".equalsIgnoreCase(item)) { } else if ("dtg".equalsIgnoreCase(item)) { publishDTG(); } else if ("config".equalsIgnoreCase(item)){ publishJPFConfig(); } else if ("sut".equalsIgnoreCase(item)){ publishSuT(); } } if (extensions != null) { for (PublisherExtension e : extensions) { e.publishStart(this); } } } public void publishTransition() { for (String topic : transitionItems) { if ("statistics".equalsIgnoreCase(topic)){ publishStatistics(); } } if (extensions != null) { for (PublisherExtension e : extensions) { e.publishTransition(this); } } } public void publishConstraintHit() { for (String item : constraintItems) { if ("constraint".equalsIgnoreCase(item)) { publishConstraint(); } else if ("trace".equalsIgnoreCase(item)){ publishTrace(); } else if ("snapshot".equalsIgnoreCase(item)){ publishSnapshot(); } else if ("output".equalsIgnoreCase(item)){ publishOutput(); } else if ("statistics".equalsIgnoreCase(item)){ publishStatistics(); // not sure if that is good for anything } } if (extensions != null) { for (PublisherExtension e : extensions) { e.publishConstraintHit(this); } } } public void publishProbe(){ for (String topic : probeItems) { if ("statistics".equalsIgnoreCase(topic)){ publishStatistics(); } } if (extensions != null) { for (PublisherExtension e : extensions) { e.publishProbe(this); } } } public void publishPropertyViolation() { for (String topic : propertyViolationItems) { if ("error".equalsIgnoreCase(topic)) { publishError(); } else if ("trace".equalsIgnoreCase(topic)){ publishTrace(); } else if ("snapshot".equalsIgnoreCase(topic)){ publishSnapshot(); } else if ("output".equalsIgnoreCase(topic)){ publishOutput(); } else if ("statistics".equalsIgnoreCase(topic)){ publishStatistics(); // not sure if that is good for anything } } if (extensions != null) { for (PublisherExtension e : extensions) { e.publishPropertyViolation(this); } } } public void publishFinished() { if (extensions != null) { for (PublisherExtension e : extensions) { e.publishFinished(this); } } for (String topic : finishedItems) { if ("result".equalsIgnoreCase(topic)){ publishResult(); } else if ("statistics".equalsIgnoreCase(topic)){ publishStatistics(); } } } protected void publishProlog() {} // XML headers etc protected void publishEpilog() {} // likewise at the end //--- our standard topics (only placeholders here) protected void publishJPF() {} protected void publishJPFConfig() {} protected void publishPlatform() {} protected void publishUser() {} protected void publishDTG() {} protected void publishJava() {} protected void publishSuT() {} protected void publishResult() {} protected void publishError() {} protected void publishConstraint() {} protected void publishTrace() {} protected void publishOutput() {} protected void publishSnapshot() {} protected void publishStatistics() {} //--- internal helpers }