Merge pull request #296 from tnelson/dev

[minor] test messages, Sterling menu filtering, fix

e2e/README.md

@@ -0,0 +1,5 @@
+# Forge models for end-to-end testing
+
+These models aren't meant to illustrate any particular concept, but rather are used for 
+end-to-end testing of the Sterling<->Forge<->Solver workflow. They may use unusual syntax,
+unsafe features, etc. 

e2e/fail_assertion.frg

@@ -0,0 +1,16 @@
+#lang forge
+
+option no_overflow true // disallow integer overflow
+
+sig Pigeon {location: one Pigeonhole}
+sig Pigeonhole {}
+
+pred some_roommates {
+    some disj p1, p2: Pigeon | p1.location = p2.location
+}
+-- This should pass; we don't expect Sterling to open at all.
+assert {#Pigeon > #Pigeonhole} is sufficient for some_roommates
+-- This should fail; we expect Sterling to open with **only one command**,
+-- and for the instance to auto-load. **The evaluator should be usable**.
+assert {#Pigeon >= #Pigeonhole} is sufficient for some_roommates
+

e2e/failing_decls_example.frg

@@ -0,0 +1,21 @@
+#lang forge
+
+option no_overflow true // disallow integer overflow
+
+sig Pigeon {location: one Pigeonhole}
+sig Pigeonhole {}
+
+pred some_roommates {
+    some disj p1, p2: Pigeon | p1.location = p2.location
+}
+
+// This fails because the instance given violates the type definitions
+// The solver yields unsat, so Sterling should not open.
+example threePigeons is {some_roommates} for {
+    Pigeon = `Pigeon0 + `Pigeon1 + `Pigeon2
+    Pigeonhole = `Pigeonhole0 + `Pigeonhole1
+    // This violates the type declarations:
+    location = `Pigeon0 -> (`Pigeonhole0 + `Pigeonhole1) +
+               `Pigeon1 -> `Pigeonhole0 +
+               `Pigeon2 -> `Pigeonhole0 
+}

e2e/failing_example.frg

@@ -0,0 +1,19 @@
+#lang forge
+
+option no_overflow true // disallow integer overflow
+
+sig Pigeon {location: one Pigeonhole}
+sig Pigeonhole {}
+
+pred some_roommates {
+    some disj p1, p2: Pigeon | p1.location = p2.location
+}
+
+// This fails. Since the solver has yielded unsat, Sterling shouldn't open.
+example threePigeons is {not some_roommates} for {
+    Pigeon = `Pigeon0 + `Pigeon1 + `Pigeon2
+    Pigeonhole = `Pigeonhole0 + `Pigeonhole1
+    location = `Pigeon0 -> `Pigeonhole0 +
+               `Pigeon1 -> `Pigeonhole0 +
+               `Pigeon2 -> `Pigeonhole1 
+}

e2e/passing_example.frg

@@ -0,0 +1,18 @@
+#lang forge
+
+option no_overflow true // disallow integer overflow
+
+sig Pigeon {location: one Pigeonhole}
+sig Pigeonhole {}
+
+pred some_roommates {
+    some disj p1, p2: Pigeon | p1.location = p2.location
+}
+
+example threePigeons is some_roommates for {
+    Pigeon = `Pigeon0 + `Pigeon1 + `Pigeon2
+    Pigeonhole = `Pigeonhole0 + `Pigeonhole1
+    location = `Pigeon0 -> `Pigeonhole0 +
+               `Pigeon1 -> `Pigeonhole0 +
+               `Pigeon2 -> `Pigeonhole1 
+}

e2e/sat_pass_unsat_pass_2_runs.frg

@@ -0,0 +1,19 @@
+#lang forge
+
+option no_overflow true // disallow integer overflow
+
+sig Pigeon {location: one Pigeonhole}
+sig Pigeonhole {}
+
+pred some_roommates {
+    some disj p1, p2: Pigeon | p1.location = p2.location
+}
+test expect { 
+  -- This is satisfiable, and so should appear in the run menu.
+  not_vacuous: {#Pigeon > #Pigeonhole} is sat 
+  -- This is unsatisfiable, and so wouldn't be useful to visualize.
+  should_be_unsat: {Pigeon != Pigeon} is unsat 
+}
+
+see_principle_1: run {} for exactly 5 Pigeon, exactly 4 Pigeonhole
+see_principle_2: run {} for exactly 4 Pigeon, exactly 3 Pigeonhole

forge/examples/lights_puzzle/ring_of_lights.frg

@@ -2,6 +2,7 @@
 
 option run_sterling "lights.js"
 
+
 /*
   When using the custom vis script, remember to click "Run" after
   asking for a new trace or config! (the script doesn't re-run automatically)

forge/info.rkt

@@ -69,6 +69,6 @@
                               #rx"tests/forge-core/*"
                               #rx"tests/forge-functional/*"
                               "tests/error/"
-                              #rx"domains/abac/tests/*"
+                              #rx"domains/abac/*"
                               #rx"domains/crypto/examples/*"
                               "OLD"))

forge/pardinus-cli/server/kks.rkt

@@ -19,12 +19,12 @@
 (define server-name "Pardinus")
 
 (provide start-server) ; stdin stdout)
-(define (start-server [solver-type 'stepper] [solver-subtype 'default])
+(define (start-server [solver-type 'stepper] [solver-subtype 'default] [java-exe #f])
   (when (>= (get-verbosity) VERBOSITY_HIGH)
     (printf "Starting ~a server.~n" server-name))
   (define kks (new server%
                    [name server-name]
-                   [initializer (thunk (pardinus-initializer solver-type solver-subtype))]))
+                   [initializer (thunk (pardinus-initializer solver-type solver-subtype java-exe))]))
   (send kks initialize)
   (define stdin-val (send kks stdin))
   (define stderr-val (send kks stderr))

forge/pardinus-cli/server/pardinus-server.rkt

@@ -10,7 +10,7 @@
 
 (define-runtime-path pardinus (build-path ".."))
 
-(define (pardinus-initializer solver-type solver-subtype)
+(define (pardinus-initializer solver-type solver-subtype java-exe)
   (unless (member solver-type '(incremental stepper))
     (raise (format  "Invalid solver type: ~a" solver-type)))
 
@@ -19,15 +19,17 @@
                     (filter (curry regexp-match #rx".+\\.jar")
                             (directory-list pardinus/jar)))]
          [windows? (equal? (system-type) 'windows)]
-         [java (find-executable-path (if windows? "java.exe" "java"))]
+         [java (if (and java-exe (> (string-length java-exe) 0))
+                   (build-path java-exe)
+                   (find-executable-path (if windows? "java.exe" "java")))]
          [path-separator (if windows? ";" ":")]
          [cp (foldl string-append "" (add-between (map path->string jars) path-separator))]
          ;[lib (path->string (build-path pardinus/jni (case (system-type)
                                                      ;[(macosx) "darwin_x86_64"]
                                                      ;[(unix) "linux_x86_64"]
                                                      ;[(windows) "win_x86_64"])))]
          ;[-Djava.library.path (string-append "-Djava.library.path=" lib)]
-         [error-out (build-path (find-system-path 'home-dir) "error-output.txt")])
+         [error-out (build-path (find-system-path 'home-dir) "forge-pardinus-error-output.txt")])
 
     (when (> (get-verbosity) VERBOSITY_LOW)        
       (printf "  Starting solver process. subtype: ~a~n" solver-subtype))
@@ -37,6 +39,9 @@
                                      [(equal? solver-subtype 'temporal) "-temporal"]
                                      [(equal? solver-subtype 'default) ""]
                                      [else (error (format "Bad solver subtype: ~a" solver-subtype))]))
+
+    (unless (file-exists? java)
+      (raise-user-error 'start-server "Could not find a Java executable. Given or inferred location was: ~a. Type was: ~a" java (file-or-directory-type java)))
 
     (when (>= (get-verbosity) VERBOSITY_HIGH)        
       (printf "  Subprocess invocation information: ~a~n"

forge/send-to-solver.rkt

@@ -190,7 +190,9 @@
         'stepper ; always a stepper problem (there is a "next" button)
         ; 'default, 'temporal, or 'target (tells Pardinus which solver to load,
         ;  and affects parsing so needs to be known at invocation time)
-        (get-option run-spec 'problem_type))]
+        (get-option run-spec 'problem_type)
+        ; control version of java used (by path string)
+        (get-option run-spec 'java_exe_location))]
 
       [else (raise (format "Invalid backend: ~a" backend))]))
 

forge/server/forgeserver.rkt

@@ -71,7 +71,9 @@
     (define returned-instance (tree:get-value current-tree))
     (set-box! (Run-last-sterling-instance the-run) returned-instance)
     returned-instance)
-  (define (get-next-instance [next-mode 'P])    
+  (define (get-next-instance [next-mode 'P])
+    (when (@>= (get-verbosity) VERBOSITY_LOW)
+      (printf "Solving for next instance.~n"))
     (set! current-tree (tree:get-child current-tree next-mode))
     (set! curr-datum-id (+ curr-datum-id 1))
     ; get-current-instance updates the Run's last sterling instance cursor when called
@@ -190,26 +192,12 @@
      #:port (get-option the-run 'sterling_port) #:confirmation-channel chan))
 
   (define port (async-channel-get chan))
-  (cond [(string? port)
-         (displayln "NO PORTS AVAILABLE. Unable to start web server and Sterling visualizer.")]
-        [(equal? 'off (get-option the-run 'run_sterling))
-         (void)]
-        [else
-         ; Attempt to open a browser to the Sterling index.html, with the proper port
-         ; If this cannot be opened for whatever reason, keep the server open but print
-         ; a warning, allowing the user a workaround.
-         (with-handlers ([exn?
-                          (lambda (e) (printf "Racket could not open a browser on your system; you may be able manually navigate to this address, which is where Forge expects Sterling to load:~n  ~a~n"
-                                              (string-append (path->string sterling-path) "?" (number->string port))))])
-           (send-url/file sterling-path #f #:query (number->string port)))
-
-         (printf "Sterling running. Hit enter to stop service.\n")
-         (when (> (get-verbosity) VERBOSITY_LOW)
-           (printf "Using port: ~a~n" (number->string port)))
-         (flush-output)
-         (void (read-char))
-         ; Once a character is read, stop the server
-         (stop-service)]))
+  (when (string? port)
+    (printf "NO PORTS AVAILABLE. Could not start provider server.~n"))
+
+  ; Now, serve the static sterling website files (this will be a different server/port).
+  (unless (equal? 'off (get-option state-for-run 'run_sterling))
+    (serve-sterling-static #:provider-port port)))
 
 (define (make-sterling-data xml id run-name temporal? not-done? [old-id #f])
   (jsexpr->string
@@ -249,15 +237,15 @@
          'payload (hash 'id (->string id)
                         'result (->string result)))))
 
-(define/contract (make-sterling-meta defined-run-names)
+(define/contract (make-sterling-meta included-run-names)
   (-> (listof symbol?) string?)
   (jsexpr->string	
    (hash 'type "meta"
          'version 1
          'payload (hash 'name "Forge"
                         'evaluator #t
                         'views (list "graph" "table" "script")
-                        'generators (map ->string defined-run-names)))))
+                        'generators (map ->string included-run-names)))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Infrastructure for starting up sterling in "command selector" mode
@@ -268,6 +256,17 @@
   (define runmap (State-runmap curr-state))
   (define defined-run-names (hash-keys runmap))
 
+  ; Filter out runs that are not useful to visualize, like tests that failed due to unsat.
+  ; ASSUME: non-tests (e.g., `run`) won't have been invoked yet.
+  ; It is *VITAL* that `or` short-circuits, since Sat? will invoke the solver if needed.
+  (define useful-run-names (filter
+                            (lambda (rn)
+                              (define this-run (hash-ref runmap rn))
+                              ; Include if this run hasn't been solved yet, or if it's solved and sat.
+                              (or (not (tree:is-evaluated? (Run-result this-run)))
+                                  (is-sat? this-run)))
+                            defined-run-names))
+
   ; Assumption: if Sterling is the source of instance requests, there will be no
   ; instance requests seen from any other sources.
 
@@ -278,7 +277,7 @@
 
   (when (> (get-verbosity) VERBOSITY_LOW)
     (printf "Starting Sterling in command-selection mode...~n")
-    (printf "Available commands: ~a~n" defined-run-names))
+    (printf "Available commands: ~a~n" useful-run-names))
 
   (define (send-to-sterling m #:connection connection)
     (when (@>= (get-verbosity) VERBOSITY_STERLING) 
@@ -356,6 +355,9 @@
 
        ; Get the next instance of this run's lazy result tree. Advance the tree pointer.
        (define (get-next-instance [next-mode 'P])
+         (when (@>= (get-verbosity) VERBOSITY_LOW)
+           (printf "Solving for next instance.~n"))
+
          (define next-tree (get-next-tree next-mode))
          (set! curr-datum-id (+ curr-datum-id 1))
 
@@ -421,7 +423,8 @@
        ;;(define xml (get-xml inst))
        ;;(define response (make-sterling-data xml id name temporal?))
        ;;(send-to-sterling response #:connection connection)
-       (printf "Ignoring Sterling 'data' request...~n")
+       (when (@>= (get-verbosity) VERBOSITY_STERLING)
+         (printf "Ignoring Sterling 'data' request...~n"))
        ]
       [(equal? (hash-ref json-m 'type) "eval")
        ; A message requesting that the provider evaluate some expression
@@ -475,7 +478,7 @@
       [(equal? (hash-ref json-m 'type) "meta")
        ; A message requesting data about the data provider, such as the provider's
        ; name and the types of views it supports. Respond in turn with a meta message.
-       (send-to-sterling (make-sterling-meta defined-run-names) #:connection connection)]      
+       (send-to-sterling (make-sterling-meta useful-run-names) #:connection connection)]      
       [else
        (send-to-sterling "BAD REQUEST" #:connection connection)
        (raise-forge-error
@@ -508,5 +511,8 @@
     (printf "NO PORTS AVAILABLE. Could not start provider server.~n"))
 
   ; Now, serve the static sterling website files (this will be a different server/port).
-  (unless (equal? 'off (get-option curr-state 'run_sterling))
-    (serve-sterling-static #:provider-port port)))
+  (unless (or (equal? 'off (get-option curr-state 'run_sterling))
+              (empty? useful-run-names))
+    (serve-sterling-static #:provider-port port))
+  (when (empty? useful-run-names)
+    (printf "There was nothing useful to visualize: all commads were already executed and produced no instances.~n")))

forge/server/serve-sterling-static.rkt

@@ -57,7 +57,7 @@
                                               e))])
            (send-url sterling-url))
 
-         (printf "Opening Forge menu in Sterling (static server port=~a). Press enter to stop Forge.~n" port)
+         (printf "Opening Forge menu in Sterling (static server port=~a). Press enter to stop Forge (or click 'Stop' in VSCode).~n" port)
 
          (flush-output)
          ; On Windows, this blocks all Racket threads, which delays output until input is read.

forge/shared.rkt

@@ -149,7 +149,7 @@
           (set-box! success? (apply system* exe cmd*))))))
   (if (unbox success?)
     str
-    (raise-user-error 'shell "failed to apply '~a' to arguments '~a'" exe cmd*)))
+    (raise-user-error 'shell "failed to apply '~a' to arguments '~a': got ~a" exe cmd* (unbox success?))))
 
 ;; --- timing