StandaloneContext¶

public class StandaloneContext extends io.cocotec.coco.platform.coco.Context ¶: A Context that allows new modules to be loaded.

Constructors¶

StandaloneContext¶

public StandaloneContext(APIClient client)¶

StandaloneContext¶

protected StandaloneContext(APIClient client, long objectId)¶: Internal constructor

Methods¶

addDiagnosticsConsumer¶

public void addDiagnosticsConsumer(io.cocotec.coco.platform.coco.DiagnosticConsumer consumer)¶: Adds a diagnostic consumer that will receive diagnostics about errors found about nodes within this Context. The caller is responsible for ensuring that the DiagnosticConsumer remains valid whilst the context is active: the context does not take ownership of the DiagnosticConsumer at all.

addImportPath¶

public void addImportPath(String directoryPath)¶: Appends a directory to the back of the list of paths in which imported modules are loaded. This can only be called prior to load_module and only if load_root_package and add_package_dependency are not called.

addPackageDependency¶

public boolean addPackageDependency(String directoryPath)¶: Imports a package and makes it available for importing from. This can only be called prior to load_module and only if load_root_package is not called.

addPackageSource¶

public void addPackageSource(String directoryPath)¶: Appends a directory to the list of directories from which Coco packages can be resolved. This can only be called prior to load_root_package.

addVerificationProgressListener¶

public void addVerificationProgressListener(io.cocotec.coco.platform.coco.VerificationProgressListener listener)¶: Adds a verification progress monitor that will receive callbacks about verification events in this Context. The caller is responsible for ensuring that the VerificationProgressListener remains valid whilst the context is active: the context does not take ownership of the VerificationProgressListener at all.

finalize¶

protected void finalize()¶

getObjectId¶

public long getObjectId()¶: Internal method

getOrCreate¶

public static StandaloneContext getOrCreate(APIClient client, long objectId)¶: Internal method

internalExportModuleEmf¶

public io.cocotec.coco.platform.coco.ExportedEmfmodule internalExportModuleEmf(io.cocotec.coco.platform.coco.Node node, String resourceUri)¶: Internal method: should not be used directly.

internalLoadBinaryModule¶

public io.cocotec.coco.platform.coco.Node internalLoadBinaryModule(String resourceUri, byte[] moduleData)¶: Internal method: should not be used directly.

internalNodeEmfUri¶

public String internalNodeEmfUri(io.cocotec.coco.platform.coco.Node node)¶: Internal method: should not be used directly.

internalNodeWithEmfUri¶

public io.cocotec.coco.platform.coco.Node internalNodeWithEmfUri(String proxyUri)¶: Internal method: should not be used directly.

internalPrintBinaryModule¶

public String internalPrintBinaryModule(byte[] moduleData)¶: Internal method: should not be used directly.

internalPrintBinaryModule¶

public String internalPrintBinaryModule(byte[] moduleData, String formatSpecification)¶: Internal method: should not be used directly.

loadModule¶

public io.cocotec.coco.platform.coco.Node loadModule(String moduleImportPath, io.cocotec.coco.platform.coco.ModulePathType modulePathType)¶

Loads the given module. If this module is already loaded, this will not reload the module.

Parameters:	moduleImportPath – This should either be a path to the given file relative to one of the import paths, or the name of a module. modulePathType – The type of the argument to module_import_path.
Returns:	The root Coco element. If loading fails this will be an invalid node in which case diagnostics will be reported to this Context’s DiagnosticConsumer.

loadModule¶

public io.cocotec.coco.platform.coco.Node loadModule(String moduleImportPath)¶

loadModule¶

public io.cocotec.coco.platform.coco.Node loadModule(String moduleImportPath, String moduleData)¶

Loads the given module using the specified data as its contents.

Parameters:	moduleImportPath – The path to the module in the form of A.B.C (i.e. ModulePathType::ModulePath). moduleData – The Coco source code for the given module.
Returns:	The root Coco element. If loading fails this will be an invalid node in which case diagnostics will be reported to this Context’s DiagnosticConsumer.

loadPackageModules¶

public java.util.ArrayList<io.cocotec.coco.platform.coco.Node> loadPackageModules()¶

Loads all modules in the package. Requires that load_root_package has been called.

Returns:	The nodes for each of the modules that are loaded. If any module could not be loaded, then its corresponding node will not be valid.

loadRootPackage¶

public boolean loadRootPackage(String directoryPath)¶

Loads a Coco package, making all modules in the package available for loading. This can only be called prior to the other load methods, since it will affect how all subsequent modules are loaded into this context.

Parameters:	directoryPath – The path to the directory containing a Coco.toml file to load.
Returns:	true if an error occurred. If an error was raised, a diagnostic will have been reported to this context’s DiagnosticConsumer.

moduleAssertion¶

public io.cocotec.coco.platform.coco.VerificationAssertion moduleAssertion(io.cocotec.coco.platform.coco.Node moduleNode)¶: The assertion that corresponds to given module.

rootAssertion¶

public io.cocotec.coco.platform.coco.VerificationAssertion rootAssertion()¶: The root assertion for this context.

setDeterministicCounterexamples¶

public void setDeterministicCounterexamples(boolean deterministicCounterexamples)¶: Controls whether the verification will be guaranteed to generate counterexamples deterministically. This means that the same input will always give the same result. Note that enabling this may increase verification time.