NotSerializableException when saving a type checked specification through the bundled version of VDMJ

donbex commented 2 years ago

Description

Our Gradle plugin leverages the Overture engine to programmatically animate a specification. As part of the process, it saves a copy of parsed and type checked specifications using the -o argument of the VDMJ class: https://github.com/overturetool/overture/blob/8e73876ae1e259b041db9a11afc7f8b93c385fa6/core/interpreter/src/main/java/org/overture/interpreter/VDMJ.java#L146-L159

However, certain specifications parse and type check correctly, but raise a "cannot write" error due to a NotSerializableException on org.overture.typechecker.assistant.TypeCheckerAssistantFactory.

Steps to Reproduce

Download an unpack the attached test.tar.gz
Run VDMJ on the Test.vdmsl specification file, using the -o option. For example, assuming Overture was downloaded to Maven Local:

$ java -cp /Users/alessandro.pezzoni/.m2/repository/org/overturetool/core/interpreter/3.0.2/interpreter-3.0.2.jar:/Users/alessandro.pezzoni/.m2/repository/org/overturetool/core/typechecker/3.0.2/typechecker-3.0.2.jar:/Users/alessandro.pezzoni/.m2/repository/org/overturetool/core/ast/3.0.2/ast-3.0.2.jar:/Users/alessandro.pezzoni/.m2/repository/org/overturetool/core/parser/3.0.2/parser-3.0.2.jar org.overture.interpreter.VDMJ -vdmsl -o test.lib Test.vdmsl

Expected behavior: The specification is parsed, type checked, and saved into the file test.lib.

Actual behavior: The specification is parsed and type checked correctly, but saving fails.

Parsed 1 module in 0.06 secs. No syntax errors
Warning 5000: Definition 'TestAdd' not used in 'Test' (Test.vdmsl) at line 12:3
Type checked 1 module in 0.054 secs. No type errors and 1 warning
Cannot write test.lib: org.overture.typechecker.assistant.TypeCheckerAssistantFactory

Reproduces how often: Always.

Versions

Overture version 3.0.2, OpenJDK version 17.0.2 (also tested with version 11), MacOS Monterey version 12.2.1.

Additional Information

The expected behaviour is observed with Overture version 2.6.4.

Interestingly, the -o option was removed from VDMJ itself: https://github.com/nickbattle/vdmj/issues/59

nickbattle commented 2 years ago

The -o option was originally added to VDMJ a long time ago in the hope that a serialized copy of the AST/TC tree could be loaded (deserialized from disk) faster than it could be re-created from the sources. Surprisingly, this turned out not to be the case, or at least any performance advantage was minimal.

The feature was removed in VDMJ version 4 when the "ClassMapper" was introduced to separate the AST, TC, IN, PO trees internally - although an individual tree could be serialized, you would need all of them (and in future, more) to be complete. Given the lack of performance advantage, it seemed best to remove it.

But in Overture, the feature may still work. If it fails in cases like this, it will be because the class concerned does not implement the Serializable interface (which requires a serial number declaration as well).

Assuming the feature does work (it may not!) the simple fix would be to add Serialize to TypeCheckerAssistantFactory. If this does not work however, I would recommend removing the feature, which just involves the command line option and some changes in the top level classes (VDMJ and the TypeChecker, from memory).

nickbattle commented 2 years ago

With Serialized added, the test example included does save and re-load a "lib" file:

Parsed 1 module in 0.095 secs. No syntax errors and 1 warning
Type checked 1 module in 0.075 secs. No type errors and 1 warning
Saved 1 module to test.lib in 0.078 secs.
Initialized 1 module in 0.047 secs. 
Interpreter started
> 

Loaded 1 module from test.lib in 0.144 secs
Initialized 1 module in 0.128 secs. 
Interpreter started
>

I'll push the change to the ncb/development branch.

overturetool / overture