Undetected infinite multi-objective reward

[Chickenpowerrr]

The property multi(R{"inf"}min=? [ C ]) should obviously be infinite in the model below. However, the linear programming solver incorrectly reports a result of 0.0.

This seems to be the case since the constraint is not violated according to the code since it is not a maximising objective.

mdp

module infinite
    s : [0..1];
    [inf] s=0 -> true;
endmodule

rewards "inf" 
	[inf] true : 1;
endrewards

PRISM
=====

Version: 4.8.1
Date: Tue Oct 29 11:27:13 CET 2024
Hostname: LAPTOP-9DDD1OSE
Memory limits: cudd=1g, java(heap)=1g
Command line: prism infinite.nm -pf 'multi(R{"inf"}min=? [C])' -lp

Parsing model file "infinite.nm"...

Type:        MDP
Modules:     infinite
Variables:   s

1 property:
(1) multi(R{"inf"}min=? [ C ])

---------------------------------------------------------------------

Model checking: multi(R{"inf"}min=? [ C ])

Building model...

Computing reachable states...

Reachability (BFS): 1 iterations in 0.00 seconds (average 0.000000, setup 0.00)

Time for model construction: 0.008 seconds.

Type:        MDP
States:      1 (1 initial)
Transitions: 1
Choices:     1

Transition matrix: 5 nodes (2 terminal), 1 minterms, vars: 1r/1c/1nd
Total time for product construction: 0.0 seconds.

States:      1 (1 initial)
Transitions: 1
Choices:     1

Transition matrix: 5 nodes (2 terminal), 1 minterms, vars: 1r/1c/1nd

Prob0A: 1 iterations in 0.00 seconds (average 0.000000, setup 0.00)

yes = 0, no = 0, maybe = 1

Computing remaining probabilities...
Switching engine since only sparse engine currently supports this computation...
Engine: Sparse

0 Targets:

1 Rewards:
#0: Rmin=?

Building sparse matrix... [n=1, nc=1, nnz=1, k=1] [0.0 KB]
Creating vectors for yes... [0 x 0.0 KB]
Creating vector for maybe... [0.0 KB]
Creating vector for bottom end components... [0.0 KB]
Initial state index: 0
TOTAL: [0.0 KB]

Building LP problem...
Number of LP variables = 2
Adding extra constraints for bounded objectives...
computing max function for rewards ...
Setting objective...
Solving LP problem...
LP problem solution found; result is 0.000000

LP problem solved in 0.00 seconds (setup 0.00, lpsolve 0.00)

Value in the initial state: 0.0

Time for model checking: 0.004 seconds.

Result: 0.0