org.ginsim.service.export.nusmv

Class NuSMVExportService

java.lang.Object

org.ginsim.service.export.nusmv.NuSMVExportService

All Implemented Interfaces:

Service

@MetaInfServices(value=Service.class)
 @Alias(value="NuSMV")
 @ServiceStatus(value=RELEASED)
public class NuSMVExportService
extends Object
implements Service

GINsim export service capable of encoding the working model into a NuSMV specification. It currently uses NuSMV version 2.5.3.

It considers the use of priority classes for every model, whichever the updating policy defined inside GINsim. If a given model considers priority classes, it maps the corresponding classes. However, if a given model considers an asynchronous (synchronous) updating policy, it creates an equivalent mapping using priority classes, one class for each (all the) variable(s).

Author:

Pedro T. Monteiro

Constructor Summary

Constructors

Constructor and Description
NuSMVExportService()

Method Summary

Modifier and Type	Method and Description
void	export(NuSMVConfig config, File file)
NuSMVConfig	getConfig(org.colomoto.biolqm.LogicalModel model)
void	run(org.colomoto.biolqm.LogicalModel model, String filename)
void	run(NuSMVConfig config, String filename)

Methods inherited from class java.lang.Object

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

Constructor Detail

NuSMVExportService

public NuSMVExportService()

Method Detail

getConfig

public NuSMVConfig getConfig(org.colomoto.biolqm.LogicalModel model)

run

public void run(org.colomoto.biolqm.LogicalModel model,
                String filename)
         throws IOException,
                GsException

Throws:

IOException

GsException

run

public void run(NuSMVConfig config,
                String filename)
         throws IOException,
                GsException

Throws:

IOException

GsException

export

public void export(NuSMVConfig config,
                   File file)
            throws IOException,
                   GsException

Throws:

IOException

GsException