306 Lines

testcase(no_yesterday_in_start,not(yesterday(true)),[root],model(_,_)).

testcase(simple_until,
    finally(and(ap(start),finally(ap(end)))),
    [10],
    model(_,_)).

testcase(trivial_false_globally,
    not(globally(ap(never))),
    [10],
    model([atom(10,_,none)],no_loop)).

testcase(partial_counter,
    finally(ap(target)),
    [20],
    model(_,_)).

testcase(partial_incomplete,not(F),Inits,incomplete) :-
    testcase(partial_counter,F,Inits,_).

testcase(exception,F,[40],exception(testexception)) :-
    testcase(partial_counter,F,_,_).

testcase(finally_loop,not(finally(or(ap(final),not(next(true))))),[50],
    model([atom(50,_,t01),atom(51,_,t14),atom(54,_,t45),atom(55,_,t54)],loop(2))).

testcase(finally,not(finally(ap(final))),[60],
    model([atom(60,_,t01),atom(61,_,t13),atom(63,_,none)],deadlock)).

testcase(ticket_3187a,
    not(implies(implies(globally(finally(ap(a_enabled))),
    globally(finally(action(is_a)))),
    finally(action(is_c)))),
    [70],
    model(_,_)).

testcase(ticket_3187b,Formula,[71], model(_,_)) :-
    testcase(ticket_3187a,Formula,_,_).

testcase(ticket_3187_simplified,
    not(implies(implies(globally(finally(ap(a_enabled))),
    globally(finally(action(is_a)))),
    finally(action(is_c)))),
    [80],
    model(_,_)).

testcase(ticket_3187_even_more_simplified,
    globally(finally(action(is_a))),
    [80],
    model(_,_)).

testcase(loopsize,
    not(globally(implies(action(start),next(finally(ap(goal)))))),
    [90],
    model([atom(90,_,t90),
    atom(91,_,t91),
    atom(93,_,t93),
    atom(94,_,t94),
    atom(95,_,t95)],
    loop(3))).

testcase/5

testltlc/0

trans/4

update/5

Determinacy Checker

Determinacy Checker:

* Non-determinate: user:file_search_path/2 (clause 1)
* This predicate is multifile, and this clause has no cut.
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_enter_debugger_upon_error,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_use_timer,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(no_terminal_colors,true)
! warning: predicate user:file_search_path/2 is dynamic.
! Some nondeterminism may have been missed.
! Add (or move) the directive
! :- dynamic user:file_search_path/2 .
! near the top of this file.
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_release,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_avl_custom,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_core_only,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_flag,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(plspec_patch_libraries,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_debug_flag,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_release,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(error_manager) does not exist
! goal: absolute_file_name(probsrc(error_manager),_69617,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xml_prob.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(debug) does not exist
! goal: absolute_file_name(probsrc(debug),_67953,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/xml_prob.pl')])
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_profile,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_src_profile,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_safe_mode,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_core_only,true)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(prob_myheap,false)
! Existence error in user:environ/2
! procedure user:environ/2 does not exist
! goal: user:environ(disable_chr,true)
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools_strings) does not exist
! goal: absolute_file_name(probsrc(tools_strings),_48593,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/pathes_lib.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file extension('counter/counter') does not exist
! goal: absolute_file_name(extension('counter/counter'),_17751,[access(exist),file_type(source),relative_to('/builds/stups/prob/prolog_doc_gen/prolog-Doc/prob_prolog/src/error_manager.pl')])
* Non-determinate: testltlc:testcase/5 (clause 1)
* Indexing cannot distinguish this from clause 2.
* Non-determinate: testltlc:trans/4 (clause 2)
* Indexing cannot distinguish this from clause 3.
* Non-determinate: testltlc:trans/4 (clause 7)
* Indexing cannot distinguish this from clause 8.
* Non-determinate: testltlc:trans/4 (clause 10)
* Indexing cannot distinguish this from clause 11.
* Non-determinate: testltlc:trans/4 (clause 14)
* Indexing cannot distinguish this from clause 15.
* Non-determinate: testltlc:trans/4 (clause 18)
* Indexing cannot distinguish this from clause 19.
* Non-determinate: testltlc:trans/4 (clause 19)
* Indexing cannot distinguish this from clause 20.
* Non-determinate: testltlc:trans/4 (clause 25)
* Indexing cannot distinguish this from clause 26.
* Non-determinate: testltlc:trans/4 (clause 27)
* Indexing cannot distinguish this from clause 28.
* Non-determinate: testltlc:trans/4 (clause 29)
* Indexing cannot distinguish this from clause 30.
* Non-determinate: testltlc:trans/4 (clause 38)
* Indexing cannot distinguish this from clause 39.
* Non-determinate: testltlc:trans/4 (clause 42)
* Indexing cannot distinguish this from clause 43.
* Non-determinate: testltlc:trans/4 (clause 45)
* Indexing cannot distinguish this from clause 46.

Name: RECURSIVE_CALL/3	Module: testltlc
Name: !
Name: =/2
Name: member/2
Name: ->/3

Name: RECURSIVE_CALL/3	Module: testltlc
Name: is/2
Name: show_atom/1	Module: testltlc
Name: show_loop/2	Module: testltlc

Name: nl
Name: write/1
Name: trans/4	Module: testltlc
Name: ->/3

Name: write/1
Name: !
Name: >/2
Name: =/2
Name: </2

Name: nl
Name: print/1
Name: true
Name: =/2
Name: ->/3
Name: format/2
Name: call/2
Name: catch/3
Name: testcase/5	Module: testltlc
Name: ltlc_init	Module: foo_error

testltlc

prob_prolog/extensions/ltlc/test_ltlc.pl

Modules

Predicates of testltlc

Module Information

306 Lines

18 Predicates

Imported Modules: ltlc lists

1 Exports

0 specified Imports

Predicates:

:/2

combineverdict/3

evalprops/3

fairness/2

node/2

show/1

show2/3

show_atom/1

show_loop/2

test/2

test_scc/2

testall/2

testcallback/5

testcase/4

testcase/5

testltlc/0

trans/4

update/5

Determinacy Checker:

Name: combineverdict/3	Module: testltlc
Name: RECURSIVE_CALL/2	Module: testltlc
Name: test/2	Module: testltlc

Name: findall/3
Name: evalprops/3	Module: testltlc
Name: throw/1
Name: =/2
Name: ->/3
Name: fail
Name: node/2	Module: testltlc