Cannot run PO Generation

[wavy-n1c9]

Ive installed VDM VSCode to VSCODE 1.106 version.
Created vdmsl file, but i dont have a button to run POG

[nickbattle]

How did you open the file? The extension is "project oriented" and is expecting you to open a folder containing the source(s), rather than opening one source file. Can you try opening the folder that contains the source (preferably with nothing else in there!)

[wavy-n1c9]

Thank you for answer, but I opened as folder on the screenshot, and tried few more times, didnt help

[nickbattle]

Hmm, okay. Can you have a look at the System Requirements, here?. It may just be that your VSCode version is quite old? You need >1.49, as well as a compatible Java.

[nickbattle]

Incidentally, if you want to do serious work with POs, I would recommend the latest VDM-VSCode VSIX. This has many improvements, including the latest version of QuickCheck, that will help try to find counterexamples.

[wavy-n1c9]

As I wrote before my vscode is 1.106 version

[wavy-n1c9]

Do you have any guidance for usage this tool?

Incidentally, if you want to do serious work with POs, I would recommend the latest VDM-VSCode VSIX. This has many improvements, including the latest version of QuickCheck, that will help try to find counterexamples.

[nickbattle]

Can you try enabling the logging in your settings:

"vdm-vscode.server.logLevel": "all"

That should write logging into (saomething like) /home/nick/.config/Code/logs/20251207T141525/window2/exthost/overturetool.vdm-vscode. My guess is that something is failing at startup, when you open the folder.

There is information about QuickCheck here, though you would normally run it via the GUI. But first we have to sort out why you can't get the extension working...

[wavy-n1c9]

Here is all logs i got

2025-12-07 17:56:01.718 [info] Extension host with pid 18436 started
2025-12-07 17:56:01.718 [info] Skipping acquiring lock for c:\Users\koles\AppData\Roaming\Code\User\workspaceStorage\0064420c7df35cb90e071f36b697e73e.
2025-12-07 17:56:01.780 [info] ExtensionService#_doActivateExtension vscode.github-authentication, startup: false, activationEvent: 'onAuthenticationRequest:github'
2025-12-07 17:56:01.820 [info] ExtensionService#_doActivateExtension vscode.emmet, startup: false, activationEvent: 'onLanguage'
2025-12-07 17:56:01.842 [info] ExtensionService#_doActivateExtension overturetool.vdm-vscode, startup: false, activationEvent: 'onLanguage:vdmsl'
2025-12-07 17:56:01.983 [info] ExtensionService#_doActivateExtension vscode.git-base, startup: true, activationEvent: '*', root cause: vscode.git
2025-12-07 17:56:02.043 [info] ExtensionService#_doActivateExtension vscode.git, startup: true, activationEvent: '*'
2025-12-07 17:56:02.110 [info] ExtensionService#_doActivateExtension vscode.github, startup: true, activationEvent: '*'
2025-12-07 17:56:02.258 [info] Eager extensions activated
2025-12-07 17:56:02.302 [info] ExtensionService#_doActivateExtension vscode.debug-auto-launch, startup: false, activationEvent: 'onStartupFinished'
2025-12-07 17:56:02.306 [info] ExtensionService#_doActivateExtension vscode.merge-conflict, startup: false, activationEvent: 'onStartupFinished'
2025-12-07 17:56:02.602 [info] ExtensionService#_doActivateExtension vscode.terminal-suggest, startup: false, activationEvent: 'onTerminalShellIntegration:*'
2025-12-07 17:56:18.028 [info] Extension host terminating: renderer closed the MessagePort
2025-12-07 17:56:18.041 [error] TypeError: Cannot read properties of undefined (reading 'getAllClients')
	at Object.<anonymous> (c:\Users\koles\.vscode\extensions\overturetool.vdm-vscode-1.5.1\dist\extension.js:1:605346)
	at Generator.next (<anonymous>)
	at c:\Users\koles\.vscode\extensions\overturetool.vdm-vscode-1.5.1\dist\extension.js:1:600826
	at new Promise (<anonymous>)
	at n (c:\Users\koles\.vscode\extensions\overturetool.vdm-vscode-1.5.1\dist\extension.js:1:600571)
	at t.deactivate (c:\Users\koles\.vscode\extensions\overturetool.vdm-vscode-1.5.1\dist\extension.js:1:605295)
	at kX.eb (file:///c:/Users/koles/AppData/Local/Programs/Microsoft%20VS%20Code/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:118:11850)
	at file:///c:/Users/koles/AppData/Local/Programs/Microsoft%20VS%20Code/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:118:10000
	at Array.map (<anonymous>)
	at kX.$ (file:///c:/Users/koles/AppData/Local/Programs/Microsoft%20VS%20Code/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:118:9988)
	at kX.terminate (file:///c:/Users/koles/AppData/Local/Programs/Microsoft%20VS%20Code/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:118:10231)
	at nN.terminate (file:///c:/Users/koles/AppData/Local/Programs/Microsoft%20VS%20Code/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:120:914)
	at Fs (file:///c:/Users/koles/AppData/Local/Programs/Microsoft%20VS%20Code/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:402:10411)
	at MessagePortMain.<anonymous> (file:///c:/Users/koles/AppData/Local/Programs/Microsoft%20VS%20Code/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:402:6949)
	at MessagePortMain.emit (node:events:519:28)
	at MessagePortMain._internalPort.emit (node:electron/js2c/utility_init:2:2949)
2025-12-07 17:56:18.041 [info] Extension host with pid 18436 exiting with code 0
2025-12-07 17:56:18.700 [info] Extension host with pid 11420 started
2025-12-07 17:56:18.700 [info] Skipping acquiring lock for c:\Users\koles\AppData\Roaming\Code\User\workspaceStorage\0064420c7df35cb90e071f36b697e73e.
2025-12-07 17:56:18.713 [info] ExtensionService#_doActivateExtension vscode.terminal-suggest, startup: false, activationEvent: 'onTerminalShellIntegration:*'
2025-12-07 17:56:18.778 [info] ExtensionService#_doActivateExtension vscode.github-authentication, startup: false, activationEvent: 'onAuthenticationRequest:github'
2025-12-07 17:56:18.803 [info] ExtensionService#_doActivateExtension vscode.emmet, startup: false, activationEvent: 'onLanguage'
2025-12-07 17:56:18.880 [info] ExtensionService#_doActivateExtension vscode.git-base, startup: true, activationEvent: '*', root cause: vscode.git
2025-12-07 17:56:18.906 [info] ExtensionService#_doActivateExtension vscode.git, startup: true, activationEvent: '*'
2025-12-07 17:56:18.959 [info] ExtensionService#_doActivateExtension vscode.github, startup: true, activationEvent: '*'
2025-12-07 17:56:19.094 [info] Eager extensions activated
2025-12-07 17:56:19.097 [info] ExtensionService#_doActivateExtension vscode.debug-auto-launch, startup: false, activationEvent: 'onStartupFinished'
2025-12-07 17:56:19.101 [info] ExtensionService#_doActivateExtension vscode.merge-conflict, startup: false, activationEvent: 'onStartupFinished'
2025-12-07 17:56:20.337 [info] ExtensionService#_doActivateExtension overturetool.vdm-vscode, startup: false, activationEvent: 'onLanguage:vdmsl'

[nickbattle]

I'm after a different log. I may not have given the correct JSON settings - can you try this (put this in .vscode/settings.json within the source folder):

{
	"vdm-vscode.server.development.experimentalServer": false,
	"vdm-vscode.server.logLevel": "all",
	"vdm-vscode.trace.server": "verbose"
}

That should create a file called .../window1/exthost/overturetool.vdm-vscode/TestSL_lang_server.log. It will look something like this:

16:21:32.542: [INFO][1] Logging level set to ALL
16:21:32.672: [INFO][1] LSP VDM_SL Server connecting to port 42109
16:21:32.681: [INFO][20] DAP VDM_SL Server listening on port 34569
16:21:32.700: [INFO][1] Created PluginRegistry
16:21:32.701: [INFO][1] Created EventHub
16:21:32.701: [INFO][1] Created MessageHub
...

If it's too large to attach to this issue, you can email me at nick.battle@gmail.com.

[nickbattle]

Alternatively, could you ZIP the project (the folder and the source within, together with any .vscode files)? I can try it here.

Incidentally, what version of Java are you using?

[wavy-n1c9]

hello, i am currently got java

java version "1.8.0_471"
Java(TM) SE Runtime Environment (build 1.8.0_471-b09)
Java HotSpot(TM) 64-Bit Server VM (build 25.471-b09, mixed mode)

and i got next issue

Exception in thread "main" 
java.lang.UnsupportedClassVersionError: lsp/LSPServerSocket has been compiled by a more recent version of the Java Runtime (class file version 55.0), this version of the Java Runtime only recognizes class file versions up to 52.0
	at java.lang.ClassLoader.defineClass1(Native Method)
	at java.lang.ClassLoader.defineClass(Unknown Source)
	at java.security.SecureClassLoader.defineClass(Unknown Source)
	at java.net.URLClassLoader.defineClass(Unknown Source)
	at java.net.URLClassLoader.access$100(Unknown Source)
	at java.net.URLClassLoader$1.run(Unknown Source)
	at java.net.URLClassLoader$1.run(Unknown Source)
	at java.security.AccessController.doPrivileged(Native Method)
	at java.net.URLClassLoader.findClass(Unknown Source)
	at java.lang.ClassLoader.loadClass(Unknown Source)
	at sun.misc.Launcher$AppClassLoader.loadClass(Unknown Source)
	at java.lang.ClassLoader.loadClass(Unknown Source)
	at sun.launcher.LauncherHelper.checkAndLoadMain(Unknown Source)

[nickbattle]

Ah, now this is making more sense. You need Java later than version 11. Version 8 is really very old now.

Can you upgrade and let me know if that gets you further? (I usually test with versions 11 and 21).

[nickbattle]

Do you have any guidance for usage this tool?

Incidentally, if you want to do serious work with POs, I would recommend the latest VDM-VSCode VSIX.

Working with the VDM extension itself is covered by the wiki. But hopefully it's fairly intuitive.

Guidance about how to write formal specifications is much harder to give. There is some very introductory material on the VDMJ wiki -- see "VDMJ Help for Specifiers". VDMJ is the language engine that supports VDM-VSCode.

But beyond that, I would need to know more about what you hope to model in VDM. But that isn't something for this issue!

[nickbattle]

Did a Java upgrade fix this? (Or perhaps you're already on Xmas holiday!)