org.eclipse.emf.henshin.statespace.external.prism
Class MDPStateSpaceExporter

java.lang.Object
  org.eclipse.emf.henshin.statespace.external.AbstractStateSpaceExporter
      org.eclipse.emf.henshin.statespace.external.prism.MDPStateSpaceExporter

All Implemented Interfaces:

StateSpaceExporter

public class MDPStateSpaceExporter
extends AbstractStateSpaceExporter

Exporter for PRISM. This generates an MDP or a PTA model.

Field Summary

static String

EXPORTER_ID ID of this exporter.

Fields inherited from class org.eclipse.emf.henshin.statespace.external.AbstractStateSpaceExporter

stateSpaceIndex

Constructor Summary

MDPStateSpaceExporter()

Method Summary

void	doExport(StateSpace stateSpace, URI uri, String parameters, org.eclipse.core.runtime.IProgressMonitor monitor) Perform the export operation.
String[]	getFileExtensions() Get the list of file extensions supported by this exporter.
String	getName() Get the name of this exported.

Methods inherited from class org.eclipse.emf.henshin.statespace.external.AbstractStateSpaceExporter

createWriter, setStateSpaceIndex

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

EXPORTER_ID

public static final String EXPORTER_ID

ID of this exporter.

See Also:

Constant Field Values

Constructor Detail

MDPStateSpaceExporter

public MDPStateSpaceExporter()

Method Detail

doExport

public void doExport(StateSpace stateSpace,
                     URI uri,
                     String parameters,
                     org.eclipse.core.runtime.IProgressMonitor monitor)
              throws IOException,
                     StateSpaceException

Description copied from interface: StateSpaceExporter

Perform the export operation.

Parameters:

stateSpace - State space to be exported.

uri - URI where the state space should be exported to.

monitor - Progress monitor.

Throws:

StateSpaceException - On state space errors.

IOException

getName

public String getName()

Description copied from interface: StateSpaceExporter

Get the name of this exported.

Returns:

The name.

getFileExtensions

public String[] getFileExtensions()

Description copied from interface: StateSpaceExporter

Get the list of file extensions supported by this exporter.

Returns:

List of file extensions.