Next and Previous Operators

[BaileyFernandez]

(Moved from fork )

For anyone who might know what is going on, I am having some issues with examples.py and operators.py I defined two operators (Next and Previous) which I believe are syntactically correct, but the examples will not seem to print when I run the model checker on examples.py. I made sure to add both operators to "bimodal operators" at the end of operators.py . Here is the code for reference: `class NextOperator(syntactic.Operator): """Temporal operator that evaluates whether an argument holds at the "next" time in a history.

This operator implements the "Next it will be the case that..." It evaluates
whether its argument is true at the "next" time in a history. 

Key Properties:
    - Evaluates the truth value of a formula and the successive time in a history.
    --Returns true if the formula is true at the next time. 
    --Returns false if the formula is false at the next time. 
    - Vacuously true if there is no "next" time. 
    - Only considers times within the valid interval for the current world

Methods:
    true_at: Returns true if argument holds at the next time
    false_at: Returns true if argument fails at the next time
    find_truth_condition: Computes temporal profiles for all worlds
    print_method: Displays evaluation across different time points

Example:
    If p means "it's raining", then ∘p means "it will rain at the next time"
    . More colloquially, it might mean "it will rain tomorrow." 
"""

name = "\\Next"
arity = 1

def true_at(self, argument, eval_world, eval_time):
    """Returns true if argument is true at the time of evaluation plus one. 
    
    Args:
        argument: The argument to apply the next operator to
        eval_world: The world ID for evaluation context
        eval_time: The time for evaluation context
    """
    semantics = self.semantics
    time = z3.Int('next_true_time')

    #define "next time" variable
    next_time = eval_time + 1

    return z3.And(
            
        #Time is within the valid range for this world's interval
        semantics.is_valid_time_for_world(eval_world, next_time),

        #Formula is true at next time in world 
        semantics.true_at(argument, eval_world, next_time)
        )
    

def false_at(self, argument, eval_world, eval_time):
    """Returns true if argument is false at the "next" time in the world's time interval. 
    
    Args:
        argument: The argument to apply the next operator to
        eval_world: The world ID for evaluation context
        eval_time: The time for evaluation context
    """
    semantics = self.semantics
    time = z3.Int('next_false_time')
    next_time = eval_time + 1

    return z3.And(
            # Time is within the valid range for this world's interval
            semantics.is_valid_time_for_world(eval_world, next_time),

            #Formula is false at the next time in world 
            semantics.false_at(argument, eval_world, next_time),
        )

def find_truth_condition(self, argument, eval_world, eval_time):
    """Gets truth-condition for 'Next it will be the case that'.
    
    Args:
        argument: The argument to apply the next operator to
        eval_world: The world ID for evaluation context
        eval_time: The time for evaluation context
        
    Returns:
        dict: A dictionary mapping world_ids to (true_times, false_times) pairs,
             where a time is in the true_times if the argument is true in all
             past times and the time is in the false_times otherwise
             
    Raises:
        KeyError: If world_time_intervals information is missing for a world_id.
                 This follows the fail-fast philosophy to make errors explicit.
    """
    model_structure = argument.proposition.model_structure
    semantics = model_structure.semantics
    argument_extension = argument.proposition.extension
    truth_condition = {}
    
    # For any current_world with a temporal_profile of true and false times
    for current_world, temporal_profile in argument_extension.items():
        true_times, false_times = temporal_profile
        
        # Start with empty lists for past/future times
        new_true_times, new_false_times = [], []
        
        # Find the time_interval for the current_world
        start_time, end_time = semantics.world_time_intervals[current_world]
        time_interval = list(range(start_time, end_time + 1))
        
        # Calculate which times the argument always has been true
        for time_point in time_interval:

            # Check if there are any world_times strictly after this time_point
            has_future_times = any(any_time > time_point for any_time in time_interval)
            
            # If there are no future times in this world's interval, the Next operator is vacuously true
            if not has_future_times:
                new_true_times.append(time_point)
                continue
                
            # Find the next time from each time point 
            next_false_times=[
                any_time
                for any_time in false_times 
                if any_time==(time_point + 1)
                and any_time in time_interval 
            ]

            # If the argument is not false at the next time, consider it true now 
            if not next_false_times:
                # Add time_point to the new_true_times
                new_true_times.append(time_point)
            else:
                # Otherwise add time_point to the new_false_times
                new_false_times.append(time_point)
        
        # Store the results for this world_id
        truth_condition[current_world] = (new_true_times, new_false_times)

    # Return result dictionary
    return truth_condition

def print_method(self, sentence_obj, eval_point, indent_num, use_colors):
    """Print the sentence over all time points.
    
    Args:
        sentence_obj: The sentence to print
        eval_point: The evaluation point (world ID and time)
        indent_num: The indentation level
        use_colors: Whether to use colors in output
    """
    all_times = sentence_obj.proposition.model_structure.all_times
    self.print_over_times(sentence_obj, eval_point, all_times, indent_num, use_colors)

class PreviousOperator(syntactic.Operator): """Temporal operator that evaluates whether an argument holds at the "previous" time in a history.

This operator implements the "Previously it was the case that.." It evaluates
whether its argument is true at the "next" time in a history. 

Key Properties:
    - Evaluates the truth value of a formula and the previous time in a history.
    --Returns true if the formula is true at the previous time. 
    --Returns false if the formula is false at the previous time. 
    - Vacuously true if there is no "previous" time. 
    - Only considers times within the valid interval for the current world

Methods:
    true_at: Returns true if argument holds at the previous time
    false_at: Returns true if argument fails at the previous time
    find_truth_condition: Computes temporal profiles for all worlds
    print_method: Displays evaluation across different time points

Example:
    If p means "it's raining", then ∘p means "it will rain at the next time"
    . More colloquially, it might mean "it will rain tomorrow." 
"""

name = "\\Previous"
arity = 1

def true_at(self, argument, eval_world, eval_time):
    """Returns true if argument is true at the time of evaluation plus one. 
    
    Args:
        argument: The argument to apply the next operator to
        eval_world: The world ID for evaluation context
        eval_time: The time for evaluation context
    """
    semantics = self.semantics
    time = z3.Int('previous_true_time')

    #define "previous time" variable
    previous_time = eval_time - 1

    return z3.And(
            
        #Time is within the valid range for this world's interval
        semantics.is_valid_time_for_world(eval_world, previous_time),

        #Formula is true at previous time in world 
        semantics.true_at(argument, eval_world, previous_time)
        )
    

def false_at(self, argument, eval_world, eval_time):
    """Returns true if argument is false at the "next" time in the world's time interval. 
    
    Args:
        argument: The argument to apply the next operator to
        eval_world: The world ID for evaluation context
        eval_time: The time for evaluation context
    """
    semantics = self.semantics
    time = z3.Int('previous_false_time')
    previous_time = eval_time - 1

    return z3.And(
            # Time is within the valid range for this world's interval
            semantics.is_valid_time_for_world(eval_world, previous_time),

            #Formula is false at the previous time in world 
            semantics.false_at(argument, eval_world, previous_time),
        )

def find_truth_condition(self, argument, eval_world, eval_time):
    """Gets truth-condition for 'Previously it was the case that'.
    
    Args:
        argument: The argument to apply the previous operator to
        eval_world: The world ID for evaluation context
        eval_time: The time for evaluation context
        
    Returns:
        dict: A dictionary mapping world_ids to (true_times, false_times) pairs,
             where a time is in the true_times if the argument is true in all
             past times and the time is in the false_times otherwise
             
    Raises:
        KeyError: If world_time_intervals information is missing for a world_id.
                 This follows the fail-fast philosophy to make errors explicit.
    """
    model_structure = argument.proposition.model_structure
    semantics = model_structure.semantics
    argument_extension = argument.proposition.extension
    truth_condition = {}
    
    # For any current_world with a temporal_profile of true and false times
    for current_world, temporal_profile in argument_extension.items():
        true_times, false_times = temporal_profile
        
        # Start with empty lists for past/future times
        new_true_times, new_false_times = [], []
        
        # Find the time_interval for the current_world
        start_time, end_time = semantics.world_time_intervals[current_world]
        time_interval = list(range(start_time, end_time + 1))
        
        # Calculate which times the argument always has been true
        for time_point in time_interval:

            # Check if there are any world_times strictly before this time_point
            has_past_times = any(any_time < time_point for any_time in time_interval)
            
            # If there are no past times in this world's interval, the Previous operator is vacuously true
            if not has_past_times:
                new_true_times.append(time_point)
                continue
                
            # Find the next time from each time point 
            previous_false_times=[
                any_time
                for any_time in false_times 
                if any_time==(time_point -1)
                and any_time in time_interval 
            ]

            # If the argument is not false at the previous time, consider it true now 
            if not previous_false_times:
                # Add time_point to the new_true_times
                new_true_times.append(time_point)
            else:
                # Otherwise add time_point to the new_false_times
                new_false_times.append(time_point)
        
        # Store the results for this world_id
        truth_condition[current_world] = (new_true_times, new_false_times)

    # Return result dictionary
    return truth_condition`

[benbrastmckie]

This is great! The issue is to do with the number of arguments. Sentences should always be evaluated at eval_point where this is a dictionary consisting of the (in the case of this semantics) world and time (but could differ for other theories).

I'm just did some digging and this has exposed an issue in the bimodal semantics. I will fix that now and report back.

[benbrastmckie]

This has already been really helpful as this brought to light an issue in bimodal that I was missing before. I fixed the changes and so you should be able to get the patch by syncing your fork on GitHub, then pulling the most recent down locally from your fork. Since you directly changed the bimodal theory, there may be conflicts.

It is also worth mentioning before you go too far that it would probably be best to leave bimodal as it is and create a LTL_project from the bimodal theory so that you can compare to the bimodal theory when convenient. The easiest thing might be to save the files you changed in a backup folder and repeat the fork process, deleting the old fork from both GitHub and locally. Then generate a new bimodal project from within the theory_lib/ directory and then modify that theory to have the operators you defined (these are saved in the backup you stored at the beginning). That way there would be no risk of merge conflicts and you will have a local version of the bimodal semantics for comparison as you develop your theory.

Alternatively, if syncing your fork and pulling the changes I made works no problem, you can always look at the bimodal semantics in this repo if you need to compare. So that way you can stick with your current fork and keep editing the bimodal semantics as you have been. Both options should work, and maybe easiest to stick with your fork assuming the merge conflicts aren't too tricky (I don't think they should be).

One unrelated thought is that for LTL, you won't need worlds, just a single time line represented by the integers. This will simplify the semantics a lot, giving you a big performance bump. But I nevertheless think it is great to start with the operators that you are working on. Shouldn't take much more to get them working. They look great!

[benbrastmckie]

Here is an example of how the true_at method will go with the patched bimodal/ theory:

    def true_at(self, argument, eval_point):
        """Returns true if argument is true at the time of evaluation plus one. 
        
        Args:
            argument: The argument to apply the next operator to
            eval_world: The world ID for evaluation context
            eval_time: The time for evaluation context
        """
        semantics = self.semantics
        
        # Extract world and time from eval_point
        eval_world = eval_point["world"]
        eval_time = eval_point["time"]

        #define "next time" variable
        next_time = eval_time + 1
        next_point = {"world": eval_world, "time": next_time}

        return z3.And(
                
            #Time is within the valid range for this world's interval
            semantics.is_valid_time_for_world(eval_world, next_time),

            #Formula is true at next time in world 
            semantics.true_at(argument, next_point)
            )

[BaileyFernandez]

Hey Ben! Sorry for the later reply -- still working through patching the operators to fit the changes.

All of this sounds great! Regarding the bimodal, I actually thought it would be easiest to start with defining the LTL-like operators in the bimodal semantics -- kind of how you suggest them towards the end of the draft paper -- and then work on the semantics for LTL in a new project once I got them working. I thought this might work well for two reasons: i). for my own learning, it is comparatively similar to work within the already-defined semantics and then slowly transition into defining my own, ii). intellectually, I think that it would actually be interested to run the model-checker on how some of these opeartors interact with modality. Once I get "Until" and "Since" up and running, it might be nice to check how those interact with \Diamond. For instance, I would expect that there is a counter model to \Diamond (\metaA \Until \metaB) \MLModels\metaA \Until \Diamond(\metaB). But it would be nice to be able to use the model checker for these, because the \Until and \Since operators are complicated enough that I anticipate the proofs will be pretty grueling.

Would this kind of work flow make sense to you? My plan was
1). Define Next/Previous, Since/Until, and the novel Reichenbach inspired ones we came up with (PresentProg/PastProg) in the bimodal semantics.
2). Use that to reverse engineer an LTL-theory. The modal operators in that theory will just be \Always, \Eventually, and \Until. \Always and \Eventually are identical to \Future and \future from the bimodal semantics.
3). Check out some examples as I go.

Cheers
Bailey

[benbrastmckie]

Oh! That makes good sense. And yes, great to include new operators in the bimodal theory. In that case, you will need to sync your fork and pull changes from your fork. If you run into any problems let me know, but assuming that you have only been working in operators.py you should be safe.

[BaileyFernandez]

Hey Ben! Wanted to give you a quick shout. I am attaching a pseudo-codey version of "Until" I am working on. I had a quick question regarding how binary operators work. At one point in this code, I want to check for whether the right arg is true at an eval_point. I know how to get the eval_point, but I was not quite sure how to do the truth clause now that we have shifted to points instead of times/worlds. Did you have any suggestions for that?

Thank you so much! -

Best
Bailey (Code below)

` name = "\Until"
arity = 2

def true_at(self, leftarg, rightarg, eval_point):
    """Returns true if argument is true at all future times in this world's interval."""
    semantics = self.semantics
    
    # Extract world and time from eval_point
    eval_world = eval_point["world"]
    eval_time = eval_point["time"]

    #get ordered list of times in history
    start_time, end_time = semantics.world_time_intervals[eval_world]
    #stores list as variable
    time_interval= list(range(start_time, end_time + 1))
    #changes list data type to integer
    time=z3.int(time_interval)
    
    #initialize eval_point_2
    eval_world_2=eval_point_2["world"]
    eval_time_2= eval_point_2["time"]

    #find right hand side of "until "
    for time_interval in time_interval 
        #find interval where argument is true (note on this semantics for UNtil, we are agnostic about whether left arg can be true at the end of the interval )
        if eval_time <time_interval and semantics.true_at(rigntarg, eval__point): 
            eval_time_2=time_interval
            #break to make sure we do not move beyond the first time where rightarg is true in a history
            break 
    #duration= temporal range of left and right argument
    duration=list(range(eval_time, eval_time_2+1))

    endurant=z3.int('duration')

    #gets true times for left arg in the future 
    future_time=z3.Int('future_true_time')

#return clause (incomplete -- neds leftarg and rightarg truth values as well)
return z3.ForAll(
future_time, endurant in duration
z3.Implies(
z3.And(
future_time==endurant
# If the past_time is within the eval_world's time interval
semantics.is_valid_time_for_world(eval_world, future_time),
),
# Then the argument is true at the past_time in the eval_world
semantics.true_at(argument, {"world": eval_world, "time": endurant}),
)
)
`

[benbrastmckie]

Hey I think I see what you are on to. Here are a few points:

• Although we are working in Python, the constraints that the true_at and false_at methods return must be something Z3 understands, and so we can't include any python there (this is why z3.And() and the like are used).
• With that said, we can use all the python we want to build the right constraint that we intend to return.
• In the case of Until, we want to require the antecedent to be true at all future times before the first future time where the consequent is true (what happens then is left unconstrained).
• The next question is what we have to work with, where, in this case, we have the antecedent, consequent, and evaluation point which is a dictionary consisting of an evaluation world and evaluation time.
• We also have access to the semantics, but keep in mind that we don't yet have access to any particular model structure since we want the semantics to remains general (work for all interpretations/models of the language).
• If we look into the semantics and what attributes it includes, we find it includes world_interval_end and world_interval_start functions which say where worlds begin and end, but also world_time_interfals which is a python dictionary (so not Z3 friendly) with a note that it is for after model extraction (i.e., Z3 finds a model and we build a model structure from it).
• It would be better if world_time_interfals didn't show up in the BimodalSemantics class at all, and so I will make a note of this (the function is used in the BimodalStructure and the find_truth_condition methods for each operator which helps to assign sentences to elements of a model structure).
• So we can't use world_time_intervals in the semantic clauses because before there is a z3 model and model structure, this will just be an empty dictionary.
• The situation is similar to the model-theoretic semantics where we have a model, world, and time of evaluation, keeping in mind that we can't assume anything about the model if the model is to be truly general.
• Moreover, the semantics for Since and Until makes do without any intervals being handed over.
• It might help to use the doc string to provide a detailed conceptual target being as explicit and detailed as is useful about the given ingredients and the semantics (constraint to return) while staying within English more or less.
• One further, and more minor point is that if you want to change the time in an eval_point, one way that is nice and readable is to begin by extracting as you do, using the eval_point to define eval_time and eval_world.
• Then say you have a time variable some_time bound by a quantifier, and you want to pass that along to evaluate an argument, what you want to do is define some_point = { "world" : eval_world, "time" : some_time}, and then pass that to the true_at method along with the argument you want to evaluate.
• There are other ways to go, but this is the most explicit and readable method.

Hope this helps, and let me know if there are specific points that remain unclear. The semantics/model_structure and Z3/python divides are both tricky to navigate.