Members/kono/jpf-core: src/main/gov/nasa/jpf/util/script/ScriptEnvironment.java comparison

comparison src/main/gov/nasa/jpf/util/script/ScriptEnvironment.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

comparison

equal deleted inserted replaced

--1:000000000000
+:61d41facf527
+/*
+* 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.util.script;
+import gov.nasa.jpf.JPF;
+import gov.nasa.jpf.util.StateExtensionClient;
+import gov.nasa.jpf.util.StateExtensionListener;
+import gov.nasa.jpf.vm.ChoiceGenerator;
+import java.io.FileNotFoundException;
+import java.io.FileReader;
+import java.io.Reader;
+import java.util.ArrayList;
+import java.util.BitSet;
+import java.util.HashMap;
+import java.util.List;
+/**
+* class representing a statemachine environment that produces SCEventGenerators
+* from scripts
+*/
+public abstract class ScriptEnvironment<CG extends ChoiceGenerator<?>>
+implements StateExtensionClient<ScriptEnvironment<CG>.ActiveSnapshot> {
+static final String DEFAULT = "default";
+//--- just a helper tuple
+static class ActiveSequence implements Cloneable {
+String stateName;
+Section section;
+SequenceInterpreter intrp;
+public ActiveSequence (String stateName, Section section, SequenceInterpreter intrp) {
+this.stateName = stateName;
+this.section = section;
+this.intrp = intrp;
+}
+@Override
+	public Object clone() {
+try {
+ActiveSequence as = (ActiveSequence) super.clone();
+as.intrp = (SequenceInterpreter) intrp.clone();
+return as;
+} catch (CloneNotSupportedException nonsense) {
+return null; // we are a Cloneable, so we don't get here
+}
+}
+public boolean isDone() {
+return intrp.isDone();
+}
+}
+//--- our state extension - we need this mostly for cloning (deep copy)
+class ActiveSnapshot implements Cloneable {
+ActiveSequence[] actives;
+ActiveSnapshot () {
+actives = new ActiveSequence[0];
+}
+ActiveSnapshot (ActiveSequence[] as) {
+actives = as;
+}
+public ActiveSequence get (String stateName) {
+for (ActiveSequence as : actives) {
+if (as.stateName.equals(stateName)) {
+return as;
+}
+}
+return null;
+}
+@Override
+	public Object clone() {
+try {
+ActiveSnapshot ss = (ActiveSnapshot)super.clone();
+for (int i=0; i<actives.length; i++) {
+ActiveSequence as = actives[i];
+ss.actives[i] = (ActiveSequence)as.clone();
+}
+return ss;
+} catch (CloneNotSupportedException nonsense) {
+return null; // we are a Cloneable, so we don't get here
+}
+}
+ActiveSnapshot advance (String[] activeStates, BitSet isReEntered) {
+ActiveSequence[] newActives = new ActiveSequence[activeStates.length];
+//--- carry over the persisting entries
+for (int i=0; i<activeStates.length; i++) {
+String sn = activeStates[i];
+for (ActiveSequence as : actives) {
+if (as.stateName.equals(sn) ) {
+// we could use isReEntered to determine if we want to restart sequences
+// <2do> how do we factor this out as policy?
+newActives[i] = (ActiveSequence)as.clone();
+}
+}
+}
+//--- add the new ones
+int skipped = 0;
+nextActive:
+for (int i=0; i<activeStates.length; i++) {
+if (newActives[i] == null) {
+// get the script section
+Section sec = getSection(activeStates[i]);
+if (sec != null) {
+// check if that section is already processed by another active state, in which case we skip
+for (int j=0; j<newActives.length; j++) {
+if (newActives[j] != null && newActives[j].section == sec) {
+skipped++;
+continue nextActive;
+}
+}
+// check if it was processed by a prev state (superstate section by a
+// common parent of a new and an old state - this is the common case
+for (int j=0; j<actives.length; j++) {
+// <2do> how do we handle state re-entering?
+if (actives[j].section == sec) {
+ActiveSequence as = new ActiveSequence(activeStates[i], sec, actives[j].intrp);
+newActives[i] = as;
+continue nextActive;
+}
+}
+// it's a new one
+ActiveSequence as = new ActiveSequence(activeStates[i], sec,
+new SequenceInterpreter(sec));
+newActives[i] = as;
+} else { // sec == null : we didn't find any sequence for this state
+skipped++;
+}
+}
+}
+//--- compress if we skipped any active states
+if (skipped > 0) {
+int n = activeStates.length - skipped;
+ActiveSequence[] na = new ActiveSequence[n];
+for (int i=0, j=0; j<n; i++) {
+if (newActives[i] != null) {
+na[j++] = newActives[i];
+}
+}
+newActives = na;
+}
+return new ActiveSnapshot(newActives);
+}
+}
+//--- start of ScriptEnvronment
+String scriptName;
+Reader scriptReader;
+Script script;
+ActiveSnapshot cur;
+HashMap<String,Section> sections = new HashMap<String,Section>();
+Section defaultSection;
+//--- initialization
+public ScriptEnvironment (String fname) throws FileNotFoundException {
+this( fname, new FileReader(fname));
+}
+public ScriptEnvironment (String name, Reader r) {
+this.scriptName = name;
+this.scriptReader = r;
+}
+public void parseScript () throws ESParser.Exception {
+ESParser parser= new ESParser(scriptName, scriptReader);
+script = parser.parse();
+initSections();
+cur = new ActiveSnapshot();
+}
+void initSections() {
+Section defSec = new Section(script, DEFAULT);
+for (ScriptElement e : script) {
+if (e instanceof Section) {
+Section sec = (Section)e;
+List<String> secIds = sec.getIds();
+if (secIds.size() > 0) {
+for (String id : secIds) {
+sections.put(id, (Section)sec.clone()); // clone to guarantee different identities
+}
+} else {
+sections.put(secIds.get(0), sec);
+}
+} else { // add copy to default sequence
+defSec.add(e.clone());
+}
+}
+if (defSec.getNumberOfChildren() > 0) {
+defaultSection = defSec;
+}
+}
+Section getSection (String id) {
+Section sec = null;
+while (id != null) {
+sec = sections.get(id);
+if (sec != null) {
+return sec;
+}
+int idx = id.lastIndexOf('.');
+if (idx > 0) {
+id = id.substring(0, idx); // ?? do we really want this recursive? that's policy
+} else {
+id = null;
+}
+}
+return defaultSection;
+}
+void addExpandedEvent(ArrayList<Event> events, Event se) {
+for (Event e : se.expand()) {
+if (!events.contains(e)) {
+events.add(e);
+}
+}
+}
+static final String[] ACTIVE_DEFAULT = { DEFAULT };
+public CG getNext (String id) {
+return getNext(id, ACTIVE_DEFAULT, null);
+}
+public CG getNext (String id, String[] activeStates) {
+return getNext(id, activeStates, null);
+}
+// this is our main purpose in life, but there is some policy in here
+public CG getNext (String id, String[] activeStates, BitSet isReEntered) {
+cur = cur.advance(activeStates, isReEntered);
+ArrayList<Event> events = new ArrayList<Event>(cur.actives.length);
+for (ActiveSequence as : cur.actives) {
+while (true) {
+ScriptElement se = as.intrp.getNext();
+if (se != null) {
+if (se instanceof Event) {
+addExpandedEvent(events, (Event)se);
+break;
+} else if (se instanceof Alternative) {
+for (ScriptElement ase : (Alternative)se) {
+if (ase instanceof Event) {
+addExpandedEvent(events, (Event)ase);
+}
+}
+break;
+} else {
+// get next event
+}
+} else {
+break; // process next active sequence
+}
+}
+}
+return createCGFromEvents(id, events);
+}
+protected abstract CG createCGFromEvents(String id, List<Event> events);
+//--- StateExtension interface
+@Override
+public ActiveSnapshot getStateExtension() {
+return cur;
+}
+@Override
+public void restore(ActiveSnapshot stateExtension) {
+cur = stateExtension;
+}
+@Override
+public void registerListener(JPF jpf) {
+StateExtensionListener<ActiveSnapshot> sel = new StateExtensionListener(this);
+jpf.addSearchListener(sel);
+}
+}

Mercurial > hg > Members > kono > jpf-core

comparison src/main/gov/nasa/jpf/util/script/ScriptEnvironment.java @ 0:61d41facf527